mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq o
inst✝ : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
j' : m
hj : g.symm j ≠ j'
⊢ single i j r (f (f.symm i)) (g j') = single (f.symm i) (g.symm j) r (f.symm i) j'

Tactic:
rw [single_apply_of_col_ne _ _ hj, single_apply_of_col_ne]
    exact g.symm_apply_eq.not.1 hj

Goal state after:
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: case mp
α : Type u_1
ι : Sort u_3
β : Type u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ iUnion S
t : Set β
x : ↑T
i : ι
hi : ↑x ∈ S i
h : iUnionLift S f hf T hT x ∈ t
⊢ f i ⟨↑x, hi⟩ ∈ t

Tactic:
rwa [iUnionLift_of_mem x hi] at h

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

Goal state before:
pp: F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
b : Basis (Free.ChooseBasisIndex F K) F K := Free.chooseBasis F K
c : Basis (Free.ChooseBasisIndex K A) K A := Free.chooseBasis K A
⊢ lift.{w, v} (lift.{v, v} (Module.rank F K)) * lift.{v, w} (Module.rank K A) = lift.{v, w} (Module.rank F A)

Tactic:
← b.mk_eq_rank,

Goal state after:
F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
b : Basis (Free.ChooseBasisIndex F K) F K := Free.chooseBasis F K
c : Basis (Free.ChooseBasisIndex K A) K A := Free.chooseBasis K A
⊢ lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) * lift.{v, w} (Module.rank K A) = lift.{v, w} (Module.rank F A)
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
h : ¬Module.Finite R M
⊢ finrank R M = 0

Tactic:
rw [finrank, toNat_eq_zero, ← not_lt, Module.rank_lt_aleph0_iff]

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
h : ¬Module.Finite R M
⊢ Module.rank R M = 0 ∨ ¬Module.Finite R M
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I✝ I J : TwoSidedIdeal R
h :
  { toFun := ringCon, invFun := ofRingCon, left_inv := ⋯, right_inv := ⋯ } I ≤
    { toFun := ringCon, invFun := ofRingCon, left_inv := ⋯, right_inv := ⋯ } J
x : R
hx : x ∈ ↑I
⊢ x ∈ ↑J

Tactic:
SetLike.mem_coe,

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I✝ I J : TwoSidedIdeal R
h :
  { toFun := ringCon, invFun := ofRingCon, left_inv := ⋯, right_inv := ⋯ } I ≤
    { toFun := ringCon, invFun := ofRingCon, left_inv := ⋯, right_inv := ⋯ } J
x : R
hx : x ∈ I
⊢ x ∈ J
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
carrier : Set R
zero_mem : 0 ∈ carrier
add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier
neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier
mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier
mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier
x : R
⊢ x ∈ mk' carrier zero_mem add_mem neg_mem mul_mem_left mul_mem_right ↔ x ∈ carrier

Tactic:
by
  rw [mem_iff]
  simp [mk']

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: F : Type v'
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : Module R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : Module R B
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
φ : F
x✝ : B
⊢ x✝ ∈ ↑(NonUnitalAlgHom.range φ) ↔ x✝ ∈ Set.range ⇑φ

Tactic:
SetLike.mem_coe,

Goal state after:
F : Type v'
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : Module R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : Module R B
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
φ : F
x✝ : B
⊢ x✝ ∈ NonUnitalAlgHom.range φ ↔ x✝ ∈ Set.range ⇑φ
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: case refine_1.refine_1
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : FunLike F A B
inst✝² : NonUnitalAlgHomClass F R A B
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
a b : A
ha : a ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
hb : b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
⊢ ∀ x ∈ ↑(NonUnitalSubsemiring.closure s),
    ∀ x_1 ∈ ↑(NonUnitalSubsemiring.closure s), x_1 * x ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)

Tactic:
exact fun x (hx : x ∈ NonUnitalSubsemiring.closure s) y
              (hy : y ∈ NonUnitalSubsemiring.closure s) => Submodule.subset_span (mul_mem hy hx)

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: case refine_1.refine_3
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : FunLike F A B
inst✝² : NonUnitalAlgHomClass F R A B
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
a b : A
ha : a ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
hb : b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
⊢ ∀ (x y : A),
    x ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s) →
      y ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s) →
        (∀ x_1 ∈ ↑(NonUnitalSubsemiring.closure s), x_1 * x ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)) →
          (∀ x ∈ ↑(NonUnitalSubsemiring.closure s), x * y ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)) →
            ∀ x_1 ∈ ↑(NonUnitalSubsemiring.closure s),
              x_1 * (x + y) ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)

pp: case refine_1.refine_4
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : FunLike F A B
inst✝² : NonUnitalAlgHomClass F R A B
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
a b : A
ha : a ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
hb : b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
⊢ ∀ (a : R),
    ∀ x ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s),
      (∀ x_1 ∈ ↑(NonUnitalSubsemiring.closure s), x_1 * x ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)) →
        ∀ x_1 ∈ ↑(NonUnitalSubsemiring.closure s), x_1 * a • x ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)

Tactic:
· exact fun x y _ _ hx hy z hz => (mul_add z x y).symm ▸ add_mem (hx z hz) (hy z hz)

Goal state after:
case refine_1.refine_4
F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : FunLike F A B
inst✝² : NonUnitalAlgHomClass F R A B
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
a b : A
ha : a ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
hb : b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
⊢ ∀ (a : R),
    ∀ x ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s),
      (∀ x_1 ∈ ↑(NonUnitalSubsemiring.closure s), x_1 * x ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)) →
        ∀ x_1 ∈ ↑(NonUnitalSubsemiring.closure s), x_1 * a • x ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
S T U : Subalgebra R A
h : S ≤ T
X : Type u_1
inst✝² : SMul X R
inst✝¹ : SMul X A
inst✝ : IsScalarTower X R A
this : Module ↥S ↥T := (inclusion h).toModule
x : X
s : ↥S
t : ↥T
⊢ ↑(((x • 1) • s) • t) = ↑(x • s • t)

Tactic:
← one_smul R (s • t),

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
S T U : Subalgebra R A
h : S ≤ T
X : Type u_1
inst✝² : SMul X R
inst✝¹ : SMul X A
inst✝ : IsScalarTower X R A
this : Module ↥S ↥T := (inclusion h).toModule
x : X
s : ↥S
t : ↥T
⊢ ↑(((x • 1) • s) • t) = ↑(x • 1 • s • t)
Module: Mathlib.LinearAlgebra.TensorProduct.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq κ
𝒞 : Basis κ R N
x : M ⊗[R] N
i : κ
⊢ ((equivFinsuppOfBasisRight 𝒞) x) i = (TensorProduct.rid R M) ((lTensor M (𝒞.coord i)) x)

Tactic:
induction x

Goal state after:
case zero
R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq κ
𝒞 : Basis κ R N
i : κ
⊢ ((equivFinsuppOfBasisRight 𝒞) 0) i = (TensorProduct.rid R M) ((lTensor M (𝒞.coord i)) 0)

case tmul
R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq κ
𝒞 : Basis κ R N
i : κ
x✝ : M
y✝ : N
⊢ ((equivFinsuppOfBasisRight 𝒞) (x✝ ⊗ₜ[R] y✝)) i = (TensorProduct.rid R M) ((lTensor M (𝒞.coord i)) (x✝ ⊗ₜ[R] y✝))

case add
R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq κ
𝒞 : Basis κ R N
i : κ
x✝ y✝ : M ⊗[R] N
a✝¹ : ((equivFinsuppOfBasisRight 𝒞) x✝) i = (TensorProduct.rid R M) ((lTensor M (𝒞.coord i)) x✝)
a✝ : ((equivFinsuppOfBasisRight 𝒞) y✝) i = (TensorProduct.rid R M) ((lTensor M (𝒞.coord i)) y✝)
⊢ ((equivFinsuppOfBasisRight 𝒞) (x✝ + y✝)) i = (TensorProduct.rid R M) ((lTensor M (𝒞.coord i)) (x✝ + y✝))
Module: Mathlib.LinearAlgebra.TensorProduct.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
ℬ : Basis ι R M
x : M ⊗[R] N
i : ι
⊢ ((equivFinsuppOfBasisLeft ℬ) x) i = (TensorProduct.lid R N) ((rTensor N (ℬ.coord i)) x)

Tactic:
induction x

Goal state after:
case zero
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
ℬ : Basis ι R M
i : ι
⊢ ((equivFinsuppOfBasisLeft ℬ) 0) i = (TensorProduct.lid R N) ((rTensor N (ℬ.coord i)) 0)

case tmul
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
ℬ : Basis ι R M
i : ι
x✝ : M
y✝ : N
⊢ ((equivFinsuppOfBasisLeft ℬ) (x✝ ⊗ₜ[R] y✝)) i = (TensorProduct.lid R N) ((rTensor N (ℬ.coord i)) (x✝ ⊗ₜ[R] y✝))

case add
R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
ℬ : Basis ι R M
i : ι
x✝ y✝ : M ⊗[R] N
a✝¹ : ((equivFinsuppOfBasisLeft ℬ) x✝) i = (TensorProduct.lid R N) ((rTensor N (ℬ.coord i)) x✝)
a✝ : ((equivFinsuppOfBasisLeft ℬ) y✝) i = (TensorProduct.lid R N) ((rTensor N (ℬ.coord i)) y✝)
⊢ ((equivFinsuppOfBasisLeft ℬ) (x✝ + y✝)) i = (TensorProduct.lid R N) ((rTensor N (ℬ.coord i)) (x✝ + y✝))
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
inst✝¹ : AddGroup R
inst✝ : StarAddMonoid R
x : R
hx : IsSelfAdjoint x
⊢ IsSelfAdjoint (-x)

Tactic:
by
  simp only [isSelfAdjoint_iff, star_neg, hx.star_eq]

Goal state after:
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemigroup R
inst✝ : StarMul R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ IsSelfAdjoint (x * y)

Tactic:
simp only [isSelfAdjoint_iff, star_mul', hx.star_eq, hy.star_eq]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Star α
⊢ (M.map star)ᵀ.updateRow j (star c) = ((M.updateCol j c).map star)ᵀ

Tactic:
updateRow_transpose,

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Star α
⊢ ((M.map star).updateCol j (star c))ᵀ = ((M.updateCol j c).map star)ᵀ
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
⊢ (diagonal v)ᵀ.updateRow i (Pi.single i x) = diagonal (Function.update v i x)

Tactic:
updateRow_transpose,

Goal state after:
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
⊢ ((diagonal v).updateCol i (Pi.single i x))ᵀ = diagonal (Function.update v i x)
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ψ ⟨y, ⋯⟩
ψ' : ↥O →ₗ[R] R := r₁ • ϕ + r₂ • ψ
⊢ d ∈ ↑(ψ'.submoduleImage N)

Tactic:
SetLike.mem_coe,

Goal state after:
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ψ ⟨y, ⋯⟩
ψ' : ↥O →ₗ[R] R := r₁ • ϕ + r₂ • ψ
⊢ d ∈ ψ'.submoduleImage N
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
⊢ generator (ϕ.submoduleImage N) ∣ ψ ⟨y, ⋯⟩

Tactic:
by
  let a : R := generator (ϕ.submoduleImage N)
  let d : R := IsPrincipal.generator (Submodule.span R {a, ψ ⟨y, hNO yN⟩})
  have d_dvd_left : d ∣ a := (mem_iff_generator_dvd _).mp (subset_span (mem_insert _ _))
  have d_dvd_right : d ∣ ψ ⟨y, hNO yN⟩ :=
    (mem_iff_generator_dvd _).mp (subset_span (mem_insert_of_mem _ (mem_singleton _)))
  refine dvd_trans ?_ d_dvd_right
  rw [dvd_generator_iff, Ideal.span, ←
    span_singleton_generator (Submodule.span R {a, ψ ⟨y, hNO yN⟩})]
  · obtain ⟨r₁, r₂, d_eq⟩ : ∃ r₁ r₂ : R, d = r₁ * a + r₂ * ψ ⟨y, hNO yN⟩ := by
      obtain ⟨r₁, r₂', hr₂', hr₁⟩ :=
        mem_span_insert.mp (IsPrincipal.generator_mem (Submodule.span R {a, ψ ⟨y, hNO yN⟩}))
      obtain ⟨r₂, rfl⟩ := mem_span_singleton.mp hr₂'
      exact ⟨r₁, r₂, hr₁⟩
    let ψ' : O →ₗ[R] R := r₁ • ϕ + r₂ • ψ
    have : span R {d} ≤ ψ'.submoduleImage N := by
      rw [span_le, singleton_subset_iff, SetLike.mem_coe, LinearMap.mem_submoduleImage_of_le hNO]
      refine ⟨y, yN, ?_⟩
      change r₁ * ϕ ⟨y, hNO yN⟩ + r₂ * ψ ⟨y, hNO yN⟩ = d
      rw [d_eq, ϕy_eq]
    refine
      le_antisymm (this.trans (le_of_eq ?_)) (Ideal.span_singleton_le_span_singleton.mpr d_dvd_left)
    rw [span_singleton_generator]
    apply (le_trans _ this).eq_of_not_lt' (hϕ ψ')
    rw [← span_singleton_generator (ϕ.submoduleImage N)]
    exact Ideal.span_singleton_le_span_singleton.mpr d_dvd_left
  · exact subset_span (mem_insert _ _)

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: case refine_1
α : Type u_1
x y : α
h : Function.Injective ![x, y]
⊢ x ≠ y

pp: case refine_2
α : Type u_1
x y : α
h : x ≠ y
a b : Fin (Nat.succ 0).succ
h' : ![x, y] a = ![x, y] b
⊢ a = b

Tactic:
· simpa using h.ne Fin.zero_ne_one

Goal state after:
case refine_2
α : Type u_1
x y : α
h : x ≠ y
a b : Fin (Nat.succ 0).succ
h' : ![x, y] a = ![x, y] b
⊢ a = b
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u_1
x y : α
⊢ Function.Injective ![x, y] ↔ x ≠ y

Tactic:
refine ⟨fun h ↦ ?_, fun h a b h' ↦ ?_⟩
  · simpa using h.ne Fin.zero_ne_one
  · fin_cases a <;> fin_cases b <;> aesop

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
x✝¹ : A ⊗[R] ↥p
x✝ : x✝¹ ∈ {t | ∃ m n, m ⊗ₜ[R] n = t}
a : A
m : ↥p
h : a ⊗ₜ[R] m = x✝¹
⊢ a ⊗ₜ[R] m ∈ ↑(comap (LinearMap.baseChange A p.subtype) (span A ↑(map ((TensorProduct.mk R A M) 1) p)))

Tactic:
SetLike.mem_coe,

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
x✝¹ : A ⊗[R] ↥p
x✝ : x✝¹ ∈ {t | ∃ m n, m ⊗ₜ[R] n = t}
a : A
m : ↥p
h : a ⊗ₜ[R] m = x✝¹
⊢ a ⊗ₜ[R] m ∈ comap (LinearMap.baseChange A p.subtype) (span A ↑(map ((TensorProduct.mk R A M) 1) p))
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
m : Type u_3
n : Type u_4
inst✝ : Fintype m
M : Matrix m n R
this : DecidableEq m := Classical.decEq m
⊢ span R (Set.range fun x ↦ Pi.single x 1 ᵥ* M) = span R (Set.range M.row)

Tactic:
row_def

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
m : Type u_3
n : Type u_4
inst✝ : Fintype m
M : Matrix m n R
this : DecidableEq m := Classical.decEq m
⊢ span R (Set.range fun x ↦ Pi.single x 1 ᵥ* M) = span R (Set.range fun i ↦ M i)
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
m : Type u_4
n : Type u_5
inst✝ : Fintype n
M : Matrix m n R
⊢ M.mulVecLin.range = span R (Set.range M.col)

Tactic:
by
  rw [← vecMulLinear_transpose, range_vecMulLinear, row_transpose]

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
x : OreLocalization S X
⊢ 0 + x = x

Tactic:
induction x

Goal state after:
case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r✝ : X
s✝ : ↥S
⊢ 0 + r✝ /ₒ s✝ = r✝ /ₒ s✝
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
x : OreLocalization S X
⊢ x + 0 = x

Tactic:
induction x

Goal state after:
case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r✝ : X
s✝ : ↥S
⊢ r✝ /ₒ s✝ + 0 = r✝ /ₒ s✝
Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors

Goal state before:
pp: R : Type u_1
inst✝³ : MonoidWithZero R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
⊢ 0⁻¹ = 0

Tactic:
rw [OreLocalization.zero_def, OreLocalization.inv_def]

Goal state after:
R : Type u_1
inst✝³ : MonoidWithZero R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
⊢ (if hr : 0 = 0 then 0 else ↑1 /ₒ ⟨0, ⋯⟩) = 0 /ₒ 1
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃
⊢ ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) =
    rb • r₁ /ₒ (sb * (sa * s₂)) + ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁)

Tactic:
rcases oreDivSMulChar' ((sb * ra) • r₃) r₁ (sb * sa * s₂) s₁ with ⟨rc, sc, hc, hc'⟩

Goal state after:
case c.c.c
R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
r₁ : X
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₂ = ra * ↑s₃
rb : R
sb : ↥S
hb : ↑sb * sa • r₂ = rb * ↑s₁
hs₃rasb : ↑sb * ra * ↑s₃ ∈ S
ha' : ↑(sb * sa * s₂) = ↑sb * ra * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * (↑sb * ra) • r₃ = rc * ↑s₁
hc' : ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁) = rc • r₁ /ₒ (sc * (sb * sa * s₂))
⊢ ((sa • r₂ + ra • r₃) /ₒ (sa * s₂)) • (r₁ /ₒ s₁) =
    rb • r₁ /ₒ (sb * (sa * s₂)) + ((↑sb * ra) • r₃ /ₒ (sb * sa * s₂)) • (r₁ /ₒ s₁)
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
x y : S
⊢ g
        (((toLocalizationMap M S).sec y).1 * ↑((toLocalizationMap M S).sec x).2 *
          ↑((toLocalizationMap M S).sec (x + y)).2) +
      g
        (↑((toLocalizationMap M S).sec y).2 * ((toLocalizationMap M S).sec x).1 *
          ↑((toLocalizationMap M S).sec (x + y)).2) =
    g
      (↑((toLocalizationMap M S).sec y).2 * ↑((toLocalizationMap M S).sec x).2 *
        ((toLocalizationMap M S).sec (x + y)).1)

Tactic:
← map_add g

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
x y : S
⊢ g
      (((toLocalizationMap M S).sec y).1 * ↑((toLocalizationMap M S).sec x).2 *
          ↑((toLocalizationMap M S).sec (x + y)).2 +
        ↑((toLocalizationMap M S).sec y).2 * ((toLocalizationMap M S).sec x).1 *
          ↑((toLocalizationMap M S).sec (x + y)).2) =
    g
      (↑((toLocalizationMap M S).sec y).2 * ↑((toLocalizationMap M S).sec x).2 *
        ((toLocalizationMap M S).sec (x + y)).1)
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
a : R
ha : a ∈ ↑M₂
⊢ IsUnit ((algebraMap S₁ T) ↑⟨(algebraMap R S₁) a, ⋯⟩)

Tactic:
← IsScalarTower.algebraMap_apply,

Goal state after:
R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
a : R
ha : a ∈ ↑M₂
⊢ IsUnit ((algebraMap R T) a)