mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n m : ℕ
f : Matrix (Fin m) (Fin n) R
g : Matrix (Fin n) (Fin m) R
⊢ (transposeAddEquiv (Fin m) (Fin m) R) (opEquiv.mapMatrix.symm (opEquiv.mapMatrix f * opEquiv.mapMatrix g)) =
        (transposeAddEquiv (Fin m) (Fin m) R) (opEquiv.mapMatrix.symm 1) →
      m ≤ n ↔
    (transposeAddEquiv (Fin n) (Fin m) R).toEquiv g * (transposeAddEquiv (Fin m) (Fin n) R).toEquiv f = 1 → m ≤ n

Tactic:
congrm (?_ = ?_ → _)

Goal state after:
case refine_1
R : Type u_1
inst✝ : Semiring R
n m : ℕ
f : Matrix (Fin m) (Fin n) R
g : Matrix (Fin n) (Fin m) R
⊢ (transposeAddEquiv (Fin m) (Fin m) R) (opEquiv.mapMatrix.symm (opEquiv.mapMatrix f * opEquiv.mapMatrix g)) =
    (transposeAddEquiv (Fin n) (Fin m) R).toEquiv g * (transposeAddEquiv (Fin m) (Fin n) R).toEquiv f

case refine_2
R : Type u_1
inst✝ : Semiring R
n m : ℕ
f : Matrix (Fin m) (Fin n) R
g : Matrix (Fin n) (Fin m) R
⊢ (transposeAddEquiv (Fin m) (Fin m) R) (opEquiv.mapMatrix.symm 1) = 1
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: case refine_2.hdim
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 : finrank K (V ⧸ W) = 1
⊢ finrank K V ≤ finrank K ↥W + finrank K ↥(K ∙ v)

Tactic:
rw [← W.finrank_quotient_add_finrank, add_comm, add_le_add_iff_left, hW]
      aesop

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

Goal state before:
pp: case ha
K : Type u
V : Type v
W : Type v'
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Module K W
f : V →ₗ[K] W
p : Submodule K W
inst✝¹ : FiniteDimensional K ↥p
inst✝ : FiniteDimensional K ↥f.ker
⊢ lift.{v, v'} (Module.rank K ↥p) < ℵ₀

pp: case hb
K : Type u
V : Type v
W : Type v'
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Module K W
f : V →ₗ[K] W
p : Submodule K W
inst✝¹ : FiniteDimensional K ↥p
inst✝ : FiniteDimensional K ↥f.ker
⊢ lift.{v', v} (Module.rank K ↥f.ker) < ℵ₀

Tactic:
<;>

Goal state after:
case ha
K : Type u
V : Type v
W : Type v'
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Module K W
f : V →ₗ[K] W
p : Submodule K W
inst✝¹ : FiniteDimensional K ↥p
inst✝ : FiniteDimensional K ↥f.ker
⊢ lift.{v, v'} (Module.rank K ↥p) < ℵ₀

case hb
K : Type u
V : Type v
W : Type v'
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Module K W
f : V →ₗ[K] W
p : Submodule K W
inst✝¹ : FiniteDimensional K ↥p
inst✝ : FiniteDimensional K ↥f.ker
⊢ lift.{v', v} (Module.rank K ↥f.ker) < ℵ₀
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: case ha
K : Type u
V : Type v
W : Type v'
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Module K W
f : V →ₗ[K] W
p : Submodule K V
inst✝¹ : FiniteDimensional K (V ⧸ p)
inst✝ : FiniteDimensional K (W ⧸ f.range)
⊢ lift.{v, v'} (Module.rank K (W ⧸ f.range)) < ℵ₀

pp: case hb
K : Type u
V : Type v
W : Type v'
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Module K W
f : V →ₗ[K] W
p : Submodule K V
inst✝¹ : FiniteDimensional K (V ⧸ p)
inst✝ : FiniteDimensional K (W ⧸ f.range)
⊢ lift.{v', v} (Module.rank K (V ⧸ p)) < ℵ₀

Tactic:
<;>

Goal state after:
case ha
K : Type u
V : Type v
W : Type v'
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Module K W
f : V →ₗ[K] W
p : Submodule K V
inst✝¹ : FiniteDimensional K (V ⧸ p)
inst✝ : FiniteDimensional K (W ⧸ f.range)
⊢ lift.{v, v'} (Module.rank K (W ⧸ f.range)) < ℵ₀

case hb
K : Type u
V : Type v
W : Type v'
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Module K W
f : V →ₗ[K] W
p : Submodule K V
inst✝¹ : FiniteDimensional K (V ⧸ p)
inst✝ : FiniteDimensional K (W ⧸ f.range)
⊢ lift.{v', v} (Module.rank K (V ⧸ p)) < ℵ₀
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case mp
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I₁ I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M
v : n → M₁
⊢ (∀ (i j : n), i ≠ j → (B (v i)) (v j) = 0) → ∀ (i j : n), i ≠ j → (B.flip (v i)) (v j) = 0

pp: case mpr
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I₁ I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M
v : n → M₁
⊢ (∀ (i j : n), i ≠ j → (B.flip (v i)) (v j) = 0) → ∀ (i j : n), i ≠ j → (B (v i)) (v j) = 0

Tactic:
<;>

Goal state after:
case mp
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I₁ I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M
v : n → M₁
⊢ (∀ (i j : n), i ≠ j → (B (v i)) (v j) = 0) → ∀ (i j : n), i ≠ j → (B.flip (v i)) (v j) = 0

case mpr
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
n : Type u_19
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I₁ I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M
v : n → M₁
⊢ (∀ (i j : n), i ≠ j → (B.flip (v i)) (v j) = 0) → ∀ (i j : n), i ≠ j → (B (v i)) (v j) = 0
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case mp
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
⊢ (B x) y = 0 → (B (a • x)) y = 0

pp: case mpr
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
⊢ (B (a • x)) y = 0 → (B x) y = 0

Tactic:
<;>

Goal state after:
case mp
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
⊢ (B x) y = 0 → (B (a • x)) y = 0

case mpr
K : Type u_13
K₁ : Type u_14
K₂ : Type u_15
V : Type u_16
V₁ : Type u_17
V₂ : Type u_18
inst✝⁸ : Field K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : Field K₁
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K₁ V₁
inst✝² : Field K₂
inst✝¹ : AddCommGroup V₂
inst✝ : Module K₂ V₂
I₁ : K₁ →+* K
I₂ : K₂ →+* K
B : V₁ →ₛₗ[I₁] V₂ →ₛₗ[I₂] V
x : V₁
y : V₂
a : K₁
ha : a ≠ 0
⊢ (B (a • x)) y = 0 → (B x) y = 0
Module: Mathlib.Algebra.Category.FGModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
⊢ ModuleCat.isFG R (ModuleCat.of R PUnit.{v + 1})

Tactic:
unfold ModuleCat.isFG; infer_instance

Goal state after:
Module: Mathlib.Algebra.Category.FGModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
V W : Type v
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : Module.Finite R W
e : V ≃ₗ[R] W
⊢ ConcreteCategory.ofHom ↑e.symm ≫ ConcreteCategory.ofHom ↑e = 𝟙 (of R W)

Tactic:
by ext x; exact e.right_inv x

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case neg
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
m : Type u_7
n : Type u_8
inst✝³ : Fintype m
inst✝² : Finite n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : ¬¬(¬i = i' ∨ ¬j = j')
⊢ (toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) i' j' = Matrix.single i j 1 i' j'

Tactic:
Classical.not_not

Goal state after:
case neg
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
m : Type u_7
n : Type u_8
inst✝³ : Fintype m
inst✝² : Finite n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : ¬i = i' ∨ ¬j = j'
⊢ (toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) i' j' = Matrix.single i j 1 i' j'
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case neg
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
m : Type u_7
n : Type u_8
inst✝³ : Fintype m
inst✝² : Finite n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : ¬(i = i' ∧ j = j')
⊢ (toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) i' j' = Matrix.single i j 1 i' j'

Tactic:
rw [and_iff_not_or_not, Classical.not_not] at hij

Goal state after:
case neg
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
m : Type u_7
n : Type u_8
inst✝³ : Fintype m
inst✝² : Finite n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : ¬i = i' ∨ ¬j = j'
⊢ (toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) i' j' = Matrix.single i j 1 i' j'
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case neg.inl
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
m : Type u_7
n : Type u_8
inst✝³ : Fintype m
inst✝² : Finite n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : ¬i = i'
⊢ (toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) i' j' = Matrix.single i j 1 i' j'

pp: case neg.inr
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
m : Type u_7
n : Type u_8
inst✝³ : Fintype m
inst✝² : Finite n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : ¬j = j'
⊢ (toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) i' j' = Matrix.single i j 1 i' j'

Tactic:
<;>

Goal state after:
case neg.inl
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
m : Type u_7
n : Type u_8
inst✝³ : Fintype m
inst✝² : Finite n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : ¬i = i'
⊢ (toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) i' j' = Matrix.single i j 1 i' j'

case neg.inr
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
m : Type u_7
n : Type u_8
inst✝³ : Fintype m
inst✝² : Finite n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i i' : n
j' : m
hij : ¬j = j'
⊢ (toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) i' j' = Matrix.single i j 1 i' j'
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case mp
R : Type u_1
R₁ : Type u_2
M₁ : Type u_6
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I : R₁ →+* R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
⊢ B.IsAlt → B = -B.flip

pp: case mpr
R : Type u_1
R₁ : Type u_2
M₁ : Type u_6
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I : R₁ →+* R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
⊢ B = -B.flip → B.IsAlt

Tactic:
<;>

Goal state after:
case mp
R : Type u_1
R₁ : Type u_2
M₁ : Type u_6
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I : R₁ →+* R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
⊢ B.IsAlt → B = -B.flip

case mpr
R : Type u_1
R₁ : Type u_2
M₁ : Type u_6
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I : R₁ →+* R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
⊢ B = -B.flip → B.IsAlt
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case mp
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
⊢ B.IsAdjointPair B' ⇑f ⇑g → B' ∘ₗ f = B.compl₂ g

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
⊢ B' ∘ₗ f = B.compl₂ g → B.IsAdjointPair B' ⇑f ⇑g

Tactic:
<;>

Goal state after:
case mp
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
⊢ B.IsAdjointPair B' ⇑f ⇑g → B' ∘ₗ f = B.compl₂ g

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
⊢ B' ∘ₗ f = B.compl₂ g → B.IsAdjointPair B' ⇑f ⇑g
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: case e'_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
⊢ pullbackFst F =
    (pullback.fst (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
        prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left)) ≫
      prod.fst

pp: case e'_3
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
⊢ pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
      (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) =
    (pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
        prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
      prod.fst

Tactic:
<;>

Goal state after:
case e'_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
⊢ pullbackFst F =
    (pullback.fst (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
        prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left)) ≫
      prod.fst

case e'_3
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
⊢ pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
      (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) =
    (pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
        prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
      prod.fst
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: case e'_2
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
⊢ pullbackFst F ≫ F.map WalkingParallelPairHom.left =
    (pullback.fst (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
        prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left)) ≫
      prod.snd

pp: case e'_3
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
⊢ pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
        (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
      F.map WalkingParallelPairHom.right =
    (pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
        prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
      prod.snd

Tactic:
<;>

Goal state after:
case e'_2
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
⊢ pullbackFst F ≫ F.map WalkingParallelPairHom.left =
    (pullback.fst (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
        prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left)) ≫
      prod.snd

case e'_3
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
⊢ pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
        (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
      F.map WalkingParallelPairHom.right =
    (pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
        prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
      prod.snd
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: case zero
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
c : Cone F
⊢ pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯ ≫
      (equalizerCone F).π.app WalkingParallelPair.zero =
    c.π.app WalkingParallelPair.zero

pp: case one
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
c : Cone F
⊢ pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯ ≫
      (equalizerCone F).π.app WalkingParallelPair.one =
    c.π.app WalkingParallelPair.one

Tactic:
<;>

Goal state after:
case zero
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
c : Cone F
⊢ pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯ ≫
      (equalizerCone F).π.app WalkingParallelPair.zero =
    c.π.app WalkingParallelPair.zero

case one
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
c : Cone F
⊢ pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯ ≫
      (equalizerCone F).π.app WalkingParallelPair.one =
    c.π.app WalkingParallelPair.one
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

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:
<;>

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
⊢ B.SeparatingLeft → ∀ (x : M₁), B x = 0 → x = 0

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