text:
/-
Copyright (c) 2021 Damiano Testa. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Damiano Testa
-/
import algebra.smul_with_zero
import algebra.regular.basic

/-!
# Action of regular elements on a module

We introduce `M`-regular elements, in the context of an `R`-module `M`.  The corresponding
predicate is called `is_smul_regular`.

There are very limited typeclass assumptions on `R` and `M`, but the "mathematical" case of interest
is a commutative ring `R` acting an a module `M`. Since the properties are "multiplicative", there
is no actual requirement of having an addition, but there is a zero in both `R` and `M`.
Smultiplications involving `0` are, of course, all trivial.

The defining property is that an element `a ∈ R` is `M`-regular if the smultiplication map
`M → M`, defined by `m ↦ a • m`, is injective.

This property is the direct generalization to modules of the property `is_left_regular` defined in
`algebra/regular`.  Lemma `is_smul_regular.is_left_regular_iff` shows that indeed the two notions
coincide.
-/

variables {R S : Type*} (M : Type*) {a b : R} {s : S}

/-- An `M`-regular element is an element `c` such that multiplication on the left by `c` is an
injective map `M → M`. -/
def is_smul_regular [has_smul R M] (c : R) := function.injective ((•) c : M → M)

lemma is_left_regular.is_smul_regular [has_mul R] {c : R} (h : is_left_regular c) :
  is_smul_regular R c := h

/-- Left-regular multiplication on `R` is equivalent to `R`-regularity of `R` itself. -/
lemma is_left_regular_iff [has_mul R] {a : R} :
  is_left_regular a ↔ is_smul_regular R a := iff.rfl

lemma is_right_regular.is_smul_regular [has_mul R] {c : R} (h : is_right_regular c) :
  is_smul_regular R (mul_opposite.op c) := h

/-- Right-regular multiplication on `R` is equivalent to `Rᵐᵒᵖ`-regularity of `R` itself. -/
lemma is_right_regular_iff [has_mul R] {a : R} :
  is_right_regular a ↔ is_smul_regular R (mul_opposite.op a) := iff.rfl

namespace is_smul_regular

variables {M}

section has_smul

variables [has_smul R M] [has_smul R S] [has_smul S M] [is_scalar_tower R S M]

/-- The product of `M`-regular elements is `M`-regular. -/
lemma smul (ra : is_smul_regular M a) (rs : is_smul_regular M s) :
  is_smul_regular M (a • s) :=
λ a b ab, rs (ra ((smul_assoc _ _ _).symm.trans (ab.trans (smul_assoc _ _ _))))

/-- If an element `b` becomes `M`-regular after multiplying it on the left by an `M`-regular
element, then `b` is `M`-regular. -/
lemma of_smul (a : R) (ab : is_smul_regular M (a • s)) :
  is_smul_regular M s :=
@function.injective.of_comp _ _ _ (λ m : M, a • m) _ (λ c d cd, ab
  (by rwa [smul_assoc, smul_assoc]))

/-- An element is `M`-regular if and only if multiplying it on the left by an `M`-regular element
is `M`-regular. -/
@[simp] lemma smul_iff (b : S) (ha : is_smul_regular M a) :
  is_smul_regular M (a • b) ↔ is_smul_regular M b :=
⟨of_smul _, ha.smul⟩

lemma is_left_regular [has_mul R] {a : R} (h : is_smul_regular R a) :
  is_left_regular a := h

lemma is_right_regular [has_mul R] {a : R} (h : is_smul_regular R (mul_opposite.op a)) :
  is_right_regular a := h

lemma mul [has_mul R] [is_scalar_tower R R M]
  (ra : is_smul_regular M a) (rb : is_smul_regular M b) : is_smul_regular M (a * b) :=
ra.smul rb

lemma of_mul [has_mul R] [is_scalar_tower R R M] (ab : is_smul_regular M (a * b)) :
  is_smul_regular M b :=
by { rw ← smul_eq_mul at ab, exact ab.of_smul _ }

@[simp] lemma mul_iff_right [has_mul R] [is_scalar_tower R R M] (ha : is_smul_regular M a) :
  is_smul_regular M (a * b) ↔ is_smul_regular M b :=
⟨of_mul, ha.mul⟩

/-- Two elements `a` and `b` are `M`-regular if and only if both products `a * b` and `b * a`
are `M`-regular. -/
lemma mul_and_mul_iff [has_mul R] [is_scalar_tower R R M] :
  is_smul_regular M (a * b) ∧ is_smul_regular M (b * a) ↔
  is_smul_regular M a ∧ is_smul_regular M b :=
begin
  refine ⟨_, _⟩,
  { rintros ⟨ab, ba⟩,
    refine ⟨ba.of_mul, ab.of_mul⟩ },
  { rintros ⟨ha, hb⟩,
    exact ⟨ha.mul hb, hb.mul ha⟩ }
end

end has_smul

section monoid

variables [monoid R] [mul_action R M]

variable (M)

/-- One is `M`-regular always. -/
@[simp] lemma one : is_smul_regular M (1 : R) :=
λ a b ab, by rwa [one_smul, one_smul] at ab

variable {M}

/-- An element of `R` admitting a left inverse is `M`-regular. -/
lemma of_mul_eq_one (h : a * b = 1) : is_smul_regular M b :=
of_mul (by { rw h, exact one M })

/-- Any power of an `M`-regular element is `M`-regular. -/
lemma pow (n : ℕ) (ra : is_smul_regular M a) : is_smul_regular M (a ^ n) :=
begin
  induction n with n hn,
  { simp only [one, pow_zero] },
  { rw pow_succ, exact (ra.smul_iff (a ^ n)).mpr hn }
end

/-- An element `a` is `M`-regular if and only if a positive power of `a` is `M`-regular. -/
lemma pow_iff {n : ℕ} (n0 : 0 < n) :
  is_smul_regular M (a ^ n) ↔ is_smul_regular M a :=
begin
  refine ⟨_, pow n⟩,
  rw [← nat.succ_pred_eq_of_pos n0, pow_succ', ← smul_eq_mul],
  exact of_smul _,
end

end monoid

section monoid_smul

variables [monoid S] [has_smul R M] [has_smul R S] [mul_action S M] [is_scalar_tower R S M]

/-- An element of `S` admitting a left inverse in `R` is `M`-regular. -/
lemma of_smul_eq_one (h : a • s = 1) : is_smul_regular M s :=
of_smul a (by { rw h, exact one M })

end monoid_smul

section monoid_with_zero

variables [monoid_with_zero R] [monoid_with_zero S] [has_zero M]
          [mul_action_with_zero R M] [mul_action_with_zero R S] [mul_action_with_zero S M]
          [is_scalar_tower R S M]

/-- The element `0` is `M`-regular if and only if `M` is trivial. -/
protected lemma subsingleton (h : is_smul_regular M (0 : R)) : subsingleton M :=
⟨λ a b, h (by repeat { rw mul_action_with_zero.zero_smul })⟩

/-- The element `0` is `M`-regular if and only if `M` is trivial. -/
lemma zero_iff_subsingleton : is_smul_regular M (0 : R) ↔ subsingleton M :=
⟨λ h, h.subsingleton, λ H a b h, @subsingleton.elim _ H a b⟩

/-- The `0` element is not `M`-regular, on a non-trivial module. -/
lemma not_zero_iff : ¬ is_smul_regular M (0 : R) ↔ nontrivial M :=
begin
  rw [nontrivial_iff, not_iff_comm, zero_iff_subsingleton, subsingleton_iff],
  push_neg,
  exact iff.rfl
end

/-- The element `0` is `M`-regular when `M` is trivial. -/
lemma zero [sM : subsingleton M] : is_smul_regular M (0 : R) :=
zero_iff_subsingleton.mpr sM

/-- The `0` element is not `M`-regular, on a non-trivial module. -/
lemma not_zero [nM : nontrivial M] : ¬ is_smul_regular M (0 : R) :=
not_zero_iff.mpr nM

end monoid_with_zero

section comm_semigroup

variables [comm_semigroup R] [has_smul R M] [is_scalar_tower R R M]

/-- A product is `M`-regular if and only if the factors are. -/
lemma mul_iff : is_smul_regular M (a * b) ↔
  is_smul_regular M a ∧ is_smul_regular M b :=
begin
  rw ← mul_and_mul_iff,
  exact ⟨λ ab, ⟨ab, by rwa mul_comm⟩, λ rab, rab.1⟩
end

end comm_semigroup

end is_smul_regular

section group

variables {G : Type*} [group G]

/-- An element of a group acting on a Type is regular. This relies on the availability
of the inverse given by groups, since there is no `left_cancel_smul` typeclass. -/
lemma is_smul_regular_of_group [mul_action G R] (g : G) : is_smul_regular R g :=
begin
  intros x y h,
  convert congr_arg ((•) g⁻¹) h using 1;
  simp [←smul_assoc]
end

end group

section units

variables [monoid R] [mul_action R M]

/-- Any element in `Rˣ` is `M`-regular. -/
lemma units.is_smul_regular (a : Rˣ) : is_smul_regular M (a : R) :=
is_smul_regular.of_mul_eq_one a.inv_val

/-- A unit is `M`-regular. -/
lemma is_unit.is_smul_regular (ua : is_unit a) : is_smul_regular M a :=
begin
  rcases ua with ⟨a, rfl⟩,
  exact a.is_smul_regular M
end

end units

author: Parinya-Siri

repo: lean-machine-learning


text:
/-
Copyright (c) 2021 Yakov Pechersky. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yakov Pechersky

! This file was ported from Lean 3 source module data.fintype.list
! leanprover-community/mathlib commit cc70d9141824ea8982d1562ce009952f2c3ece30
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathbin.Data.Fintype.Basic
import Mathbin.Data.Finset.Powerset

/-!

# Fintype instance for nodup lists

> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.

The subtype of `{l : list α // l.nodup}` over a `[fintype α]`
admits a `fintype` instance.

## Implementation details
To construct the `fintype` instance, a function lifting a `multiset α`
to the `finset (list α)` that can construct it is provided.
This function is applied to the `finset.powerset` of `finset.univ`.

In general, a `decidable_eq` instance is not necessary to define this function,
but a proof of `(list.permutations l).nodup` is required to avoid it,
which is a TODO.

-/

variable {α : Type _} [DecidableEq α]

open List

namespace Multiset

#print Multiset.lists /-
/-- The `finset` of `l : list α` that, given `m : multiset α`, have the property `⟦l⟧ = m`.
-/
def lists : Multiset α → Finset (List α) := fun s =>
  Quotient.liftOn s (fun l => l.permutations.toFinset) fun l l' (h : l ~ l') =>
    by
    ext sl
    simp only [mem_permutations, List.mem_toFinset]
    exact ⟨fun hs => hs.trans h, fun hs => hs.trans h.symm⟩
#align multiset.lists Multiset.lists
-/

#print Multiset.lists_coe /-
@[simp]
theorem lists_coe (l : List α) : lists (l : Multiset α) = l.permutations.toFinset :=
  rfl
#align multiset.lists_coe Multiset.lists_coe
-/

#print Multiset.mem_lists_iff /-
@[simp]
theorem mem_lists_iff (s : Multiset α) (l : List α) : l ∈ lists s ↔ s = ⟦l⟧ :=
  by
  induction s using Quotient.inductionOn
  simpa using perm_comm
#align multiset.mem_lists_iff Multiset.mem_lists_iff
-/

end Multiset

#print fintypeNodupList /-
instance fintypeNodupList [Fintype α] : Fintype { l : List α // l.Nodup } :=
  Fintype.subtype ((Finset.univ : Finset α).powerset.bunionᵢ fun s => s.val.lists) fun l =>
    by
    suffices (∃ a : Finset α, a.val = ↑l) ↔ l.nodup by simpa
    constructor
    · rintro ⟨s, hs⟩
      simpa [← Multiset.coe_nodup, ← hs] using s.nodup
    · intro hl
      refine' ⟨⟨↑l, hl⟩, _⟩
      simp
#align fintype_nodup_list fintypeNodupList
-/

author: leanprover-community


text:
/-
Copyright (c) 2020 Aaron Anderson. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Aaron Anderson
-/
import algebra.squarefree
import data.nat.factorization.prime_pow
import data.nat.prime_norm_num
import ring_theory.int.basic

/-!
# Lemmas about squarefreeness of natural numbers
A number is squarefree when it is not divisible by any squares except the squares of units.

## Main Results
 - `nat.squarefree_iff_nodup_factors`: A positive natural number `x` is squarefree iff
  the list `factors x` has no duplicate factors.

## Tags
squarefree, multiplicity

-/

namespace nat

lemma squarefree_iff_nodup_factors {n : ℕ} (h0 : n ≠ 0) :
  squarefree n ↔ n.factors.nodup :=
begin
  rw [unique_factorization_monoid.squarefree_iff_nodup_normalized_factors h0, nat.factors_eq],
  simp,
end

theorem squarefree_iff_prime_squarefree {n : ℕ} : squarefree n ↔ ∀ x, prime x → ¬ x * x ∣ n :=
squarefree_iff_irreducible_sq_not_dvd_of_exists_irreducible ⟨_, prime_two⟩

lemma squarefree.factorization_le_one {n : ℕ} (p : ℕ) (hn : squarefree n) :
  n.factorization p ≤ 1 :=
begin
  rcases eq_or_ne n 0 with rfl | hn',
  { simp },
  rw [multiplicity.squarefree_iff_multiplicity_le_one] at hn,
  by_cases hp : p.prime,
  { have := hn p,
    simp only [multiplicity_eq_factorization hp hn', nat.is_unit_iff, hp.ne_one, or_false] at this,
    exact_mod_cast this },
  { rw factorization_eq_zero_of_non_prime _ hp,
    exact zero_le_one }
end

lemma squarefree_of_factorization_le_one {n : ℕ} (hn : n ≠ 0) (hn' : ∀ p, n.factorization p ≤ 1) :
  squarefree n :=
begin
  rw [squarefree_iff_nodup_factors hn, list.nodup_iff_count_le_one],
  intro a,
  rw factors_count_eq,
  apply hn',
end

lemma squarefree_iff_factorization_le_one {n : ℕ} (hn : n ≠ 0) :
  squarefree n ↔ ∀ p, n.factorization p ≤ 1 :=
⟨λ p hn, squarefree.factorization_le_one hn p, squarefree_of_factorization_le_one hn⟩

lemma squarefree_pow_iff {n k : ℕ} (hn : n ≠ 1) (hk : k ≠ 0) :
  squarefree (n ^ k) ↔ squarefree n ∧ k = 1 :=
begin
  refine ⟨λ h, _, by { rintro ⟨hn, rfl⟩, simpa }⟩,
  rcases eq_or_ne n 0 with rfl | hn₀,
  { simpa [zero_pow hk.bot_lt] using h },
  refine ⟨h.squarefree_of_dvd (dvd_pow_self _ hk), by_contradiction $ λ h₁, _⟩,
  have : 2 ≤ k := k.two_le_iff.mpr ⟨hk, h₁⟩,
  apply hn (nat.is_unit_iff.1 (h _ _)),
  rw ←sq,
  exact pow_dvd_pow _ this
end

lemma squarefree_and_prime_pow_iff_prime {n : ℕ} :
  squarefree n ∧ is_prime_pow n ↔ prime n :=
begin
  refine iff.symm ⟨λ hn, ⟨hn.squarefree, hn.is_prime_pow⟩, _⟩,
  rw is_prime_pow_nat_iff,
  rintro ⟨h, p, k, hp, hk, rfl⟩,
  rw squarefree_pow_iff hp.ne_one hk.ne' at h,
  rwa [h.2, pow_one],
end

/-- Assuming that `n` has no factors less than `k`, returns the smallest prime `p` such that
  `p^2 ∣ n`. -/
def min_sq_fac_aux : ℕ → ℕ → option ℕ
| n k :=
  if h : n < k * k then none else
  have nat.sqrt n + 2 - (k + 2) < nat.sqrt n + 2 - k,
    by { rw nat.add_sub_add_right, exact nat.min_fac_lemma n k h },
  if k ∣ n then
    let n' := n / k in
    have nat.sqrt n' + 2 - (k + 2) < nat.sqrt n + 2 - k, from
      lt_of_le_of_lt (nat.sub_le_sub_right
        (nat.add_le_add_right (nat.sqrt_le_sqrt $ nat.div_le_self _ _) _) _) this,
    if k ∣ n' then some k else min_sq_fac_aux n' (k + 2)
  else min_sq_fac_aux n (k + 2)
using_well_founded {rel_tac :=
  λ _ _, `[exact ⟨_, measure_wf (λ ⟨n, k⟩, nat.sqrt n + 2 - k)⟩]}

/-- Returns the smallest prime factor `p` of `n` such that `p^2 ∣ n`, or `none` if there is no
  such `p` (that is, `n` is squarefree). See also `squarefree_iff_min_sq_fac`. -/
def min_sq_fac (n : ℕ) : option ℕ :=
if 2 ∣ n then
  let n' := n / 2 in
  if 2 ∣ n' then some 2 else min_sq_fac_aux n' 3
else min_sq_fac_aux n 3

/-- The correctness property of the return value of `min_sq_fac`.
  * If `none`, then `n` is squarefree;
  * If `some d`, then `d` is a minimal square factor of `n` -/
def min_sq_fac_prop (n : ℕ) : option ℕ → Prop
| none := squarefree n
| (some d) := prime d ∧ d * d ∣ n ∧ ∀ p, prime p → p * p ∣ n → d ≤ p

theorem min_sq_fac_prop_div (n) {k} (pk : prime k) (dk : k ∣ n) (dkk : ¬ k * k ∣ n)
  {o} (H : min_sq_fac_prop (n / k) o) : min_sq_fac_prop n o :=
begin
  have : ∀ p, prime p → p*p ∣ n → k*(p*p) ∣ n := λ p pp dp,
    have _ := (coprime_primes pk pp).2 (λ e, by { subst e, contradiction }),
    (coprime_mul_iff_right.2 ⟨this, this⟩).mul_dvd_of_dvd_of_dvd dk dp,
  cases o with d,
  { rw [min_sq_fac_prop, squarefree_iff_prime_squarefree] at H ⊢,
    exact λ p pp dp, H p pp ((dvd_div_iff dk).2 (this _ pp dp)) },
  { obtain ⟨H1, H2, H3⟩ := H,
    simp only [dvd_div_iff dk] at H2 H3,
    exact ⟨H1, dvd_trans (dvd_mul_left _ _) H2, λ p pp dp, H3 _ pp (this _ pp dp)⟩ }
end

theorem min_sq_fac_aux_has_prop : ∀ {n : ℕ} k, 0 < n → ∀ i, k = 2*i+3 →
  (∀ m, prime m → m ∣ n → k ≤ m) → min_sq_fac_prop n (min_sq_fac_aux n k)
| n k := λ n0 i e ih, begin
  rw min_sq_fac_aux,
  by_cases h : n < k*k; simp [h],
  { refine squarefree_iff_prime_squarefree.2 (λ p pp d, _),
    have := ih p pp (dvd_trans ⟨_, rfl⟩ d),
    have := nat.mul_le_mul this this,
    exact not_le_of_lt h (le_trans this (le_of_dvd n0 d)) },
  have k2 : 2 ≤ k, { subst e, exact dec_trivial },
  have k0 : 0 < k := lt_of_lt_of_le dec_trivial k2,
  have IH : ∀ n', n' ∣ n → ¬ k ∣ n' → min_sq_fac_prop n' (n'.min_sq_fac_aux (k + 2)),
  { intros n' nd' nk,
    have hn' := le_of_dvd n0 nd',
    refine
      have nat.sqrt n' - k < nat.sqrt n + 2 - k, from
        lt_of_le_of_lt (nat.sub_le_sub_right (nat.sqrt_le_sqrt hn') _) (nat.min_fac_lemma n k h),
      @min_sq_fac_aux_has_prop n' (k+2) (pos_of_dvd_of_pos nd' n0)
        (i+1) (by simp [e, left_distrib]) (λ m m2 d, _),
    cases nat.eq_or_lt_of_le (ih m m2 (dvd_trans d nd')) with me ml,
    { subst me, contradiction },
    apply (nat.eq_or_lt_of_le ml).resolve_left, intro me,
    rw [← me, e] at d, change 2 * (i + 2) ∣ n' at d,
    have := ih _ prime_two (dvd_trans (dvd_of_mul_right_dvd d) nd'),
    rw e at this, exact absurd this dec_trivial },
  have pk : k ∣ n → prime k,
  { refine λ dk, prime_def_min_fac.2 ⟨k2, le_antisymm (min_fac_le k0) _⟩,
    exact ih _ (min_fac_prime (ne_of_gt k2)) (dvd_trans (min_fac_dvd _) dk) },
  split_ifs with dk dkk,
  { exact ⟨pk dk, (nat.dvd_div_iff dk).1 dkk, λ p pp d, ih p pp (dvd_trans ⟨_, rfl⟩ d)⟩ },
  { specialize IH (n/k) (div_dvd_of_dvd dk) dkk,
    exact min_sq_fac_prop_div _ (pk dk) dk (mt (nat.dvd_div_iff dk).2 dkk) IH },
  { exact IH n (dvd_refl _) dk }
end
using_well_founded {rel_tac :=
  λ _ _, `[exact ⟨_, measure_wf (λ ⟨n, k⟩, nat.sqrt n + 2 - k)⟩]}

theorem min_sq_fac_has_prop (n : ℕ) : min_sq_fac_prop n (min_sq_fac n) :=
begin
  dunfold min_sq_fac, split_ifs with d2 d4,
  { exact ⟨prime_two, (dvd_div_iff d2).1 d4, λ p pp _, pp.two_le⟩ },
  { cases nat.eq_zero_or_pos n with n0 n0, { subst n0, cases d4 dec_trivial },
    refine min_sq_fac_prop_div _ prime_two d2 (mt (dvd_div_iff d2).2 d4) _,
    refine min_sq_fac_aux_has_prop 3 (nat.div_pos (le_of_dvd n0 d2) dec_trivial) 0 rfl _,
    refine λ p pp dp, succ_le_of_lt (lt_of_le_of_ne pp.two_le _),
    rintro rfl, contradiction },
  { cases nat.eq_zero_or_pos n with n0 n0, { subst n0, cases d2 dec_trivial },
    refine min_sq_fac_aux_has_prop _ n0 0 rfl _,
    refine λ p pp dp, succ_le_of_lt (lt_of_le_of_ne pp.two_le _),
    rintro rfl, contradiction },
end

theorem min_sq_fac_prime {n d : ℕ} (h : n.min_sq_fac = some d) : prime d :=
by { have := min_sq_fac_has_prop n, rw h at this, exact this.1 }

theorem min_sq_fac_dvd {n d : ℕ} (h : n.min_sq_fac = some d) : d * d ∣ n :=
by { have := min_sq_fac_has_prop n, rw h at this, exact this.2.1 }

theorem min_sq_fac_le_of_dvd {n d : ℕ} (h : n.min_sq_fac = some d)
  {m} (m2 : 2 ≤ m) (md : m * m ∣ n) : d ≤ m :=
begin
  have := min_sq_fac_has_prop n, rw h at this,
  have fd := min_fac_dvd m,
  exact le_trans
    (this.2.2 _ (min_fac_prime $ ne_of_gt m2) (dvd_trans (mul_dvd_mul fd fd) md))
    (min_fac_le $ lt_of_lt_of_le dec_trivial m2),
end

lemma squarefree_iff_min_sq_fac {n : ℕ} :
  squarefree n ↔ n.min_sq_fac = none :=
begin
  have := min_sq_fac_has_prop n,
  split; intro H,
  { cases n.min_sq_fac with d, {refl},
    cases squarefree_iff_prime_squarefree.1 H _ this.1 this.2.1 },
  { rwa H at this }
end

instance : decidable_pred (squarefree : ℕ → Prop) :=
λ n, decidable_of_iff' _ squarefree_iff_min_sq_fac

theorem squarefree_two : squarefree 2 := by rw squarefree_iff_nodup_factors; norm_num

open unique_factorization_monoid

lemma divisors_filter_squarefree {n : ℕ} (h0 : n ≠ 0) :
  (n.divisors.filter squarefree).val =
    (unique_factorization_monoid.normalized_factors n).to_finset.powerset.val.map
      (λ x, x.val.prod) :=
begin
  rw (finset.nodup _).ext ((finset.nodup _).map_on _),
  { intro a,
    simp only [multiset.mem_filter, id.def, multiset.mem_map, finset.filter_val, ← finset.mem_def,
      mem_divisors],
    split,
    { rintro ⟨⟨an, h0⟩, hsq⟩,
      use (unique_factorization_monoid.normalized_factors a).to_finset,
      simp only [id.def, finset.mem_powerset],
      rcases an with ⟨b, rfl⟩,
      rw mul_ne_zero_iff at h0,
      rw unique_factorization_monoid.squarefree_iff_nodup_normalized_factors h0.1 at hsq,
      rw [multiset.to_finset_subset, multiset.to_finset_val, hsq.dedup, ← associated_iff_eq,
        normalized_factors_mul h0.1 h0.2],
      exact ⟨multiset.subset_of_le (multiset.le_add_right _ _), normalized_factors_prod h0.1⟩ },
    { rintro ⟨s, hs, rfl⟩,
      rw [finset.mem_powerset, ← finset.val_le_iff, multiset.to_finset_val] at hs,
      have hs0 : s.val.prod ≠ 0,
      { rw [ne.def, multiset.prod_eq_zero_iff],
        simp only [exists_prop, id.def, exists_eq_right],
        intro con,
        apply not_irreducible_zero (irreducible_of_normalized_factor 0
            (multiset.mem_dedup.1 (multiset.mem_of_le hs con))) },
      rw (normalized_factors_prod h0).symm.dvd_iff_dvd_right,
      refine ⟨⟨multiset.prod_dvd_prod_of_le (le_trans hs (multiset.dedup_le _)), h0⟩, _⟩,
      have h := unique_factorization_monoid.factors_unique irreducible_of_normalized_factor
        (λ x hx, irreducible_of_normalized_factor x (multiset.mem_of_le
          (le_trans hs (multiset.dedup_le _)) hx)) (normalized_factors_prod hs0),
      rw [associated_eq_eq, multiset.rel_eq] at h,
      rw [unique_factorization_monoid.squarefree_iff_nodup_normalized_factors hs0, h],
      apply s.nodup } },
  { intros x hx y hy h,
    rw [← finset.val_inj, ← multiset.rel_eq, ← associated_eq_eq],
    rw [← finset.mem_def, finset.mem_powerset] at hx hy,
    apply unique_factorization_monoid.factors_unique _ _ (associated_iff_eq.2 h),
    { intros z hz,
      apply irreducible_of_normalized_factor z,
      rw ← multiset.mem_to_finset,
      apply hx hz },
    { intros z hz,
      apply irreducible_of_normalized_factor z,
      rw ← multiset.mem_to_finset,
      apply hy hz } }
end

open_locale big_operators

lemma sum_divisors_filter_squarefree {n : ℕ} (h0 : n ≠ 0)
  {α : Type*} [add_comm_monoid α] {f : ℕ → α} :
  ∑ i in (n.divisors.filter squarefree), f i =
    ∑ i in (unique_factorization_monoid.normalized_factors n).to_finset.powerset, f (i.val.prod) :=
by rw [finset.sum_eq_multiset_sum, divisors_filter_squarefree h0, multiset.map_map,
    finset.sum_eq_multiset_sum]

lemma sq_mul_squarefree_of_pos {n : ℕ} (hn : 0 < n) :
  ∃ a b : ℕ, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ squarefree a :=
begin
  let S := {s ∈ finset.range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2},
  have hSne : S.nonempty,
  { use 1,
    have h1 : 0 < n ∧ ∃ (x : ℕ), 1 = x ^ 2 := ⟨hn, ⟨1, (one_pow 2).symm⟩⟩,
    simpa [S] },
  let s := finset.max' S hSne,
  have hs : s ∈ S := finset.max'_mem S hSne,
  simp only [finset.sep_def, S, finset.mem_filter, finset.mem_range] at hs,
  obtain ⟨hsn1, ⟨a, hsa⟩, ⟨b, hsb⟩⟩ := hs,
  rw hsa at hn,
  obtain ⟨hlts, hlta⟩ := canonically_ordered_comm_semiring.mul_pos.mp hn,
  rw hsb at hsa hn hlts,
  refine ⟨a, b, hlta, (pow_pos_iff zero_lt_two).mp hlts, hsa.symm, _⟩,
  rintro x ⟨y, hy⟩,
  rw nat.is_unit_iff,
  by_contra hx,
  refine lt_le_antisymm _ (finset.le_max' S ((b * x) ^ 2) _),
  { simp_rw [S, hsa, finset.sep_def, finset.mem_filter, finset.mem_range],
    refine ⟨lt_succ_iff.mpr (le_of_dvd hn _), _, ⟨b * x, rfl⟩⟩; use y; rw hy; ring },
  { convert lt_mul_of_one_lt_right hlts
      (one_lt_pow 2 x zero_lt_two (one_lt_iff_ne_zero_and_ne_one.mpr ⟨λ h, by simp * at *, hx⟩)),
    rw mul_pow },
end

lemma sq_mul_squarefree_of_pos' {n : ℕ} (h : 0 < n) :
  ∃ a b : ℕ, (b + 1) ^ 2 * (a + 1) = n ∧ squarefree (a + 1) :=
begin
  obtain ⟨a₁, b₁, ha₁, hb₁, hab₁, hab₂⟩ := sq_mul_squarefree_of_pos h,
  refine ⟨a₁.pred, b₁.pred, _, _⟩;
  simpa only [add_one, succ_pred_eq_of_pos, ha₁, hb₁],
end

lemma sq_mul_squarefree (n : ℕ) : ∃ a b : ℕ, b ^ 2 * a = n ∧ squarefree a :=
begin
  cases n,
  { exact ⟨1, 0, (by simp), squarefree_one⟩ },
  { obtain ⟨a, b, -, -, h₁, h₂⟩ := sq_mul_squarefree_of_pos (succ_pos n),
    exact ⟨a, b, h₁, h₂⟩ },
end

/-- `squarefree` is multiplicative. Note that the → direction does not require `hmn`
and generalizes to arbitrary commutative monoids. See `squarefree.of_mul_left` and
`squarefree.of_mul_right` above for auxiliary lemmas. -/
lemma squarefree_mul {m n : ℕ} (hmn : m.coprime n) :
  squarefree (m * n) ↔ squarefree m ∧ squarefree n :=
begin
  simp only [squarefree_iff_prime_squarefree, ←sq, ←forall_and_distrib],
  refine ball_congr (λ p hp, _),
  simp only [hmn.is_prime_pow_dvd_mul (hp.is_prime_pow.pow two_ne_zero), not_or_distrib],
end

end nat

/-! ### Square-free prover -/

open norm_num

namespace tactic
namespace norm_num

/-- A predicate representing partial progress in a proof of `squarefree`. -/
def squarefree_helper (n k : ℕ) : Prop :=
0 < k → (∀ m, nat.prime m → m ∣ bit1 n → bit1 k ≤ m) → squarefree (bit1 n)

lemma squarefree_bit10 (n : ℕ) (h : squarefree_helper n 1) :
  squarefree (bit0 (bit1 n)) :=
begin
  refine @nat.min_sq_fac_prop_div _ _ nat.prime_two two_dvd_bit0 _ none _,
  { rw [bit0_eq_two_mul (bit1 n), mul_dvd_mul_iff_left (two_ne_zero' ℕ)],
    exact nat.not_two_dvd_bit1 _ },
  { rw [bit0_eq_two_mul, nat.mul_div_right _ (dec_trivial:0<2)],
    refine h dec_trivial (λ p pp dp, nat.succ_le_of_lt (lt_of_le_of_ne pp.two_le _)),
    rintro rfl, exact nat.not_two_dvd_bit1 _ dp }
end

lemma squarefree_bit1 (n : ℕ) (h : squarefree_helper n 1) :
  squarefree (bit1 n) :=
begin
  refine h dec_trivial (λ p pp dp, nat.succ_le_of_lt (lt_of_le_of_ne pp.two_le _)),
  rintro rfl, exact nat.not_two_dvd_bit1 _ dp
end

lemma squarefree_helper_0 {k} (k0 : 0 < k)
  {p : ℕ} (pp : nat.prime p) (h : bit1 k ≤ p) : bit1 (k + 1) ≤ p ∨ bit1 k = p :=
begin
  rcases lt_or_eq_of_le h with (hp:_+1≤_) | hp,
  { rw [bit1, bit0_eq_two_mul] at hp, change 2*(_+1) ≤ _ at hp,
    rw [bit1, bit0_eq_two_mul],
    refine or.inl (lt_of_le_of_ne hp _), unfreezingI { rintro rfl },
    exact nat.not_prime_mul dec_trivial (lt_add_of_pos_left _ k0) pp },
  { exact or.inr hp }
end

lemma squarefree_helper_1 (n k k' : ℕ) (e : k + 1 = k')
  (hk : nat.prime (bit1 k) → ¬ bit1 k ∣ bit1 n)
  (H : squarefree_helper n k') : squarefree_helper n k :=
λ k0 ih, begin
  subst e,
  refine H (nat.succ_pos _) (λ p pp dp, _),
  refine (squarefree_helper_0 k0 pp (ih p pp dp)).resolve_right (λ hp, _),
  subst hp, cases hk pp dp
end

lemma squarefree_helper_2 (n k k' c : ℕ) (e : k + 1 = k')
  (hc : bit1 n % bit1 k = c) (c0 : 0 < c)
  (h : squarefree_helper n k') : squarefree_helper n k :=
begin
  refine squarefree_helper_1 _ _ _ e (λ _, _) h,
  refine mt _ (ne_of_gt c0), intro e₁,
  rwa [← hc, ← nat.dvd_iff_mod_eq_zero],
end

lemma squarefree_helper_3 (n n' k k' c : ℕ) (e : k + 1 = k')
  (hn' : bit1 n' * bit1 k = bit1 n)
  (hc : bit1 n' % bit1 k = c) (c0 : 0 < c)
  (H : squarefree_helper n' k') : squarefree_helper n k :=
λ k0 ih, begin
  subst e,
  have k0' : 0 < bit1 k := bit1_pos (nat.zero_le _),
  have dn' : bit1 n' ∣ bit1 n := ⟨_, hn'.symm⟩,
  have dk : bit1 k ∣ bit1 n := ⟨_, ((mul_comm _ _).trans hn').symm⟩,
  have : bit1 n / bit1 k = bit1 n',
  { rw [← hn', nat.mul_div_cancel _ k0'] },
  have k2 : 2 ≤ bit1 k := nat.succ_le_succ (bit0_pos k0),
  have pk : (bit1 k).prime,
  { refine nat.prime_def_min_fac.2 ⟨k2, le_antisymm (nat.min_fac_le k0') _⟩,
    exact ih _ (nat.min_fac_prime (ne_of_gt k2)) (dvd_trans (nat.min_fac_dvd _) dk) },
  have dkk' : ¬ bit1 k ∣ bit1 n', {rw [nat.dvd_iff_mod_eq_zero, hc], exact ne_of_gt c0},
  have dkk : ¬ bit1 k * bit1 k ∣ bit1 n, {rwa [← nat.dvd_div_iff dk, this]},
  refine @nat.min_sq_fac_prop_div _ _ pk dk dkk none _,
  rw this, refine H (nat.succ_pos _) (λ p pp dp, _),
  refine (squarefree_helper_0 k0 pp (ih p pp $ dvd_trans dp dn')).resolve_right (λ e, _),
  subst e, contradiction
end

lemma squarefree_helper_4 (n k k' : ℕ) (e : bit1 k * bit1 k = k')
  (hd : bit1 n < k') : squarefree_helper n k :=
begin
  cases nat.eq_zero_or_pos n with h h,
  { subst n, exact λ _ _, squarefree_one },
  subst e,
  refine λ k0 ih, irreducible.squarefree (nat.prime_def_le_sqrt.2 ⟨bit1_lt_bit1.2 h, _⟩),
  intros m m2 hm md,
  obtain ⟨p, pp, hp⟩ := nat.exists_prime_and_dvd (ne_of_gt m2),
  have := (ih p pp (dvd_trans hp md)).trans
    (le_trans (nat.le_of_dvd (lt_of_lt_of_le dec_trivial m2) hp) hm),
  rw nat.le_sqrt at this,
  exact not_le_of_lt hd this
end

lemma not_squarefree_mul (a aa b n : ℕ) (ha : a * a = aa) (hb : aa * b = n)
  (h₁ : 1 < a) : ¬ squarefree n :=
by { rw [← hb, ← ha], exact λ H, ne_of_gt h₁ (nat.is_unit_iff.1 $ H _ ⟨_, rfl⟩) }

/-- Given `e` a natural numeral and `a : nat` with `a^2 ∣ n`, return `⊢ ¬ squarefree e`. -/
meta def prove_non_squarefree (e : expr) (n a : ℕ) : tactic expr := do
  let ea := reflect a,
  let eaa := reflect (a*a),
  c ← mk_instance_cache `(nat),
  (c, p₁) ← prove_lt_nat c `(1) ea,
  let b := n / (a*a), let eb := reflect b,
  (c, eaa, pa) ← prove_mul_nat c ea ea,
  (c, e', pb) ← prove_mul_nat c eaa eb,
  guard (e' =ₐ e),
  return $ `(@not_squarefree_mul).mk_app [ea, eaa, eb, e, pa, pb, p₁]

/-- Given `en`,`en1 := bit1 en`, `n1` the value of `en1`, `ek`,
  returns `⊢ squarefree_helper en ek`. -/
meta def prove_squarefree_aux : ∀ (ic : instance_cache) (en en1 : expr) (n1 : ℕ)
  (ek : expr) (k : ℕ), tactic expr
| ic en en1 n1 ek k := do
  let k1 := bit1 k,
  let ek1 := `(bit1:ℕ→ℕ).mk_app [ek],
  if n1 < k1*k1 then do
    (ic, ek', p₁) ← prove_mul_nat ic ek1 ek1,
    (ic, p₂) ← prove_lt_nat ic en1 ek',
    pure $ `(squarefree_helper_4).mk_app [en, ek, ek', p₁, p₂]
  else do
    let c := n1 % k1,
    let k' := k+1, let ek' := reflect k',
    (ic, p₁) ← prove_succ ic ek ek',
    if c = 0 then do
      let n1' := n1 / k1,
      let n' := n1' / 2, let en' := reflect n',
      let en1' := `(bit1:ℕ→ℕ).mk_app [en'],
      (ic, _, pn') ← prove_mul_nat ic en1' ek1,
      let c := n1' % k1,
      guard (c ≠ 0),
      (ic, ec, pc) ← prove_div_mod ic en1' ek1 tt,
      (ic, p₀) ← prove_pos ic ec,
      p₂ ← prove_squarefree_aux ic en' en1' n1' ek' k',
      pure $ `(squarefree_helper_3).mk_app [en, en', ek, ek', ec, p₁, pn', pc, p₀, p₂]
    else do
      (ic, ec, pc) ← prove_div_mod ic en1 ek1 tt,
      (ic, p₀) ← prove_pos ic ec,
      p₂ ← prove_squarefree_aux ic en en1 n1 ek' k',
      pure $ `(squarefree_helper_2).mk_app [en, ek, ek', ec, p₁, pc, p₀, p₂]

/-- Given `n > 0` a squarefree natural numeral, returns `⊢ squarefree n`. -/
meta def prove_squarefree (en : expr) (n : ℕ) : tactic expr :=
match match_numeral en with
| match_numeral_result.one := pure `(@squarefree_one ℕ _)
| match_numeral_result.bit0 en1 := match match_numeral en1 with
  | match_numeral_result.one := pure `(nat.squarefree_two)
  | match_numeral_result.bit1 en := do
    ic ← mk_instance_cache `(ℕ),
    p ← prove_squarefree_aux ic en en1 (n / 2) `(1:ℕ) 1,
    pure $ `(squarefree_bit10).mk_app [en, p]
  | _ := failed
  end
| match_numeral_result.bit1 en' := do
  ic ← mk_instance_cache `(ℕ),
  p ← prove_squarefree_aux ic en' en n `(1:ℕ) 1,
  pure $ `(squarefree_bit1).mk_app [en', p]
| _ := failed
end

/-- Evaluates the `squarefree` predicate on naturals. -/
@[norm_num] meta def eval_squarefree : expr → tactic (expr × expr)
| `(squarefree (%%e : ℕ)) := do
  n ← e.to_nat,
  match n with
  | 0 := false_intro `(@not_squarefree_zero ℕ _ _)
  | 1 := true_intro `(@squarefree_one ℕ _)
  | _ := match n.min_sq_fac with
    | some d := prove_non_squarefree e n d >>= false_intro
    | none := prove_squarefree e n >>= true_intro
    end
  end
| _ := failed

end norm_num
end tactic

repo: mathlib


text:
import Smt

open Lean Meta Elab Tactic in
elab "extract_def" i:ident : tactic => do
  let nm ← resolveGlobalConstNoOverloadWithInfo i
  let _ ← Smt.addEqnDefForConst nm

def foo : Int := 10

example : foo = 10 := by
  extract_def foo
  exact foo.def

def bar (a b : Int) : Int := a + b

example : bar 2 3 = 2 + 3 := by
  extract_def bar
  exact bar.def 2 3

def baz (a : Int) : Int → Int := (a + ·)

example : baz 2 3 = 2 + 3 := by
  extract_def baz
  exact baz.def 2 3

def baw (a : Int) : Int → Int := Int.add a

example : baw 2 3 = 2 + 3 := by
  extract_def baw
  exact baw.def 2 3

author: ufmg-smite

repo: lean-smt

save_path: github-repos/lean/ufmg-smite-lean-smt


text:
/-
Copyright (c) 2021 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison

! This file was ported from Lean 3 source module category_theory.linear.basic
! leanprover-community/mathlib commit 3dec44d0b621a174c56e994da4aae15ba60110a2
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathbin.CategoryTheory.Preadditive.Basic
import Mathbin.Algebra.Module.LinearMap
import Mathbin.Algebra.Invertible
import Mathbin.Algebra.Algebra.Basic

/-!
# Linear categories

> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.

An `R`-linear category is a category in which `X ⟶ Y` is an `R`-module in such a way that
composition of morphisms is `R`-linear in both variables.

Note that sometimes in the literature a "linear category" is further required to be abelian.

## Implementation

Corresponding to the fact that we need to have an `add_comm_group X` structure in place
to talk about a `module R X` structure,
we need `preadditive C` as a prerequisite typeclass for `linear R C`.
This makes for longer signatures than would be ideal.

## Future work

It would be nice to have a usable framework of enriched categories in which this just became
a category enriched in `Module R`.

-/

universe w v u

open CategoryTheory.Limits

open LinearMap

namespace CategoryTheory

#print CategoryTheory.Linear /-
/-- A category is called `R`-linear if `P ⟶ Q` is an `R`-module such that composition is
    `R`-linear in both variables. -/
class Linear (R : Type w) [Semiring R] (C : Type u) [Category.{v} C] [Preadditive C] where
  homModule : ∀ X Y : C, Module R (X ⟶ Y) := by infer_instance
  smul_comp' : ∀ (X Y Z : C) (r : R) (f : X ⟶ Y) (g : Y ⟶ Z), (r • f) ≫ g = r • f ≫ g := by
    obviously
  comp_smul' : ∀ (X Y Z : C) (f : X ⟶ Y) (r : R) (g : Y ⟶ Z), f ≫ (r • g) = r • f ≫ g := by
    obviously
#align category_theory.linear CategoryTheory.Linear
-/

attribute [instance] linear.hom_module

restate_axiom linear.smul_comp'

restate_axiom linear.comp_smul'

attribute [simp, reassoc.1] linear.smul_comp

attribute [reassoc.1, simp] linear.comp_smul

-- (the linter doesn't like `simp` on the `_assoc` lemma)
end CategoryTheory

open CategoryTheory

namespace CategoryTheory.Linear

variable {C : Type u} [Category.{v} C] [Preadditive C]

#print CategoryTheory.Linear.preadditiveNatLinear /-
instance preadditiveNatLinear : Linear ℕ C
    where
  smul_comp' X Y Z r f g := (Preadditive.rightComp X g).map_nsmul f r
  comp_smul' X Y Z f r g := (Preadditive.leftComp Z f).map_nsmul g r
#align category_theory.linear.preadditive_nat_linear CategoryTheory.Linear.preadditiveNatLinear
-/

/- warning: category_theory.linear.preadditive_int_linear -> CategoryTheory.Linear.preadditiveIntLinear is a dubious translation:
lean 3 declaration is
  forall {C : Type.{u2}} [_inst_1 : CategoryTheory.Category.{u1, u2} C] [_inst_2 : CategoryTheory.Preadditive.{u1, u2} C _inst_1], CategoryTheory.Linear.{0, u1, u2} Int Int.semiring C _inst_1 _inst_2
but is expected to have type
  forall {C : Type.{u2}} [_inst_1 : CategoryTheory.Category.{u1, u2} C] [_inst_2 : CategoryTheory.Preadditive.{u1, u2} C _inst_1], CategoryTheory.Linear.{0, u1, u2} Int Int.instSemiringInt C _inst_1 _inst_2
Case conversion may be inaccurate. Consider using '#align category_theory.linear.preadditive_int_linear CategoryTheory.Linear.preadditiveIntLinearₓ'. -/
instance preadditiveIntLinear : Linear ℤ C
    where
  smul_comp' X Y Z r f g := (Preadditive.rightComp X g).map_zsmul f r
  comp_smul' X Y Z f r g := (Preadditive.leftComp Z f).map_zsmul g r
#align category_theory.linear.preadditive_int_linear CategoryTheory.Linear.preadditiveIntLinear

section End

variable {R : Type w}

instance [Semiring R] [Linear R C] (X : C) : Module R (End X) :=
  by
  dsimp [End]
  infer_instance

instance [CommSemiring R] [Linear R C] (X : C) : Algebra R (End X) :=
  Algebra.ofModule (fun r f g => comp_smul _ _ _ _ _ _) fun r f g => smul_comp _ _ _ _ _ _

end End

section

variable {R : Type w} [Semiring R] [Linear R C]

section InducedCategory

universe u'

variable {C} {D : Type u'} (F : D → C)

#print CategoryTheory.Linear.inducedCategory /-
instance inducedCategory : Linear.{w, v} R (InducedCategory C F)
    where
  homModule X Y := @Linear.homModule R _ C _ _ _ (F X) (F Y)
  smul_comp' P Q R f f' g := smul_comp' _ _ _ _ _ _
  comp_smul' P Q R f g g' := comp_smul' _ _ _ _ _ _
#align category_theory.linear.induced_category CategoryTheory.Linear.inducedCategory
-/

end InducedCategory

/- warning: category_theory.linear.full_subcategory -> CategoryTheory.Linear.fullSubcategory is a dubious translation:
lean 3 declaration is
  forall {C : Type.{u3}} [_inst_1 : CategoryTheory.Category.{u2, u3} C] [_inst_2 : CategoryTheory.Preadditive.{u2, u3} C _inst_1] {R : Type.{u1}} [_inst_3 : Semiring.{u1} R] [_inst_4 : CategoryTheory.Linear.{u1, u2, u3} R _inst_3 C _inst_1 _inst_2] (Z : C -> Prop), CategoryTheory.Linear.{u1, u2, u3} R _inst_3 (CategoryTheory.FullSubcategoryₓ.{u2, u3} C _inst_1 Z) (CategoryTheory.FullSubcategory.category.{u2, u3} C _inst_1 Z) (CategoryTheory.Preadditive.fullSubcategory.{u2, u3} C _inst_1 _inst_2 Z)
but is expected to have type
  forall {C : Type.{u3}} [_inst_1 : CategoryTheory.Category.{u2, u3} C] [_inst_2 : CategoryTheory.Preadditive.{u2, u3} C _inst_1] {R : Type.{u1}} [_inst_3 : Semiring.{u1} R] [_inst_4 : CategoryTheory.Linear.{u1, u2, u3} R _inst_3 C _inst_1 _inst_2] (Z : C -> Prop), CategoryTheory.Linear.{u1, u2, u3} R _inst_3 (CategoryTheory.FullSubcategory.{u3} C Z) (CategoryTheory.FullSubcategory.category.{u2, u3} C _inst_1 Z) (CategoryTheory.Preadditive.fullSubcategory.{u2, u3} C _inst_1 _inst_2 Z)
Case conversion may be inaccurate. Consider using '#align category_theory.linear.full_subcategory CategoryTheory.Linear.fullSubcategoryₓ'. -/
instance fullSubcategory (Z : C → Prop) : Linear.{w, v} R (FullSubcategory Z)
    where
  homModule X Y := @Linear.homModule R _ C _ _ _ X.obj Y.obj
  smul_comp' P Q R f f' g := smul_comp' _ _ _ _ _ _
  comp_smul' P Q R f g g' := comp_smul' _ _ _ _ _ _
#align category_theory.linear.full_subcategory CategoryTheory.Linear.fullSubcategory

variable (R)

#print CategoryTheory.Linear.leftComp /-
/-- Composition by a fixed left argument as an `R`-linear map. -/
@[simps]
def leftComp {X Y : C} (Z : C) (f : X ⟶ Y) : (Y ⟶ Z) →ₗ[R] X ⟶ Z
    where
  toFun g := f ≫ g
  map_add' := by simp
  map_smul' := by simp
#align category_theory.linear.left_comp CategoryTheory.Linear.leftComp
-/

#print CategoryTheory.Linear.rightComp /-
/-- Composition by a fixed right argument as an `R`-linear map. -/
@[simps]
def rightComp (X : C) {Y Z : C} (g : Y ⟶ Z) : (X ⟶ Y) →ₗ[R] X ⟶ Z
    where
  toFun f := f ≫ g
  map_add' := by simp
  map_smul' := by simp
#align category_theory.linear.right_comp CategoryTheory.Linear.rightComp
-/

instance {X Y : C} (f : X ⟶ Y) [Epi f] (r : R) [Invertible r] : Epi (r • f) :=
  ⟨fun R g g' H =>
    by
    rw [smul_comp, smul_comp, ← comp_smul, ← comp_smul, cancel_epi] at H
    simpa [smul_smul] using congr_arg (fun f => ⅟ r • f) H⟩

instance {X Y : C} (f : X ⟶ Y) [Mono f] (r : R) [Invertible r] : Mono (r • f) :=
  ⟨fun R g g' H =>
    by
    rw [comp_smul, comp_smul, ← smul_comp, ← smul_comp, cancel_mono] at H
    simpa [smul_smul] using congr_arg (fun f => ⅟ r • f) H⟩

#print CategoryTheory.Linear.homCongr /-
/-- Given isomorphic objects `X ≅ Y, W ≅ Z` in a `k`-linear category, we have a `k`-linear
isomorphism between `Hom(X, W)` and `Hom(Y, Z).` -/
def homCongr (k : Type _) {C : Type _} [Category C] [Semiring k] [Preadditive C] [Linear k C]
    {X Y W Z : C} (f₁ : X ≅ Y) (f₂ : W ≅ Z) : (X ⟶ W) ≃ₗ[k] Y ⟶ Z :=
  {
    (rightComp k Y f₂.hom).comp
      (leftComp k W
        f₁.symm.hom) with
    invFun := (leftComp k W f₁.hom).comp (rightComp k Y f₂.symm.hom)
    left_inv := fun x => by
      simp only [iso.symm_hom, LinearMap.toFun_eq_coe, LinearMap.coe_comp, Function.comp_apply,
        left_comp_apply, right_comp_apply, category.assoc, iso.hom_inv_id, category.comp_id,
        iso.hom_inv_id_assoc]
    right_inv := fun x => by
      simp only [iso.symm_hom, LinearMap.coe_comp, Function.comp_apply, right_comp_apply,
        left_comp_apply, LinearMap.toFun_eq_coe, iso.inv_hom_id_assoc, category.assoc,
        iso.inv_hom_id, category.comp_id] }
#align category_theory.linear.hom_congr CategoryTheory.Linear.homCongr
-/

/- warning: category_theory.linear.hom_congr_apply -> CategoryTheory.Linear.homCongr_apply is a dubious translation:
lean 3 declaration is
  forall (k : Type.{u1}) {C : Type.{u2}} [_inst_5 : CategoryTheory.Category.{u3, u2} C] [_inst_6 : Semiring.{u1} k] [_inst_7 : CategoryTheory.Preadditive.{u3, u2} C _inst_5] [_inst_8 : CategoryTheory.Linear.{u1, u3, u2} k _inst_6 C _inst_5 _inst_7] {X : C} {Y : C} {W : C} {Z : C} (f₁ : CategoryTheory.Iso.{u3, u2} C _inst_5 X Y) (f₂ : CategoryTheory.Iso.{u3, u2} C _inst_5 W Z) (f : Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) X W), Eq.{succ u3} (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) Y Z) (coeFn.{succ u3, succ u3} (LinearEquiv.{u1, u1, u3, u3} k k _inst_6 _inst_6 (RingHom.id.{u1} k (Semiring.toNonAssocSemiring.{u1} k _inst_6)) (RingHom.id.{u1} k (Semiring.toNonAssocSemiring.{u1} k _inst_6)) (RingHomInvPair.ids.{u1} k _inst_6) (RingHomInvPair.ids.{u1} k _inst_6) (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) X W) (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) Y Z) (AddCommGroup.toAddCommMonoid.{u3} (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u3, u2} C _inst_5 _inst_7 X W)) (AddCommGroup.toAddCommMonoid.{u3} (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u3, u2} C _inst_5 _inst_7 Y Z)) (CategoryTheory.Linear.homModule.{u1, u3, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 X W) (CategoryTheory.Linear.homModule.{u1, u3, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 Y Z)) (fun (_x : LinearEquiv.{u1, u1, u3, u3} k k _inst_6 _inst_6 (RingHom.id.{u1} k (Semiring.toNonAssocSemiring.{u1} k _inst_6)) (RingHom.id.{u1} k (Semiring.toNonAssocSemiring.{u1} k _inst_6)) (RingHomInvPair.ids.{u1} k _inst_6) (RingHomInvPair.ids.{u1} k _inst_6) (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) X W) (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) Y Z) (AddCommGroup.toAddCommMonoid.{u3} (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u3, u2} C _inst_5 _inst_7 X W)) (AddCommGroup.toAddCommMonoid.{u3} (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u3, u2} C _inst_5 _inst_7 Y Z)) (CategoryTheory.Linear.homModule.{u1, u3, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 X W) (CategoryTheory.Linear.homModule.{u1, u3, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 Y Z)) => (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) X W) -> (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) Y Z)) (LinearEquiv.hasCoeToFun.{u1, u1, u3, u3} k k (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) X W) (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) Y Z) _inst_6 _inst_6 (AddCommGroup.toAddCommMonoid.{u3} (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u3, u2} C _inst_5 _inst_7 X W)) (AddCommGroup.toAddCommMonoid.{u3} (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u3, u2} C _inst_5 _inst_7 Y Z)) (CategoryTheory.Linear.homModule.{u1, u3, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 X W) (CategoryTheory.Linear.homModule.{u1, u3, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 Y Z) (RingHom.id.{u1} k (Semiring.toNonAssocSemiring.{u1} k _inst_6)) (RingHom.id.{u1} k (Semiring.toNonAssocSemiring.{u1} k _inst_6)) (RingHomInvPair.ids.{u1} k _inst_6) (RingHomInvPair.ids.{u1} k _inst_6)) (CategoryTheory.Linear.homCongr.{u1, u2, u3} k C _inst_5 _inst_6 _inst_7 _inst_8 X Y W Z f₁ f₂) f) (CategoryTheory.CategoryStruct.comp.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5) Y W Z (CategoryTheory.CategoryStruct.comp.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5) Y X W (CategoryTheory.Iso.inv.{u3, u2} C _inst_5 X Y f₁) f) (CategoryTheory.Iso.hom.{u3, u2} C _inst_5 W Z f₂))
but is expected to have type
  forall (k : Type.{u3}) {C : Type.{u2}} [_inst_5 : CategoryTheory.Category.{u1, u2} C] [_inst_6 : Semiring.{u3} k] [_inst_7 : CategoryTheory.Preadditive.{u1, u2} C _inst_5] [_inst_8 : CategoryTheory.Linear.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7] {X : C} {Y : C} {W : C} {Z : C} (f₁ : CategoryTheory.Iso.{u1, u2} C _inst_5 X Y) (f₂ : CategoryTheory.Iso.{u1, u2} C _inst_5 W Z) (f : Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W), Eq.{succ u1} ((fun (x._@.Mathlib.Algebra.Hom.GroupAction._hyg.2186 : Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) => Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) f) (FunLike.coe.{succ u1, succ u1, succ u1} (LinearEquiv.{u3, u3, u1, u1} k k _inst_6 _inst_6 (RingHom.id.{u3} k (Semiring.toNonAssocSemiring.{u3} k _inst_6)) (RingHom.id.{u3} k (Semiring.toNonAssocSemiring.{u3} k _inst_6)) (RingHomInvPair.ids.{u3} k _inst_6) (RingHomInvPair.ids.{u3} k _inst_6) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 X W)) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 Y Z)) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 X W) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 Y Z)) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (fun (_x : Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) => (fun (x._@.Mathlib.Algebra.Hom.GroupAction._hyg.2186 : Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) => Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) _x) (SMulHomClass.toFunLike.{u1, u3, u1, u1} (LinearEquiv.{u3, u3, u1, u1} k k _inst_6 _inst_6 (RingHom.id.{u3} k (Semiring.toNonAssocSemiring.{u3} k _inst_6)) (RingHom.id.{u3} k (Semiring.toNonAssocSemiring.{u3} k _inst_6)) (RingHomInvPair.ids.{u3} k _inst_6) (RingHomInvPair.ids.{u3} k _inst_6) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 X W)) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 Y Z)) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 X W) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 Y Z)) k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (SMulZeroClass.toSMul.{u3, u1} k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (AddMonoid.toZero.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (AddCommMonoid.toAddMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 X W)))) (DistribSMul.toSMulZeroClass.{u3, u1} k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (AddMonoid.toAddZeroClass.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (AddCommMonoid.toAddMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 X W)))) (DistribMulAction.toDistribSMul.{u3, u1} k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (MonoidWithZero.toMonoid.{u3} k (Semiring.toMonoidWithZero.{u3} k _inst_6)) (AddCommMonoid.toAddMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 X W))) (Module.toDistribMulAction.{u3, u1} k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) _inst_6 (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 X W)) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 X W))))) (SMulZeroClass.toSMul.{u3, u1} k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (AddMonoid.toZero.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (AddCommMonoid.toAddMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 Y Z)))) (DistribSMul.toSMulZeroClass.{u3, u1} k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (AddMonoid.toAddZeroClass.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (AddCommMonoid.toAddMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 Y Z)))) (DistribMulAction.toDistribSMul.{u3, u1} k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (MonoidWithZero.toMonoid.{u3} k (Semiring.toMonoidWithZero.{u3} k _inst_6)) (AddCommMonoid.toAddMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 Y Z))) (Module.toDistribMulAction.{u3, u1} k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) _inst_6 (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 Y Z)) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 Y Z))))) (DistribMulActionHomClass.toSMulHomClass.{u1, u3, u1, u1} (LinearEquiv.{u3, u3, u1, u1} k k _inst_6 _inst_6 (RingHom.id.{u3} k (Semiring.toNonAssocSemiring.{u3} k _inst_6)) (RingHom.id.{u3} k (Semiring.toNonAssocSemiring.{u3} k _inst_6)) (RingHomInvPair.ids.{u3} k _inst_6) (RingHomInvPair.ids.{u3} k _inst_6) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 X W)) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 Y Z)) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 X W) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 Y Z)) k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (MonoidWithZero.toMonoid.{u3} k (Semiring.toMonoidWithZero.{u3} k _inst_6)) (AddCommMonoid.toAddMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 X W))) (AddCommMonoid.toAddMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 Y Z))) (Module.toDistribMulAction.{u3, u1} k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) _inst_6 (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 X W)) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 X W)) (Module.toDistribMulAction.{u3, u1} k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) _inst_6 (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 Y Z)) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 Y Z)) (SemilinearMapClass.distribMulActionHomClass.{u3, u1, u1, u1} k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (LinearEquiv.{u3, u3, u1, u1} k k _inst_6 _inst_6 (RingHom.id.{u3} k (Semiring.toNonAssocSemiring.{u3} k _inst_6)) (RingHom.id.{u3} k (Semiring.toNonAssocSemiring.{u3} k _inst_6)) (RingHomInvPair.ids.{u3} k _inst_6) (RingHomInvPair.ids.{u3} k _inst_6) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 X W)) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 Y Z)) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 X W) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 Y Z)) _inst_6 (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 X W)) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 Y Z)) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 X W) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 Y Z) (SemilinearEquivClass.instSemilinearMapClass.{u3, u3, u1, u1, u1} k k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (LinearEquiv.{u3, u3, u1, u1} k k _inst_6 _inst_6 (RingHom.id.{u3} k (Semiring.toNonAssocSemiring.{u3} k _inst_6)) (RingHom.id.{u3} k (Semiring.toNonAssocSemiring.{u3} k _inst_6)) (RingHomInvPair.ids.{u3} k _inst_6) (RingHomInvPair.ids.{u3} k _inst_6) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 X W)) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 Y Z)) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 X W) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 Y Z)) _inst_6 _inst_6 (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 X W)) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 Y Z)) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 X W) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 Y Z) (RingHom.id.{u3} k (Semiring.toNonAssocSemiring.{u3} k _inst_6)) (RingHom.id.{u3} k (Semiring.toNonAssocSemiring.{u3} k _inst_6)) (RingHomInvPair.ids.{u3} k _inst_6) (RingHomInvPair.ids.{u3} k _inst_6) (LinearEquiv.instSemilinearEquivClassLinearEquiv.{u3, u3, u1, u1} k k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) _inst_6 _inst_6 (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 X W)) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 Y Z)) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 X W) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 Y Z) (RingHom.id.{u3} k (Semiring.toNonAssocSemiring.{u3} k _inst_6)) (RingHom.id.{u3} k (Semiring.toNonAssocSemiring.{u3} k _inst_6)) (RingHomInvPair.ids.{u3} k _inst_6) (RingHomInvPair.ids.{u3} k _inst_6)))))) (CategoryTheory.Linear.homCongr.{u3, u2, u1} k C _inst_5 _inst_6 _inst_7 _inst_8 X Y W Z f₁ f₂) f) (CategoryTheory.CategoryStruct.comp.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5) Y W Z (CategoryTheory.CategoryStruct.comp.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5) Y X W (CategoryTheory.Iso.inv.{u1, u2} C _inst_5 X Y f₁) f) (CategoryTheory.Iso.hom.{u1, u2} C _inst_5 W Z f₂))
Case conversion may be inaccurate. Consider using '#align category_theory.linear.hom_congr_apply CategoryTheory.Linear.homCongr_applyₓ'. -/
theorem homCongr_apply (k : Type _) {C : Type _} [Category C] [Semiring k] [Preadditive C]
    [Linear k C] {X Y W Z : C} (f₁ : X ≅ Y) (f₂ : W ≅ Z) (f : X ⟶ W) :
    homCongr k f₁ f₂ f = (f₁.inv ≫ f) ≫ f₂.hom :=
  rfl
#align category_theory.linear.hom_congr_apply CategoryTheory.Linear.homCongr_apply

/- warning: category_theory.linear.hom_congr_symm_apply -> CategoryTheory.Linear.homCongr_symm_apply is a dubious translation:
lean 3 declaration is
  forall (k : Type.{u1}) {C : Type.{u2}} [_inst_5 : CategoryTheory.Category.{u3, u2} C] [_inst_6 : Semiring.{u1} k] [_inst_7 : CategoryTheory.Preadditive.{u3, u2} C _inst_5] [_inst_8 : CategoryTheory.Linear.{u1, u3, u2} k _inst_6 C _inst_5 _inst_7] {X : C} {Y : C} {W : C} {Z : C} (f₁ : CategoryTheory.Iso.{u3, u2} C _inst_5 X Y) (f₂ : CategoryTheory.Iso.{u3, u2} C _inst_5 W Z) (f : Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) Y Z), Eq.{succ u3} (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) X W) (coeFn.{succ u3, succ u3} (LinearEquiv.{u1, u1, u3, u3} k k _inst_6 _inst_6 (RingHom.id.{u1} k (Semiring.toNonAssocSemiring.{u1} k _inst_6)) (RingHom.id.{u1} k (Semiring.toNonAssocSemiring.{u1} k _inst_6)) (RingHomInvPair.ids.{u1} k _inst_6) (RingHomInvPair.ids.{u1} k _inst_6) (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) Y Z) (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) X W) (AddCommGroup.toAddCommMonoid.{u3} (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u3, u2} C _inst_5 _inst_7 Y Z)) (AddCommGroup.toAddCommMonoid.{u3} (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u3, u2} C _inst_5 _inst_7 X W)) (CategoryTheory.Linear.homModule.{u1, u3, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 Y Z) (CategoryTheory.Linear.homModule.{u1, u3, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 X W)) (fun (_x : LinearEquiv.{u1, u1, u3, u3} k k _inst_6 _inst_6 (RingHom.id.{u1} k (Semiring.toNonAssocSemiring.{u1} k _inst_6)) (RingHom.id.{u1} k (Semiring.toNonAssocSemiring.{u1} k _inst_6)) (RingHomInvPair.ids.{u1} k _inst_6) (RingHomInvPair.ids.{u1} k _inst_6) (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) Y Z) (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) X W) (AddCommGroup.toAddCommMonoid.{u3} (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u3, u2} C _inst_5 _inst_7 Y Z)) (AddCommGroup.toAddCommMonoid.{u3} (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u3, u2} C _inst_5 _inst_7 X W)) (CategoryTheory.Linear.homModule.{u1, u3, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 Y Z) (CategoryTheory.Linear.homModule.{u1, u3, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 X W)) => (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) Y Z) -> (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) X W)) (LinearEquiv.hasCoeToFun.{u1, u1, u3, u3} k k (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) Y Z) (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) X W) _inst_6 _inst_6 (AddCommGroup.toAddCommMonoid.{u3} (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u3, u2} C _inst_5 _inst_7 Y Z)) (AddCommGroup.toAddCommMonoid.{u3} (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u3, u2} C _inst_5 _inst_7 X W)) (CategoryTheory.Linear.homModule.{u1, u3, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 Y Z) (CategoryTheory.Linear.homModule.{u1, u3, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 X W) (RingHom.id.{u1} k (Semiring.toNonAssocSemiring.{u1} k _inst_6)) (RingHom.id.{u1} k (Semiring.toNonAssocSemiring.{u1} k _inst_6)) (RingHomInvPair.ids.{u1} k _inst_6) (RingHomInvPair.ids.{u1} k _inst_6)) (LinearEquiv.symm.{u1, u1, u3, u3} k k (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) X W) (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) Y Z) _inst_6 _inst_6 (AddCommGroup.toAddCommMonoid.{u3} (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u3, u2} C _inst_5 _inst_7 X W)) (AddCommGroup.toAddCommMonoid.{u3} (Quiver.Hom.{succ u3, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u3, u2} C _inst_5 _inst_7 Y Z)) (CategoryTheory.Linear.homModule.{u1, u3, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 X W) (CategoryTheory.Linear.homModule.{u1, u3, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 Y Z) (RingHom.id.{u1} k (Semiring.toNonAssocSemiring.{u1} k _inst_6)) (RingHom.id.{u1} k (Semiring.toNonAssocSemiring.{u1} k _inst_6)) (RingHomInvPair.ids.{u1} k _inst_6) (RingHomInvPair.ids.{u1} k _inst_6) (CategoryTheory.Linear.homCongr.{u1, u2, u3} k C _inst_5 _inst_6 _inst_7 _inst_8 X Y W Z f₁ f₂)) f) (CategoryTheory.CategoryStruct.comp.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5) X Y W (CategoryTheory.Iso.hom.{u3, u2} C _inst_5 X Y f₁) (CategoryTheory.CategoryStruct.comp.{u3, u2} C (CategoryTheory.Category.toCategoryStruct.{u3, u2} C _inst_5) Y Z W f (CategoryTheory.Iso.inv.{u3, u2} C _inst_5 W Z f₂)))
but is expected to have type
  forall (k : Type.{u3}) {C : Type.{u2}} [_inst_5 : CategoryTheory.Category.{u1, u2} C] [_inst_6 : Semiring.{u3} k] [_inst_7 : CategoryTheory.Preadditive.{u1, u2} C _inst_5] [_inst_8 : CategoryTheory.Linear.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7] {X : C} {Y : C} {W : C} {Z : C} (f₁ : CategoryTheory.Iso.{u1, u2} C _inst_5 X Y) (f₂ : CategoryTheory.Iso.{u1, u2} C _inst_5 W Z) (f : Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z), Eq.{succ u1} ((fun (x._@.Mathlib.Algebra.Hom.GroupAction._hyg.2186 : Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) => Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) f) (FunLike.coe.{succ u1, succ u1, succ u1} (LinearEquiv.{u3, u3, u1, u1} k k _inst_6 _inst_6 (RingHom.id.{u3} k (Semiring.toNonAssocSemiring.{u3} k _inst_6)) (RingHom.id.{u3} k (Semiring.toNonAssocSemiring.{u3} k _inst_6)) (RingHomInvPair.ids.{u3} k _inst_6) (RingHomInvPair.ids.{u3} k _inst_6) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 Y Z)) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 X W)) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 Y Z) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 X W)) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (fun (_x : Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) => (fun (x._@.Mathlib.Algebra.Hom.GroupAction._hyg.2186 : Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) => Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) _x) (SMulHomClass.toFunLike.{u1, u3, u1, u1} (LinearEquiv.{u3, u3, u1, u1} k k _inst_6 _inst_6 (RingHom.id.{u3} k (Semiring.toNonAssocSemiring.{u3} k _inst_6)) (RingHom.id.{u3} k (Semiring.toNonAssocSemiring.{u3} k _inst_6)) (RingHomInvPair.ids.{u3} k _inst_6) (RingHomInvPair.ids.{u3} k _inst_6) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 Y Z)) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 X W)) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 Y Z) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 X W)) k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (SMulZeroClass.toSMul.{u3, u1} k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (AddMonoid.toZero.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (AddCommMonoid.toAddMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 Y Z)))) (DistribSMul.toSMulZeroClass.{u3, u1} k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (AddMonoid.toAddZeroClass.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (AddCommMonoid.toAddMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 Y Z)))) (DistribMulAction.toDistribSMul.{u3, u1} k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (MonoidWithZero.toMonoid.{u3} k (Semiring.toMonoidWithZero.{u3} k _inst_6)) (AddCommMonoid.toAddMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 Y Z))) (Module.toDistribMulAction.{u3, u1} k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) _inst_6 (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 Y Z)) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 Y Z))))) (SMulZeroClass.toSMul.{u3, u1} k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (AddMonoid.toZero.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (AddCommMonoid.toAddMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 X W)))) (DistribSMul.toSMulZeroClass.{u3, u1} k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (AddMonoid.toAddZeroClass.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (AddCommMonoid.toAddMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 X W)))) (DistribMulAction.toDistribSMul.{u3, u1} k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (MonoidWithZero.toMonoid.{u3} k (Semiring.toMonoidWithZero.{u3} k _inst_6)) (AddCommMonoid.toAddMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 X W))) (Module.toDistribMulAction.{u3, u1} k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) _inst_6 (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 X W)) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 X W))))) (DistribMulActionHomClass.toSMulHomClass.{u1, u3, u1, u1} (LinearEquiv.{u3, u3, u1, u1} k k _inst_6 _inst_6 (RingHom.id.{u3} k (Semiring.toNonAssocSemiring.{u3} k _inst_6)) (RingHom.id.{u3} k (Semiring.toNonAssocSemiring.{u3} k _inst_6)) (RingHomInvPair.ids.{u3} k _inst_6) (RingHomInvPair.ids.{u3} k _inst_6) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 Y Z)) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 X W)) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 Y Z) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 X W)) k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (MonoidWithZero.toMonoid.{u3} k (Semiring.toMonoidWithZero.{u3} k _inst_6)) (AddCommMonoid.toAddMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 Y Z))) (AddCommMonoid.toAddMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 X W))) (Module.toDistribMulAction.{u3, u1} k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) _inst_6 (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 Y Z)) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 Y Z)) (Module.toDistribMulAction.{u3, u1} k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) _inst_6 (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 X W)) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 X W)) (SemilinearMapClass.distribMulActionHomClass.{u3, u1, u1, u1} k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (LinearEquiv.{u3, u3, u1, u1} k k _inst_6 _inst_6 (RingHom.id.{u3} k (Semiring.toNonAssocSemiring.{u3} k _inst_6)) (RingHom.id.{u3} k (Semiring.toNonAssocSemiring.{u3} k _inst_6)) (RingHomInvPair.ids.{u3} k _inst_6) (RingHomInvPair.ids.{u3} k _inst_6) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 Y Z)) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 X W)) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 Y Z) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 X W)) _inst_6 (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 Y Z)) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 X W)) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 Y Z) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 X W) (SemilinearEquivClass.instSemilinearMapClass.{u3, u3, u1, u1, u1} k k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (LinearEquiv.{u3, u3, u1, u1} k k _inst_6 _inst_6 (RingHom.id.{u3} k (Semiring.toNonAssocSemiring.{u3} k _inst_6)) (RingHom.id.{u3} k (Semiring.toNonAssocSemiring.{u3} k _inst_6)) (RingHomInvPair.ids.{u3} k _inst_6) (RingHomInvPair.ids.{u3} k _inst_6) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 Y Z)) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 X W)) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 Y Z) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 X W)) _inst_6 _inst_6 (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 Y Z)) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 X W)) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 Y Z) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 X W) (RingHom.id.{u3} k (Semiring.toNonAssocSemiring.{u3} k _inst_6)) (RingHom.id.{u3} k (Semiring.toNonAssocSemiring.{u3} k _inst_6)) (RingHomInvPair.ids.{u3} k _inst_6) (RingHomInvPair.ids.{u3} k _inst_6) (LinearEquiv.instSemilinearEquivClassLinearEquiv.{u3, u3, u1, u1} k k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) _inst_6 _inst_6 (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 Y Z)) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 X W)) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 Y Z) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 X W) (RingHom.id.{u3} k (Semiring.toNonAssocSemiring.{u3} k _inst_6)) (RingHom.id.{u3} k (Semiring.toNonAssocSemiring.{u3} k _inst_6)) (RingHomInvPair.ids.{u3} k _inst_6) (RingHomInvPair.ids.{u3} k _inst_6)))))) (LinearEquiv.symm.{u3, u3, u1, u1} k k (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) _inst_6 _inst_6 (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) X W) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 X W)) (AddCommGroup.toAddCommMonoid.{u1} (Quiver.Hom.{succ u1, u2} C (CategoryTheory.CategoryStruct.toQuiver.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5)) Y Z) (CategoryTheory.Preadditive.homGroup.{u1, u2} C _inst_5 _inst_7 Y Z)) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 X W) (CategoryTheory.Linear.homModule.{u3, u1, u2} k _inst_6 C _inst_5 _inst_7 _inst_8 Y Z) (RingHom.id.{u3} k (Semiring.toNonAssocSemiring.{u3} k _inst_6)) (RingHom.id.{u3} k (Semiring.toNonAssocSemiring.{u3} k _inst_6)) (RingHomInvPair.ids.{u3} k _inst_6) (RingHomInvPair.ids.{u3} k _inst_6) (CategoryTheory.Linear.homCongr.{u3, u2, u1} k C _inst_5 _inst_6 _inst_7 _inst_8 X Y W Z f₁ f₂)) f) (CategoryTheory.CategoryStruct.comp.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5) X Y W (CategoryTheory.Iso.hom.{u1, u2} C _inst_5 X Y f₁) (CategoryTheory.CategoryStruct.comp.{u1, u2} C (CategoryTheory.Category.toCategoryStruct.{u1, u2} C _inst_5) Y Z W f (CategoryTheory.Iso.inv.{u1, u2} C _inst_5 W Z f₂)))
Case conversion may be inaccurate. Consider using '#align category_theory.linear.hom_congr_symm_apply CategoryTheory.Linear.homCongr_symm_applyₓ'. -/
theorem homCongr_symm_apply (k : Type _) {C : Type _} [Category C] [Semiring k] [Preadditive C]
    [Linear k C] {X Y W Z : C} (f₁ : X ≅ Y) (f₂ : W ≅ Z) (f : Y ⟶ Z) :
    (homCongr k f₁ f₂).symm f = f₁.hom ≫ f ≫ f₂.inv :=
  rfl
#align category_theory.linear.hom_congr_symm_apply CategoryTheory.Linear.homCongr_symm_apply

end

section

variable {S : Type w} [CommSemiring S] [Linear S C]

#print CategoryTheory.Linear.comp /-
/-- Composition as a bilinear map. -/
@[simps]
def comp (X Y Z : C) : (X ⟶ Y) →ₗ[S] (Y ⟶ Z) →ₗ[S] X ⟶ Z
    where
  toFun f := leftComp S Z f
  map_add' := by
    intros
    ext
    simp
  map_smul' := by
    intros
    ext
    simp
#align category_theory.linear.comp CategoryTheory.Linear.comp
-/

end

end CategoryTheory.Linear


text:
example (P Q : Prop) (p : P) (h : P → Q) : Q :=
begin
exact h p,
end

author: nicholaspun

repo: natural-number-game-solutions


text:
structure Foo where
  x : Nat
  h : x > 1

theorem foo_gt_0 (foo : Foo) : foo.x > 0 :=
  Nat.lt_of_succ_lt foo.h

example (x : Nat) (h : x > 1) : id { x, h : Foo }.x > 0 :=
  foo_gt_0 { x, h }

example (x : Nat) (h : x > 1) : id { x, h : Foo }.x > 0 :=
  foo_gt_0 _

author: leanprover


text:
-- Mostly lemmas about arithmetic?
import data.rat

lemma add_neg_le_r {A} [linear_ordered_comm_ring A] (x y : A)
  : x + y ≥ 0 ↔ x ≥ - y
:= begin
dsimp [ge],
split; intros H,
{ apply (@le_of_add_le_add_left _ _ y),
  rw add_comm y,
  rw neg_add_self, rw add_comm, assumption, },
{ apply @le_of_add_le_add_left _ _ (-y),
  rw add_zero, rw add_comm, rw add_assoc,
  rw add_comm y, rw neg_add_self,
  rw add_zero, assumption,
}
end

lemma add_neg_le_l {A} [linear_ordered_comm_ring A] (x y : A)
  : x + y ≤ 0 ↔ x ≤ - y
:= begin
split; intros H,
{ apply (@le_of_add_le_add_left _ _ y),
  rw add_comm _ (-y),
  rw neg_add_self, rw add_comm, assumption, },
{ apply @le_of_add_le_add_left _ _ (-y),
  rw add_zero, rw add_comm, rw add_assoc,
  rw add_comm y, rw neg_add_self,
  rw add_zero, assumption,
}
end

lemma add_le_zero1 {A} [linear_ordered_comm_ring A] (x y : A)
  : 0 ≤ y - x ↔ x ≤ y
:= begin
split; intros H,
{ rw ← (add_zero x), apply le_trans,
  apply add_le_add_left, assumption,
  rw ← add_sub_assoc, rw add_comm,
  rw add_sub_cancel, },
{ apply le_trans, tactic.swap, apply add_le_add_right,
  assumption, rw add_comm, rw neg_add_self }
end

lemma mul_le_zero_pos (c x : ℚ) (Hc : 0 < c)
  : x ≤ 0 ↔ c * x ≤ 0
:= begin
split; intros H,
{ apply mul_nonpos_of_nonneg_of_nonpos,
  apply le_of_lt, assumption, assumption, },
{ apply nonpos_of_mul_nonpos_left; assumption, }
end

lemma lt_zero_neg (c : ℚ)
  : c < 0 ↔ - c > 0
:= begin
split; intros H,
{ rw ← neg_zero,
  apply neg_lt_neg _, assumption, },
{ rw ← neg_zero,
  rw ← (neg_neg c),
  apply neg_lt_neg _, assumption }
end

lemma mul_le_zero_neg (c x : ℚ) (Hc : c < 0)
  : x ≤ 0 ↔ c * x ≥ 0
:= begin
split; intros H,
{ apply mul_nonneg_of_nonpos_of_nonpos,
  apply le_of_lt, assumption, assumption, },
{ apply nonpos_of_mul_nonpos_left, tactic.swap,
  rw lt_zero_neg at Hc, apply Hc,
  rw ← neg_mul_eq_neg_mul,
  apply neg_le_of_neg_le, rw neg_zero, assumption,
 }
end

lemma mul_le_zero_neg_le (c x : ℚ) (Hc : c < 0)
  : x ≤ 0 ↔ 0 ≤ c * x
:= mul_le_zero_neg c x Hc

lemma neg_le_neg_opp (x y : ℚ)
  : - y ≤ - x → x ≤ y
:= begin
intros H, rw ← (neg_neg x), rw ← (neg_neg y),
apply neg_le_neg, assumption,
end

lemma add_zero_l (n : ℚ) : 0 + n = n
:= by simp

lemma add_le_zero2 (x y : ℚ)
  : x - y ≤ 0 ↔ x ≤ y
:= begin
rw ← add_le_zero1,
rw sub_eq_add_neg,
rw neg_sub, rw add_zero_l,
rw add_le_zero1,
end

lemma mul_le_mono_neg (c x y : ℚ) (Hc : c < 0)
  (H : x ≤ y) : c * y ≤ c * x
:= begin
rw ← add_le_zero1, rw ← mul_sub,
rw ← mul_le_zero_neg_le, rw add_le_zero2, assumption,
assumption,
end

lemma mul_le_mono_pos (c x y : ℚ) (Hc : c > 0)
  (H : x ≤ y) : c * x ≤ c * y
:= begin
rw ← add_le_zero1, rw ← mul_sub,
apply mul_nonneg, apply le_of_lt, assumption,
unfold ge, rw add_le_zero1, assumption,
end

lemma gt_of_not_eq_lt
  {x : ℚ}
  (Heq : x ≠ 0) (Hlt : ¬ x < 0)
  : x > 0
:= begin
unfold gt,
rw lt_iff_not_ge,
intros contra,
apply Hlt,
intros contra, apply Heq,
rw le_antisymm_iff, split; assumption,
end

lemma rat.inv_pos (x : ℚ) (Hx : 0 < x) : 0 < x⁻¹
:= begin
have H : 0 < x * x⁻¹,
rw mul_inv_cancel, exact_dec_trivial,
apply ne_of_gt, assumption,
have H' := pos_and_pos_or_neg_and_neg_of_mul_pos H,
induction H' with H' H'; induction H' with H1 H2, assumption,
exfalso, clear H H2,
rw lt_iff_not_ge at Hx, apply Hx,
apply le_of_lt, assumption,
end

author: GaloisInc

repo: lean-protocol-support