mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: case e'_4
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ max #↑s ℵ₀ = max (lift.{0, u} #(Fin 6 ⊕ ↑s)) ℵ₀

pp: case convert_3
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ ∀ (a : Fin 6 ⊕ ↑s), Finite (Operands s a)

Tactic:
· rw [lift_uzero, mk_sum, lift_uzero]
      have : lift.{u, 0} #(Fin 6) < ℵ₀ := lift_lt_aleph0.mpr (lt_aleph0_of_finite _)
      obtain h | h := lt_or_ge #s ℵ₀
      · rw [max_eq_right h.le, max_eq_right]
        exact (add_lt_aleph0 this h).le
      · rw [max_eq_left h, add_eq_right h (this.le.trans h), max_eq_left h]

Goal state after:
case convert_3
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ ∀ (a : Fin 6 ⊕ ↑s), Finite (Operands s a)
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ (∑ x ∈ f.support, f x * if x = i then 1 else 0) = f i

Tactic:
mul_boole,

Goal state after:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ (∑ x ∈ f.support, if x = i then f x else 0) = f i
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ (∑ x ∈ f.support, f x * if i = x then 1 else 0) = f i

Tactic:
mul_boole,

Goal state after:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ (∑ x ∈ f.support, if i = x then f x else 0) = f i
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: case intro
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : ι →₀ R
i : ι
val✝ : Fintype ι
⊢ (∑ x, f x * if i = x then 1 else 0) = f i

Tactic:
mul_boole,

Goal state after:
case intro
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : ι →₀ R
i : ι
val✝ : Fintype ι
⊢ (∑ x, if i = x then f x else 0) = f i
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: case inr
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this✝ : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i ↦ bK i.1 i.2)
hLK : #↥L < #K
this : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
card_ιL : ℵ₀ ≤ #ιL
e : ℕ ↪ ιL
c : ιK →₀ K := bK.repr (⇑bL ∘ ⇑e)
rep_e : ∑ a ∈ c.support, c a • bK a = ⇑bL ∘ ⇑e
⊢ False

Tactic:
set s := c.support

Goal state after:
case inr
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this✝ : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i ↦ bK i.1 i.2)
hLK : #↥L < #K
this : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
card_ιL : ℵ₀ ≤ #ιL
e : ℕ ↪ ιL
c : ιK →₀ K := bK.repr (⇑bL ∘ ⇑e)
s : Finset ιK := c.support
rep_e : ∑ a ∈ s, c a • bK a = ⇑bL ∘ ⇑e
⊢ False
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: case refine_1.inr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
t : K
hw : t • v ∈ W ⊓ K ∙ v
ht : t • v ∈ W
ht₀ : t ≠ 0
⊢ t • v = 0

Tactic:
rw [Submodule.smul_mem_iff _ ht₀] at ht

Goal state after:
case refine_1.inr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
t : K
hw : t • v ∈ W ⊓ K ∙ v
ht : v ∈ W
ht₀ : t ≠ 0
⊢ t • v = 0
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
inst✝ : Module.Finite K V
W : Submodule K V
h : finrank K ↥W = finrank K V
⊢ finrank K ↥W = finrank K V

Tactic:
h

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
W : Submodule K V
h : finrank K ↥W = finrank K V
⊢ finrank K V = finrank K V
Module: Mathlib.LinearAlgebra.Coevaluation

Goal state before:
pp: K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := ⋯
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (((TensorProduct.mk K (Dual K V) K).compr₂ₛₗ
          (LinearMap.rTensor (Dual K V) (contractLeft K V) ∘ₗ
            ↑(TensorProduct.assoc K (Dual K V) V (Dual K V)).symm ∘ₗ LinearMap.lTensor (Dual K V) (coevaluation K V)))
        ((Basis.ofVectorSpace K V).dualBasis j))
      1 =
    (((TensorProduct.mk K (Dual K V) K).compr₂ₛₗ
          (↑(TensorProduct.lid K (Dual K V)).symm ∘ₗ ↑(TensorProduct.rid K (Dual K V))))
        ((Basis.ofVectorSpace K V).dualBasis j))
      1

Tactic:
rw [LinearMap.compr₂ₛₗ_apply, LinearMap.compr₂ₛₗ_apply, TensorProduct.mk_apply]

Goal state after:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.rTensor (Dual K V) (contractLeft K V) ∘ₗ
        ↑(TensorProduct.assoc K (Dual K V) V (Dual K V)).symm ∘ₗ LinearMap.lTensor (Dual K V) (coevaluation K V))
      ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] 1) =
    (↑(TensorProduct.lid K (Dual K V)).symm ∘ₗ ↑(TensorProduct.rid K (Dual K V)))
      ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] 1)
Module: Mathlib.LinearAlgebra.Coevaluation

Goal state before:
pp: K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (((TensorProduct.mk K K V).compr₂ₛₗ
          (LinearMap.lTensor V (contractLeft K V) ∘ₗ
            ↑(TensorProduct.assoc K V (Dual K V) V) ∘ₗ LinearMap.rTensor V (coevaluation K V)))
        1)
      ((Basis.ofVectorSpace K V) j) =
    (((TensorProduct.mk K K V).compr₂ₛₗ (↑(TensorProduct.rid K V).symm ∘ₗ ↑(TensorProduct.lid K V))) 1)
      ((Basis.ofVectorSpace K V) j)

Tactic:
rw [LinearMap.compr₂ₛₗ_apply, LinearMap.compr₂ₛₗ_apply, TensorProduct.mk_apply]

Goal state after:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.lTensor V (contractLeft K V) ∘ₗ
        ↑(TensorProduct.assoc K V (Dual K V) V) ∘ₗ LinearMap.rTensor V (coevaluation K V))
      (1 ⊗ₜ[K] (Basis.ofVectorSpace K V) j) =
    (↑(TensorProduct.rid K V).symm ∘ₗ ↑(TensorProduct.lid K V)) (1 ⊗ₜ[K] (Basis.ofVectorSpace K V) j)
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
x y : M₁
⊢ (B x) y = 0 → (B y) x = 0

Tactic:
h

Goal state after:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
x y : M₁
h : (B x) y = 0
⊢ (B y) x = 0
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
f : M →ₗ[R] M₁
g : M₁ →ₗ[R] M
h : B' ∘ₗ f = B.compl₂ g
x✝ : M
y✝ : M₁
⊢ ((B' ∘ₗ f) x✝) y✝ = ((B.compl₂ g) x✝) y✝

Tactic:
h

Goal state after:
case mpr
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
f : M →ₗ[R] M₁
g : M₁ →ₗ[R] M
h : B' ∘ₗ f = B.compl₂ g
x✝ : M
y✝ : M₁
⊢ ((B.compl₂ g) x✝) y✝ = ((B.compl₂ g) x✝) y✝
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
f : M →ₗ[R] M₁
g : M₁ →ₗ[R] M
h : B' ∘ₗ f = B.compl₂ g
⊢ B.IsAdjointPair B' ⇑f ⇑g

Tactic:
intro _ _
    rw [← compl₂_apply, ← comp_apply, h]

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

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : Module R M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] M₃
f : M → M₁
g : M₁ → M
f' : M₁ → M₂
g' : M₂ → M₁
h : B.IsAdjointPair B' f g
h' : B'.IsAdjointPair B'' f' g'
x✝¹ : M
x✝ : M₂
⊢ (B' (f x✝¹)) (g' x✝) = (B x✝¹) ((fun x ↦ g (g' x)) x✝)

Tactic:
h

Goal state after:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : Module R M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] M₃
f : M → M₁
g : M₁ → M
f' : M₁ → M₂
g' : M₂ → M₁
h : B.IsAdjointPair B' f g
h' : B'.IsAdjointPair B'' f' g'
x✝¹ : M
x✝ : M₂
⊢ (B x✝¹) (g (g' x✝)) = (B x✝¹) ((fun x ↦ g (g' x)) x✝)
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case mp
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
⊢ B.SeparatingLeft → ∀ (x : M₁), B x = 0 → x = 0

Tactic:
intro h x hB

Goal state after:
case mp
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
h : B.SeparatingLeft
x : M₁
hB : B x = 0
⊢ x = 0
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
⊢ (∀ (x : M₁), B x = 0 → x = 0) → B.SeparatingLeft

Tactic:
intro h x hB

Goal state after:
case mpr
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
h : ∀ (x : M₁), B x = 0 → x = 0
x : M₁
hB : ∀ (y : M₂), (B x) y = 0
⊢ x = 0
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
W : D
k : G.obj Y ⟶ W
wk : G.map f ≫ k = G.map g ≫ k
⊢ (G.map (coequalizer.π f g) ≫ (PreservesCoequalizer.iso G f g).inv) ≫ coequalizer.desc k wk = k

Tactic:
map_π_preserves_coequalizer_inv,

Goal state after:
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
W : D
k : G.obj Y ⟶ W
wk : G.map f ≫ k = G.map g ≫ k
⊢ coequalizer.π (G.map f) (G.map g) ≫ coequalizer.desc k wk = k
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
X' Y' : D
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : G.obj X ⟶ X'
q : G.obj Y ⟶ Y'
wf : G.map f ≫ q = p ≫ f'
wg : G.map g ≫ q = p ≫ g'
⊢ (G.map (coequalizer.π f g) ≫ (PreservesCoequalizer.iso G f g).inv) ≫
      colimMap (parallelPairHom (G.map f) (G.map g) f' g' p q wf wg) =
    q ≫ coequalizer.π f' g'

Tactic:
map_π_preserves_coequalizer_inv,

Goal state after:
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
X' Y' : D
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : G.obj X ⟶ X'
q : G.obj Y ⟶ Y'
wf : G.map f ≫ q = p ≫ f'
wg : G.map g ≫ q = p ≫ g'
⊢ coequalizer.π (G.map f) (G.map g) ≫ colimMap (parallelPairHom (G.map f) (G.map g) f' g' p q wf wg) =
    q ≫ coequalizer.π f' g'
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, (L i).ker ≤ K.ker
hK : K ∉ span 𝕜 (Set.range L)
φ : Dual 𝕜 (E →ₗ[𝕜] 𝕜)
φne : φ K ≠ 0
hφ : map φ (span 𝕜 (Set.range L)) = ⊥
φs : E := (evalEquiv 𝕜 E).symm φ
⊢ K φs = 0

Tactic:
refine h <| (Submodule.mem_iInf _).2 fun i ↦ (mem_bot 𝕜).1 ?_

Goal state after:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, (L i).ker ≤ K.ker
hK : K ∉ span 𝕜 (Set.range L)
φ : Dual 𝕜 (E →ₗ[𝕜] 𝕜)
φne : φ K ≠ 0
hφ : map φ (span 𝕜 (Set.range L)) = ⊥
φs : E := (evalEquiv 𝕜 E).symm φ
i : ι
⊢ (L i) φs ∈ ⊥
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case pos
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
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
he : (B x) y * (B y) x = (B x) x * (B y) y
hz : (B x) y • x - (B x) x • y = 0
hL : LinearIndependent R ![x, y]
hx : x = 0
⊢ False

pp: case neg
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
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
he : (B x) y * (B y) x = (B x) x * (B y) y
hz : (B x) y • x - (B x) x • y = 0
hL : LinearIndependent R ![x, y]
hx : ¬x = 0
⊢ False

Tactic:
· simpa [hx] using LinearIndependent.ne_zero 0 hL

Goal state after:
case neg
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
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
he : (B x) y * (B y) x = (B x) x * (B y) y
hz : (B x) y • x - (B x) x • y = 0
hL : LinearIndependent R ![x, y]
hx : ¬x = 0
⊢ False
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
W : Submodule R M
hW : Disjoint W (ker B)
hB' : (domRestrict₁₂ B W W).IsRefl
x : M
hx : x ∈ W
⊢ (∀ (y : ↥W), ((domRestrict₁₂ B W W) ⟨x, hx⟩) y = 0) → ⟨x, hx⟩ = 0

Tactic:
h

Goal state after:
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
W : Submodule R M
hW : Disjoint W (ker B)
hB' : (domRestrict₁₂ B W W).IsRefl
x : M
hx : x ∈ W
h : ∀ (y : ↥W), ((domRestrict₁₂ B W W) ⟨x, hx⟩) y = 0
⊢ ⟨x, hx⟩ = 0
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: case right
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
x : ↥W
⊢ (∀ (x_1 : Dual K V₁ ⧸ dualAnnihilator W), ((Submodule.dualPairing W) x_1) x = 0) → x = 0

Tactic:
h

Goal state after:
case right
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
x : ↥W
h : ∀ (x_1 : Dual K V₁ ⧸ dualAnnihilator W), ((Submodule.dualPairing W) x_1) x = 0
⊢ x = 0
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: case of_equiv
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
α β : Type u_4
⊢ ∀ (a : α ≃ β),
    (∀ (W : α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)) →
      ∀ (W : β → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)

Tactic:
h

Goal state after:
case of_equiv
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
α β : Type u_4
h : α ≃ β
⊢ (∀ (W : α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)) →
    ∀ (W : β → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: case h_option
K : Type u_1
V₁ : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
α : Type u_4
inst✝ : Fintype α
⊢ (∀ (W : α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)) →
    ∀ (W : Option α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)

Tactic:
h

Goal state after:
case h_option
K : Type u_1
V₁ : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
α : Type u_4
inst✝ : Fintype α
h : ∀ (W : α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)
⊢ ∀ (W : Option α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: case h_option
K : Type u_1
V₁ : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
α : Type u_4
inst✝ : Fintype α
h : ∀ (W : α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)
W : Option α → Subspace K V₁
⊢ dualAnnihilator (W none) ⊔ dualAnnihilator (⨅ b, W (some b)) =
    dualAnnihilator (W none) ⊔ ⨆ b, dualAnnihilator (W (some b))

Tactic:
h

Goal state after:
case h_option
K : Type u_1
V₁ : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
α : Type u_4
inst✝ : Fintype α
h : ∀ (W : α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)
W : Option α → Subspace K V₁
⊢ dualAnnihilator (W none) ⊔ ⨆ i, dualAnnihilator (W (some i)) =
    dualAnnihilator (W none) ⊔ ⨆ b, dualAnnihilator (W (some b))
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hlp : prod.lift (𝟙 A) 0 ≫ prod.snd = 0
s : Fork prod.snd 0
m : s.pt ⟶ (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp).pt
⊢ m ≫ Fork.ι (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) = s.ι → m = s.ι ≫ prod.fst

Tactic:
h

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hlp : prod.lift (𝟙 A) 0 ≫ prod.snd = 0
s : Fork prod.snd 0
m : s.pt ⟶ (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp).pt
h : m ≫ Fork.ι (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) = s.ι
⊢ m = s.ι ≫ prod.fst
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hlp : prod.lift (𝟙 A) 0 ≫ prod.snd = 0
hp1 : IsLimit (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) :=
  Fork.IsLimit.mk (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) (fun s ↦ s.ι ≫ prod.fst) ⋯ ⋯
hp2 : IsColimit (CokernelCofork.ofπ prod.snd hlp) := epiIsCokernelOfKernel (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) hp1
Z : C
⊢ ∀ (g : cokernel (diag A) ⟶ Z), r A ≫ g = 0 → g = 0

Tactic:
z

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hlp : prod.lift (𝟙 A) 0 ≫ prod.snd = 0
hp1 : IsLimit (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) :=
  Fork.IsLimit.mk (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) (fun s ↦ s.ι ≫ prod.fst) ⋯ ⋯
hp2 : IsColimit (CokernelCofork.ofπ prod.snd hlp) := epiIsCokernelOfKernel (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) hp1
Z : C
z : cokernel (diag A) ⟶ Z
⊢ r A ≫ z = 0 → z = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCokernels C
inst✝² : IsNormalEpiCategory C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst✝¹ : Epi a
inst✝ : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
⊢ b ≫ b' ≫ cokernel.desc (coprod.desc f g) (b ≫ s.inr) ⋯ = b ≫ s.inr

Tactic:
rw [CokernelCofork.π_ofπ] at hb'
              have reassoced' {W : C} (h : cokernel (coprod.desc f g) ⟶ W) : b ≫ b' ≫ h
                = cokernel.π (coprod.desc f g) ≫ h := by rw [← Category.assoc, eq_whisker hb']
              simp [reassoced']

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ 0 - -b - (0 - a) = b + a

Tactic:
add_def,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ 0 - -b - (0 - a) = b - -a
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ a + -b = a - b

Tactic:
add_def,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ a - - -b = a - b
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ 0 - a - (0 - b) = 0 - a + b

Tactic:
add_def,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ 0 - a - (0 - b) = 0 - a - -b