mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
⊢ max ℵ₀ #K ≤ Module.rank K (ℕ → K)

Tactic:
by
  have aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K) := (rank_finsupp_self K ℕ).symm.trans_le
    (Finsupp.lcoeFun.rank_le_of_injective <| by exact DFunLike.coe_injective)
  refine max_le aleph0_le ?_
  obtain card_K | card_K := le_or_gt #K ℵ₀
  · exact card_K.trans aleph0_le
  by_contra!
  obtain ⟨⟨ιK, bK⟩⟩ := Module.Free.exists_basis (R := K) (M := ℕ → K)
  let L := Subfield.closure (Set.range (fun i : ιK × ℕ ↦ bK i.1 i.2))
  have hLK : #L < #K := by
    refine (Subfield.cardinalMk_closure_le_max _).trans_lt
      (max_lt_iff.mpr ⟨mk_range_le.trans_lt ?_, card_K⟩)
    rwa [mk_prod, ← aleph0, lift_uzero, bK.mk_eq_rank'', mul_aleph0_eq aleph0_le]
  let := Module.compHom K (RingHom.op L.subtype)
  obtain ⟨⟨ιL, bL⟩⟩ := Module.Free.exists_basis (R := Lᵐᵒᵖ) (M := K)
  have card_ιL : ℵ₀ ≤ #ιL := by
    contrapose! hLK
    have := @Fintype.ofFinite _ (lt_aleph0_iff_finite.mp hLK)
    rw [bL.repr.toEquiv.cardinal_eq, mk_finsupp_of_fintype,
        ← MulOpposite.opEquiv.cardinal_eq] at card_K ⊢
    apply power_nat_le
    contrapose! card_K
    exact (power_lt_aleph0 card_K natCast_lt_aleph0).le
  obtain ⟨e⟩ := lift_mk_le'.mp (card_ιL.trans_eq (lift_uzero #ιL).symm)
  have rep_e := bK.linearCombination_repr (bL ∘ e)
  rw [Finsupp.linearCombination_apply, Finsupp.sum] at rep_e
  set c := bK.repr (bL ∘ e)
  set s := c.support
  let f i (j : s) : L := ⟨bK j i, Subfield.subset_closure ⟨(j, i), rfl⟩⟩
  have : ¬LinearIndependent Lᵐᵒᵖ f := fun h ↦ by
    have := h.cardinal_lift_le_rank
    rw [lift_uzero, (LinearEquiv.piCongrRight fun _ ↦ MulOpposite.opLinearEquiv Lᵐᵒᵖ).rank_eq,
        rank_fun'] at this
    exact natCast_lt_aleph0.not_ge this
  obtain ⟨t, g, eq0, i, hi, hgi⟩ := not_linearIndependent_iff.mp this
  refine hgi (linearIndependent_iff'.mp (bL.linearIndependent.comp e e.injective) t g ?_ i hi)
  clear_value c s
  simp_rw [← rep_e, Finset.sum_apply, Pi.smul_apply, Finset.smul_sum]
  rw [Finset.sum_comm]
  refine Finset.sum_eq_zero fun i hi ↦ ?_
  replace eq0 := congr_arg L.subtype (congr_fun eq0 ⟨i, hi⟩)
  rw [Finset.sum_apply, map_sum] at eq0
  have : SMulCommClass Lᵐᵒᵖ K K := ⟨fun _ _ _ ↦ mul_assoc _ _ _⟩
  simp_rw [smul_comm _ (c i), ← Finset.smul_sum]
  erw [eq0, smul_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this✝ : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
this : Infinite ιK
⊢ Module.rank K (ι → K) = max (#ιK) (lift.{v, u} #K)

Tactic:
bK.mk_eq_rank'',

Goal state after:
K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this✝ : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
this : Infinite ιK
⊢ Module.rank K (ι → K) = max (Module.rank K (ι → K)) (lift.{v, u} #K)
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s t : Submodule K V
inst✝¹ : FiniteDimensional K ↥s
inst✝ : FiniteDimensional K ↥t
⊢ finrank K ↥(s ⊔ t) ≤ finrank K ↥s + finrank K ↥t

Tactic:
rw [← finrank_sup_add_finrank_inf_eq]
  exact self_le_add_right _ _

Goal state after:
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s t : Submodule K V
inst✝ : FiniteDimensional K ↥t
hst : s < t
⊢ comap t.subtype s ≠ ⊤

Tactic:
simp [not_le_of_gt hst]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix

Goal state before:
pp: case e'_4
K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
this : Nontrivial K
⊢ lift.{v, u_2} (Module.rank K M) = Module.rank L (M →ₗ[K] L)

Tactic:
Module.rank_linearMap_self

Goal state after:
case e'_4
K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
this : Nontrivial K
⊢ lift.{v, u_2} (Module.rank K M) = lift.{v, u_2} (Module.rank K M)
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), (B (v i)) (v i) ≠ 0
s : Finset n
w : n → K₁
⊢ ∑ i ∈ s, w i • v i = 0 → ∀ i ∈ s, w i = 0

Tactic:
hs

Goal state after:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), (B (v i)) (v i) ≠ 0
s : Finset n
w : n → K₁
hs : ∑ i ∈ s, w i • v i = 0
⊢ ∀ i ∈ s, w i = 0
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module.Finite R M
inst✝ : Projective R M
⊢ Function.Bijective ⇑(dualTensorHom R M N)

Tactic:
obtain ⟨n, f, g, -, -, eq⟩ := Finite.exists_comp_eq_id_of_projective R M
  constructor
  · refine .of_comp (f := f.lcomp R N) ?_
    rw [← coe_comp, ← dualTensorHom_comp_rTensor_dualMap, coe_comp,
      ← coe_dualTensorHomEquivOfBasis (Pi.basisFun ..)]
    refine (EquivLike.injective _).comp (injective_of_comp_eq_id _ (rTensor _ g.dualMap) ?_)
    simp [← rTensor_comp, dualMap_comp_dualMap g f, eq]
  · refine .of_comp (g := g.dualMap.rTensor N) ?_
    rw [← coe_comp, dualTensorHom_comp_rTensor_dualMap, coe_comp,
      ← coe_dualTensorHomEquivOfBasis (Pi.basisFun ..)]
    refine (surjective_of_comp_eq_id (f.lcomp R N) _ ?_).comp (EquivLike.surjective _)
    ext φ; exact congr(φ ($eq _))

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite ι
b : Basis ι R M
⊢ Module.rank R (Dual R M) = lift.{uR, uM} (Module.rank R M)

Tactic:
classical rw [← lift_umax.{uM, uR}, b.toDualEquiv.lift_rank_eq, lift_id'.{uM, uR}]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
x : M
hx : x ∉ p
hp' : Projective R (M ⧸ p)
this : ∃ f, f (p.mkQ x) ≠ 0
⊢ ∃ f, f x ≠ 0 ∧ map f p = ⊥

Tactic:
obtain ⟨f, hf⟩ := this; exact ⟨f.comp p.mkQ, hf, by simp [Submodule.map_comp]⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝² : HasCoequalizer f g
inst✝¹ : HasCoequalizer (G.map f) (G.map g)
inst✝ : PreservesColimit (parallelPair f g) G
⊢ G.map (coequalizer.π f g) ≫ (PreservesCoequalizer.iso G f g).inv = coequalizer.π (G.map f) (G.map g)

Tactic:
rw [← ι_comp_coequalizerComparison_assoc, ← PreservesCoequalizer.iso_hom, Iso.hom_inv_id,
    comp_id]

Goal state after:
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
x y : M
⊢ (B x) y ^ 2 = (B x) y * (B y) x

Tactic:
rw [sq, ← hB.eq, RingHom.id_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
φ : Dual K V
⊢ W.quotAnnihilatorEquiv (Submodule.Quotient.mk φ) = (dualRestrict W) φ

Tactic:
ext
  rfl

Goal state after:
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
B : LinearMap.BilinForm R M
inst✝ : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
hB : IsSymm B
x y : M
⊢ (B x) y ^ 2 = (B x) y * (B y) x

Tactic:
rw [sq, ← hB.eq, RingHom.id_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ Submodule.dualPairing W = ↑W.quotAnnihilatorEquiv

Tactic:
ext
  rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: case zero.zero
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
⊢ ((dualDistrib R N M) 0) ((TensorProduct.comm R M N) 0) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) 0)) 0

Tactic:
simp_all [mul_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: case zero.tmul
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ : M
y✝ : N
⊢ ((dualDistrib R N M) 0) ((TensorProduct.comm R M N) (x✝ ⊗ₜ[R] y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) 0)) (x✝ ⊗ₜ[R] y✝)

Tactic:
simp_all [mul_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: case zero.add
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ y✝ : M ⊗[R] N
a✝¹ :
  ((dualDistrib R N M) 0) ((TensorProduct.comm R M N) x✝) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) 0)) x✝
a✝ :
  ((dualDistrib R N M) 0) ((TensorProduct.comm R M N) y✝) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) 0)) y✝
⊢ ((dualDistrib R N M) 0) ((TensorProduct.comm R M N) (x✝ + y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) 0)) (x✝ + y✝)

Tactic:
simp_all [mul_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: case tmul.zero
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ : Dual R N
y✝ : Dual R M
⊢ ((dualDistrib R N M) (x✝ ⊗ₜ[R] y✝)) ((TensorProduct.comm R M N) 0) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝ ⊗ₜ[R] y✝))) 0

Tactic:
simp_all [mul_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: case tmul.tmul
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝¹ : Dual R N
y✝¹ : Dual R M
x✝ : M
y✝ : N
⊢ ((dualDistrib R N M) (x✝¹ ⊗ₜ[R] y✝¹)) ((TensorProduct.comm R M N) (x✝ ⊗ₜ[R] y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝¹ ⊗ₜ[R] y✝¹))) (x✝ ⊗ₜ[R] y✝)

Tactic:
simp_all [mul_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: case tmul.add
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝¹ : Dual R N
y✝¹ : Dual R M
x✝ y✝ : M ⊗[R] N
a✝¹ :
  ((dualDistrib R N M) (x✝¹ ⊗ₜ[R] y✝¹)) ((TensorProduct.comm R M N) x✝) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝¹ ⊗ₜ[R] y✝¹))) x✝
a✝ :
  ((dualDistrib R N M) (x✝¹ ⊗ₜ[R] y✝¹)) ((TensorProduct.comm R M N) y✝) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝¹ ⊗ₜ[R] y✝¹))) y✝
⊢ ((dualDistrib R N M) (x✝¹ ⊗ₜ[R] y✝¹)) ((TensorProduct.comm R M N) (x✝ + y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝¹ ⊗ₜ[R] y✝¹))) (x✝ + y✝)

Tactic:
simp_all [mul_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: case add.zero
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ y✝ : Dual R N ⊗[R] Dual R M
a✝¹ :
  ((dualDistrib R N M) x✝) ((TensorProduct.comm R M N) 0) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) x✝)) 0
a✝ :
  ((dualDistrib R N M) y✝) ((TensorProduct.comm R M N) 0) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) y✝)) 0
⊢ ((dualDistrib R N M) (x✝ + y✝)) ((TensorProduct.comm R M N) 0) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝ + y✝))) 0

Tactic:
simp_all [mul_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: case add.tmul
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝¹ y✝¹ : Dual R N ⊗[R] Dual R M
x✝ : M
y✝ : N
a✝¹ :
  ((dualDistrib R N M) x✝¹) ((TensorProduct.comm R M N) (x✝ ⊗ₜ[R] y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) x✝¹)) (x✝ ⊗ₜ[R] y✝)
a✝ :
  ((dualDistrib R N M) y✝¹) ((TensorProduct.comm R M N) (x✝ ⊗ₜ[R] y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) y✝¹)) (x✝ ⊗ₜ[R] y✝)
⊢ ((dualDistrib R N M) (x✝¹ + y✝¹)) ((TensorProduct.comm R M N) (x✝ ⊗ₜ[R] y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝¹ + y✝¹))) (x✝ ⊗ₜ[R] y✝)

Tactic:
simp_all [mul_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: case add.add
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝¹ y✝¹ : Dual R N ⊗[R] Dual R M
x✝ y✝ : M ⊗[R] N
a✝³ :
  ((dualDistrib R N M) x✝¹) ((TensorProduct.comm R M N) x✝) =
      ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) x✝¹)) x✝ →
    ((dualDistrib R N M) y✝¹) ((TensorProduct.comm R M N) x✝) =
        ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) y✝¹)) x✝ →
      ((dualDistrib R N M) (x✝¹ + y✝¹)) ((TensorProduct.comm R M N) x✝) =
        ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝¹ + y✝¹))) x✝
a✝² :
  ((dualDistrib R N M) x✝¹) ((TensorProduct.comm R M N) y✝) =
      ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) x✝¹)) y✝ →
    ((dualDistrib R N M) y✝¹) ((TensorProduct.comm R M N) y✝) =
        ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) y✝¹)) y✝ →
      ((dualDistrib R N M) (x✝¹ + y✝¹)) ((TensorProduct.comm R M N) y✝) =
        ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝¹ + y✝¹))) y✝
a✝¹ :
  ((dualDistrib R N M) x✝¹) ((TensorProduct.comm R M N) (x✝ + y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) x✝¹)) (x✝ + y✝)
a✝ :
  ((dualDistrib R N M) y✝¹) ((TensorProduct.comm R M N) (x✝ + y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) y✝¹)) (x✝ + y✝)
⊢ ((dualDistrib R N M) (x✝¹ + y✝¹)) ((TensorProduct.comm R M N) (x✝ + y✝)) =
    ((dualDistrib R M N) ((TensorProduct.comm R (Dual R N) (Dual R M)) (x✝¹ + y✝¹))) (x✝ + y✝)

Tactic:
simp_all [mul_comm]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
P Q : C
f : P ⟶ Q
I : C := Abelian.image f
p : P ⟶ Abelian.image f := Abelian.factorThruImage f
i : kernel (cokernel.π f) ⟶ Q := kernel.ι (cokernel.π f)
R : C
g : I ⟶ R
hpg : p ≫ g = 0
u : kernel g ⟶ Q := kernel.ι g ≫ i
hu : NormalMono u
h : Q ⟶ NormalMono.Z u := NormalMono.g
t : P ⟶ kernel g
ht : t ≫ kernel.ι g = p
fh : f ≫ h = 0
l : cokernel f ⟶ NormalMono.Z u
hl : cokernel.π f ≫ l = h
hih : i ≫ h = 0
s : kernel (cokernel.π f) ⟶ kernel g
hs : s ≫ u = i
⊢ (s ≫ kernel.ι g) ≫ i = 𝟙 I ≫ i

Tactic:
rw [Category.assoc, hs, Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hl : IsLimit (KernelFork.ofι (diag A) ⋯) := ⋯
Z : C
x : Z ⟶ A
hx : x ≫ r A = 0
hxx : (x ≫ prod.lift (𝟙 A) 0) ≫ cokernel.π (diag A) = 0
y : Z ⟶ (KernelFork.ofι (diag A) ⋯).pt
hy : y ≫ diag A = x ≫ prod.lift (𝟙 A) 0
hyy : y = 0
this : Mono (prod.lift (𝟙 A) 0)
⊢ x ≫ prod.lift (𝟙 A) 0 = 0 ≫ prod.lift (𝟙 A) 0

Tactic:
← hy,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hl : IsLimit (KernelFork.ofι (diag A) ⋯) :=
  monoIsKernelOfCokernel (colimit.cocone (parallelPair (diag A) 0)) (colimit.isColimit (parallelPair (diag A) 0))
Z : C
x : Z ⟶ A
hx : x ≫ r A = 0
hxx : (x ≫ prod.lift (𝟙 A) 0) ≫ cokernel.π (diag A) = 0
y : Z ⟶ (KernelFork.ofι (diag A) ⋯).pt
hy : y ≫ diag A = x ≫ prod.lift (𝟙 A) 0
hyy : y = 0
this : Mono (prod.lift (𝟙 A) 0)
⊢ y ≫ diag A = 0 ≫ prod.lift (𝟙 A) 0
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hl : IsLimit (KernelFork.ofι (diag A) ⋯) :=
  monoIsKernelOfCokernel (colimit.cocone (parallelPair (diag A) 0)) (colimit.isColimit (parallelPair (diag A) 0))
Z : C
x : Z ⟶ A
hx : x ≫ r A = 0
hxx : (x ≫ prod.lift (𝟙 A) 0) ≫ cokernel.π (diag A) = 0
y : Z ⟶ (KernelFork.ofι (diag A) ⋯).pt
hy : y ≫ diag A = x ≫ prod.lift (𝟙 A) 0
hyy : y = 0
this : Mono (prod.lift (𝟙 A) 0)
⊢ y ≫ diag A = 0 ≫ prod.lift (𝟙 A) 0

Tactic:
hyy,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hl : IsLimit (KernelFork.ofι (diag A) ⋯) :=
  monoIsKernelOfCokernel (colimit.cocone (parallelPair (diag A) 0)) (colimit.isColimit (parallelPair (diag A) 0))
Z : C
x : Z ⟶ A
hx : x ≫ r A = 0
hxx : (x ≫ prod.lift (𝟙 A) 0) ≫ cokernel.π (diag A) = 0
y : Z ⟶ (KernelFork.ofι (diag A) ⋯).pt
hy : y ≫ diag A = x ≫ prod.lift (𝟙 A) 0
hyy : y = 0
this : Mono (prod.lift (𝟙 A) 0)
⊢ 0 ≫ diag A = 0 ≫ prod.lift (𝟙 A) 0
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: case refine_2
A B : GrpCat
f : A ⟶ B
b : ↑B
hb : h b = g b
r : b ∉ ↑(Hom.hom f).range
eq1 : (h b) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = fromCoset ⟨↑(Hom.hom f).range, ⋯⟩
eq2 : (g b) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩
⊢ False

Tactic:
exact (fromCoset_ne_of_nin_range _ r).symm (by rw [← eq1, ← eq2, DFunLike.congr_fun hb])

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
hf : S.f = 0
⊢ h.descQ (𝟙 S.X₂) ⋯ ≫ h.p = 𝟙 h.Q

Tactic:
simp only [← cancel_epi h.p, p_descQ_assoc, id_comp, comp_id]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
⊢ (ofIsLimitKernelFork S hf c hc).g' = S.g

Tactic:
← cancel_epi (ofIsLimitKernelFork S hf c hc).p,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
⊢ (ofIsLimitKernelFork S hf c hc).p ≫ (ofIsLimitKernelFork S hf c hc).g' = (ofIsLimitKernelFork S hf c hc).p ≫ S.g
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
T : C
φ : S.X₂ ⟶ T
⊢ (ofIsLimitKernelFork S hf c hc).descQ φ ⋯ = φ

Tactic:
← cancel_epi (ofIsLimitKernelFork S hf c hc).p,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
T : C
φ : S.X₂ ⟶ T
⊢ (ofIsLimitKernelFork S hf c hc).p ≫ (ofIsLimitKernelFork S hf c hc).descQ φ ⋯ = (ofIsLimitKernelFork S hf c hc).p ≫ φ
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : S.HasRightHomology
hg : S.g = 0
⊢ S.opcycles ≅ S.rightHomology

Tactic:
by
  have := S.isIso_rightHomologyι hg
  exact (asIso S.rightHomologyι).symm

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ (S.leftHomologyIso.symm ≪≫ h.leftHomologyIso).hom ≫ h.leftHomologyIso.inv = S.leftHomologyIso.inv

Tactic:
simp only [Iso.trans_hom, Iso.symm_hom, assoc, Iso.hom_inv_id, comp_id]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.RightHomologyData
⊢ (S.rightHomologyIso.symm ≪≫ h.rightHomologyIso).hom ≫ h.rightHomologyIso.inv = S.rightHomologyIso.inv

Tactic:
simp only [Iso.trans_hom, Iso.symm_hom, assoc, Iso.hom_inv_id, comp_id]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
hg : S.g = 0
inst✝ : S.HasHomology
⊢ IsIso S.homologyι

Tactic:
by
  have := S.isIso_rightHomologyι hg
  dsimp only [homologyι]
  infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
hₗ : S.LeftHomologyData
hᵣ : S.RightHomologyData
inst✝¹ : hₗ.IsPreservedBy F
inst✝ : hᵣ.IsPreservedBy F
⊢ F.map (hₗ.i ≫ hᵣ.p) = (hₗ.map F).π ≫ leftRightHomologyComparison' (hₗ.map F) (hᵣ.map F) ≫ (hᵣ.map F).ι

pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
hₗ : S.LeftHomologyData
hᵣ : S.RightHomologyData
inst✝¹ : hₗ.IsPreservedBy F
inst✝ : hᵣ.IsPreservedBy F
⊢ (hₗ.map F).π ≫ leftRightHomologyComparison' (hₗ.map F) (hᵣ.map F) ≫ (hᵣ.map F).ι =
    (Cofork.π (CokernelCofork.ofπ (hₗ.map F).π ⋯) ≫ leftRightHomologyComparison' (hₗ.map F) (hᵣ.map F)) ≫
      Fork.ι (KernelFork.ofι (hᵣ.map F).ι ⋯)

Tactic:
· rw [ShortComplex.π_leftRightHomologyComparison'_ι]; simp

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
hₗ : S.LeftHomologyData
hᵣ : S.RightHomologyData
inst✝¹ : hₗ.IsPreservedBy F
inst✝ : hᵣ.IsPreservedBy F
⊢ (hₗ.map F).π ≫ leftRightHomologyComparison' (hₗ.map F) (hᵣ.map F) ≫ (hᵣ.map F).ι =
    (Cofork.π (CokernelCofork.ofπ (hₗ.map F).π ⋯) ≫ leftRightHomologyComparison' (hₗ.map F) (hᵣ.map F)) ≫
      Fork.ι (KernelFork.ofι (hᵣ.map F).ι ⋯)