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

Goal state before:
pp: case neg
m : Type u_2
α : Type v
inst✝³ : Fintype m
inst✝² : CommRing α
inst✝¹ : Nontrivial m
inst✝ : Nontrivial α
a : m → α
i j : m
hij : i ≠ j
h : ¬a i = 0
h2 : ¬a j = 0
⊢ (fun k ↦ if k = i then a j else if k = j then -a i else 0) ≠ 0 ∧
    (fun k ↦ if k = i then a j else if k = j then -a i else 0) ⬝ᵥ a = 0

Tactic:
· refine ⟨Function.ne_iff.mpr ⟨i, by simp [h2]⟩, ?_⟩
    simp [dotProduct, Finset.sum_ite, Finset.sum_eq_ite i, hij.symm, mul_comm (a i)]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_2
ι : Type u_3
inst✝ : CommRing R
s : Set ι
hs : s.Finite
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
t : Finset ι
ht : ∀ (a : ι), a ∈ t ↔ a ∈ s
x✝ : R
⊢ x✝ ∈ ⋃ i ∈ s, ↑(f i) ↔ x✝ ∈ ⋃ i ∈ t, ↑(f i)

Tactic:
simpa using exists_congr (fun i ↦ (and_congr_left fun a ↦ ht i).symm)

Goal state after:
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: 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✝² : Fintype m
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
i : l
i' : m
j' : n
j : o
a : α
x : Matrix m n α
b : α
i'' : l
j'' : o
⊢ ∑ j_1,
      (∑ j, of (fun i'_1 j' ↦ if i = i'_1 ∧ i' = j' then a else 0) i'' j * x j j_1) *
        of (fun i' j'_1 ↦ if j' = i' ∧ j = j'_1 then b else 0) j_1 j'' =
    of (fun i'_1 j'_1 ↦ if i = i'_1 ∧ j = j'_1 then a * x i' j' * b else 0) i'' j''

Tactic:
by_cases h₁ : i = i'' <;> by_cases h₂ : j = j''

Goal state after:
case pos
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✝² : Fintype m
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
i : l
i' : m
j' : n
j : o
a : α
x : Matrix m n α
b : α
i'' : l
j'' : o
h₁ : i = i''
h₂ : j = j''
⊢ ∑ j_1,
      (∑ j, of (fun i'_1 j' ↦ if i = i'_1 ∧ i' = j' then a else 0) i'' j * x j j_1) *
        of (fun i' j'_1 ↦ if j' = i' ∧ j = j'_1 then b else 0) j_1 j'' =
    of (fun i'_1 j'_1 ↦ if i = i'_1 ∧ j = j'_1 then a * x i' j' * b else 0) i'' j''

case neg
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✝² : Fintype m
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
i : l
i' : m
j' : n
j : o
a : α
x : Matrix m n α
b : α
i'' : l
j'' : o
h₁ : i = i''
h₂ : ¬j = j''
⊢ ∑ j_1,
      (∑ j, of (fun i'_1 j' ↦ if i = i'_1 ∧ i' = j' then a else 0) i'' j * x j j_1) *
        of (fun i' j'_1 ↦ if j' = i' ∧ j = j'_1 then b else 0) j_1 j'' =
    of (fun i'_1 j'_1 ↦ if i = i'_1 ∧ j = j'_1 then a * x i' j' * b else 0) i'' j''

case pos
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✝² : Fintype m
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
i : l
i' : m
j' : n
j : o
a : α
x : Matrix m n α
b : α
i'' : l
j'' : o
h₁ : ¬i = i''
h₂ : j = j''
⊢ ∑ j_1,
      (∑ j, of (fun i'_1 j' ↦ if i = i'_1 ∧ i' = j' then a else 0) i'' j * x j j_1) *
        of (fun i' j'_1 ↦ if j' = i' ∧ j = j'_1 then b else 0) j_1 j'' =
    of (fun i'_1 j'_1 ↦ if i = i'_1 ∧ j = j'_1 then a * x i' j' * b else 0) i'' j''

case neg
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✝² : Fintype m
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
i : l
i' : m
j' : n
j : o
a : α
x : Matrix m n α
b : α
i'' : l
j'' : o
h₁ : ¬i = i''
h₂ : ¬j = j''
⊢ ∑ j_1,
      (∑ j, of (fun i'_1 j' ↦ if i = i'_1 ∧ i' = j' then a else 0) i'' j * x j j_1) *
        of (fun i' j'_1 ↦ if j' = i' ∧ j = j'_1 then b else 0) j_1 j'' =
    of (fun i'_1 j'_1 ↦ if i = i'_1 ∧ j = j'_1 then a * x i' j' * b else 0) i'' j''
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ (∃ a, s.toFinset = {a}) ↔ s.card ≠ 0 ∧ ∃ a, s = s.card • {a}

Tactic:
Multiset.toFinset_eq_singleton_iff,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ (∃ a, s.card ≠ 0 ∧ s = s.card • {a}) ↔ s.card ≠ 0 ∧ ∃ a, s = s.card • {a}
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
⊢ ∀ {x y : R},
    x ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} →
      y ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} → x + y ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x}

Tactic:
rintro _ _ ⟨x, ⟨hx, ⟨y, ⟨hy, rfl⟩⟩⟩⟩ ⟨a, ⟨ha, ⟨b, ⟨hb, rfl⟩⟩⟩⟩;
          exact ⟨x + a, ⟨add_mem _ hx ha, ⟨y + b, ⟨add_mem _ hy hb, by abel⟩⟩⟩⟩

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
⊢ comap f (map f S) ≤ S ⊔ adjoin R (⇑f ⁻¹' {0})

Tactic:
intro x hx
    rw [mem_comap, mem_map] at hx
    obtain ⟨y, hy, hxy⟩ := hx
    replace hxy : x - y ∈ f ⁻¹' {0} := by simp [hxy]
    rw [← Algebra.adjoin_eq S, ← Algebra.adjoin_union, ← add_sub_cancel y x]
    exact Subalgebra.add_mem _
      (Algebra.subset_adjoin <| Or.inl hy) (Algebra.subset_adjoin <| Or.inr hxy)

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

Goal state before:
pp: R : Type u
inst✝¹⁶ : CommSemiring R
S : Type ?u.6
inst✝¹⁵ : Semiring S
inst✝¹⁴ : Algebra R S
ι₁ : Type v₁
ι₂ : Type v₂
inst✝¹³ : DecidableEq ι₁
inst✝¹² : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝¹¹ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝¹⁰ : AddCommMonoid M₁'
inst✝⁹ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝⁸ : AddCommMonoid M₂'
inst✝⁷ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝⁶ : Module R M₁'
inst✝⁵ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝⁴ : Module R M₂'
inst✝³ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝² : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
inst✝¹ : Module S M₁'
inst✝ : IsScalarTower R S M₁'
⊢ ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) ≃ₗ[S] ⨁ (i : ι₁ × ι₂), M₁ i.1 ⊗[R] M₂ i.2

Tactic:
refine LinearEquiv.ofLinearMap ?toFun ?invFun ?left ?right
  · exact AlgebraTensorModule.lift <|
      toModule S _ _ fun i₁ => flip <| toModule R _ _ fun i₂ => flip <| AlgebraTensorModule.curry <|
      DirectSum.lof S (ι₁ × ι₂) (fun i => M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂)
  · exact toModule S _ _ fun i => AlgebraTensorModule.map (lof S _ M₁ i.1) (lof R _ M₂ i.2)
  · ext ⟨i₁, i₂⟩ x₁ x₂ : 4
    simp only [coe_comp, Function.comp_apply, toModule_lof, AlgebraTensorModule.map_tmul,
      AlgebraTensorModule.lift_apply, lift.tmul, coe_restrictScalars, flip_apply,
      AlgebraTensorModule.curry_apply, curry_apply, id_comp]
  · ext i₁ i₂ x₁ x₂ : 5
    simp only [coe_comp, Function.comp_apply, AlgebraTensorModule.curry_apply, curry_apply,
      coe_restrictScalars, AlgebraTensorModule.lift_apply, lift.tmul, toModule_lof, flip_apply,
      AlgebraTensorModule.map_tmul, id_coe, id_eq]

Goal state after:
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
p : ι →₀ R
n : N
i : ι
⊢ ((finsuppScalarLeft R N ι) (p ⊗ₜ[R] n)) i = p i • n

Tactic:
by
  simp [finsuppScalarLeft]

Goal state after:
Module: Mathlib.Algebra.Field.Opposite

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
q : ℚ≥0
⊢ unop ↑q = unop (↑q.num / ↑q.den)

Tactic:
unop_nnratCast,

Goal state after:
α : Type u_1
inst✝ : DivisionSemiring α
q : ℚ≥0
⊢ ↑q = unop (↑q.num / ↑q.den)
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : StarRing R
x : R
hx : star x = -x
⊢ Commute (star x) x

Tactic:
simp only [hx, Commute.neg_left, Commute.refl]

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : NonUnitalSemiring α
inst✝ : StarRing α
v w : m → α
⊢ star v ⬝ᵥ star w = star (w ⬝ᵥ v)

Tactic:
simp [dotProduct]

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : NonUnitalSemiring α
inst✝ : StarRing α
v w : m → α
⊢ star v ⬝ᵥ w = star (star w ⬝ᵥ v)

Tactic:
simp [dotProduct]

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : NonUnitalSemiring α
inst✝ : StarRing α
v w : m → α
⊢ v ⬝ᵥ star w = star (w ⬝ᵥ star v)

Tactic:
simp [dotProduct]

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

Goal state before:
pp: F : Type u_1
R✝ : Type u_2
A✝ : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝¹⁸ : CommSemiring R✝
inst✝¹⁷ : Semiring A✝
inst✝¹⁶ : Algebra R✝ A✝
inst✝¹⁵ : Star A✝
inst✝¹⁴ : Semiring B
inst✝¹³ : Algebra R✝ B
inst✝¹² : Star B
inst✝¹¹ : Semiring C
inst✝¹⁰ : Algebra R✝ C
inst✝⁹ : Star C
inst✝⁸ : Semiring D
inst✝⁷ : Algebra R✝ D
inst✝⁶ : Star D
R : Type u_7
A : Type u_8
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarMul A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
⊢ ∀ (x : R), (algebraMap R A) (star x) = star ((algebraMap R A) x)

Tactic:
by simp [Algebra.algebraMap_eq_smul_one]

Goal state after:
Module: Mathlib.Algebra.Field.Subfield.Defs

Goal state before:
pp: K : Type u
inst✝¹ : DivisionRing K
S : Type u_1
inst✝ : SetLike S K
h : SubfieldClass S K
s : S
q : ℚ≥0
⊢ ↑q ∈ s

Tactic:
by
  simpa only [NNRat.cast_def] using div_mem (natCast_mem s q.num) (natCast_mem s q.den)

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: case neg.intro.refine_1.refine_2.refine_1
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i
val✝ : Fintype ι
y' : O := ∑ i, c i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis (Fin n') R ↥N'
z : O
zN : z ∈ N
b : R
hb : ϕ ⟨z, ⋯⟩ = generator (ϕ.submoduleImage N) * b
⊢ ϕ ⟨z, ⋯⟩ - b • ϕ ⟨y, ⋯⟩ = 0

Tactic:
hb,

Goal state after:
case neg.intro.refine_1.refine_2.refine_1
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i
val✝ : Fintype ι
y' : O := ∑ i, c i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis (Fin n') R ↥N'
z : O
zN : z ∈ N
b : R
hb : ϕ ⟨z, ⋯⟩ = generator (ϕ.submoduleImage N) * b
⊢ generator (ϕ.submoduleImage N) * b - b • ϕ ⟨y, ⋯⟩ = 0
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
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • r₁ = rb • r₁'
hb' : ↑sb * ↑s₁ = rb * ↑s₁'
rc : R
sc : ↥S
hc : ↑sc * ↑s₁' = rc * ↑s₂
rd : R
sd : ↥S
hd : ↑sd * rb = rd * ↑sc
this : ↑sd * ↑sb * ↑s₁ = rd * rc * ↑s₂
⊢ (↑sc • r₁' + rc • r₂) /ₒ ⟨↑sc * ↑s₁', ⋯⟩ = (↑sd • sb • r₁ + (rd * rc) • r₂) /ₒ ⟨↑sd * ↑sb * ↑s₁, ⋯⟩

Tactic:
hb,

Goal state after:
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₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • r₁ = rb • r₁'
hb' : ↑sb * ↑s₁ = rb * ↑s₁'
rc : R
sc : ↥S
hc : ↑sc * ↑s₁' = rc * ↑s₂
rd : R
sd : ↥S
hd : ↑sd * rb = rd * ↑sc
this : ↑sd * ↑sb * ↑s₁ = rd * rc * ↑s₂
⊢ (↑sc • r₁' + rc • r₂) /ₒ ⟨↑sc * ↑s₁', ⋯⟩ = (↑sd • rb • r₁' + (rd * rc) • r₂) /ₒ ⟨↑sd * ↑sb * ↑s₁, ⋯⟩
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
s : Set K
p : (x : K) → x ∈ closure s → Prop
mem : ∀ (x : K) (hx : x ∈ s), p x ⋯
one : p 1 ⋯
add : ∀ (x y : K) (hx : x ∈ closure s) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : K) (hx : x ∈ closure s), p x hx → p (-x) ⋯
inv : ∀ (x : K) (hx : x ∈ closure s), p x hx → p x⁻¹ ⋯
mul : ∀ (x y : K) (hx : x ∈ closure s) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) ⋯
x : K
h : x ∈ closure s
x✝ : K
w✝ : x✝ ∈ closure s
hx : p x✝ w✝
⊢ -x✝ ∈ {x | ∃ (hx : x ∈ closure s), p x hx}

Tactic:
exact ⟨_, neg _ _ hx⟩

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i✝ j✝ : n
⊢ toMatrix' id i✝ j✝ = 1 i✝ j✝

Tactic:
rw [Matrix.one_apply, LinearMap.toMatrix'_apply, id_apply, Pi.single_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: case neg.intro.refine_2.refine_1.refine_2
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i
val✝ : Fintype ι
y' : O := ∑ i, c i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis (Fin n') R ↥N'
m' : ℕ
hn'm' : n' ≤ m'
bM' : Basis (Fin m') R ↥M'
z : O
zM : z ∈ M
⊢ M.subtype (⟨z, zM⟩ - ϕ ⟨z, zM⟩ • ⟨y', y'M⟩) = z + -ϕ ⟨z, zM⟩ • y'

Tactic:
rw [map_sub, map_smul, sub_eq_add_neg, neg_smul]

Goal state after:
case neg.intro.refine_2.refine_1.refine_2
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i
val✝ : Fintype ι
y' : O := ∑ i, c i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis (Fin n') R ↥N'
m' : ℕ
hn'm' : n' ≤ m'
bM' : Basis (Fin m') R ↥M'
z : O
zM : z ∈ M
⊢ M.subtype ⟨z, zM⟩ + -(ϕ ⟨z, zM⟩ • M.subtype ⟨y', y'M⟩) = z + -(ϕ ⟨z, zM⟩ • y')
Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors

Goal state before:
pp: case pos
R : Type u_1
inst✝⁴ : MonoidWithZero R
S : Submonoid R
inst✝³ : OreSet S
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
r t : R
s : ↥R⁰
hst : t * ↑s ∈ R⁰
hr : r = 0
⊢ (if hr : r = 0 then 0 else ↑s /ₒ ⟨r, ⋯⟩) = if hr : t • r = 0 then 0 else ↑⟨t * ↑s, hst⟩ /ₒ ⟨t • r, ⋯⟩

pp: case neg
R : Type u_1
inst✝⁴ : MonoidWithZero R
S : Submonoid R
inst✝³ : OreSet S
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
r t : R
s : ↥R⁰
hst : t * ↑s ∈ R⁰
hr : ¬r = 0
⊢ (if hr : r = 0 then 0 else ↑s /ₒ ⟨r, ⋯⟩) = if hr : t • r = 0 then 0 else ↑⟨t * ↑s, hst⟩ /ₒ ⟨t • r, ⋯⟩

Tactic:
· simp [hr]

Goal state after:
case neg
R : Type u_1
inst✝⁴ : MonoidWithZero R
S : Submonoid R
inst✝³ : OreSet S
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
r t : R
s : ↥R⁰
hst : t * ↑s ∈ R⁰
hr : ¬r = 0
⊢ (if hr : r = 0 then 0 else ↑s /ₒ ⟨r, ⋯⟩) = if hr : t • r = 0 then 0 else ↑⟨t * ↑s, hst⟩ /ₒ ⟨t • r, ⋯⟩
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₃
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₂))
⊢ ((↑sc * (↑sb * (↑sa * r₂)) + ↑sc * ↑sb * (ra * r₃)) /ₒ (sc * sb * (sa * s₂))) • (r₁ /ₒ s₁) =
    (↑sc • rb • r₁ + rc • r₁) /ₒ (sc * (sb * (sa * s₂)))

Tactic:
hb,

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₂))
⊢ ((↑sc * (rb * ↑s₁) + ↑sc * ↑sb * (ra * r₃)) /ₒ (sc * sb * (sa * s₂))) • (r₁ /ₒ s₁) =
    (↑sc • rb • r₁ + rc • r₁) /ₒ (sc * (sb * (sa * s₂)))
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: case refine_2
A : Type u_3
inst✝ : Semiring A
h : ∀ (n : ℕ) (f : End A (Fin n → A)), Surjective ⇑f → Injective ⇑f
n : ℕ
f g : End A (Fin n → A)
eq : f * g = 1
surj : Surjective ⇑f
this : ↑(LinearEquiv.ofBijective f ⋯).symm ∘ₗ ↑(LinearEquiv.ofBijective f ⋯) = LinearMap.id
⊢ g * f = 1

Tactic:
← left_inv_eq_right_inv this eq

Goal state after:
case refine_2
A : Type u_3
inst✝ : Semiring A
h : ∀ (n : ℕ) (f : End A (Fin n → A)), Surjective ⇑f → Injective ⇑f
n : ℕ
f g : End A (Fin n → A)
eq : f * g = 1
surj : Surjective ⇑f
this : ↑(LinearEquiv.ofBijective f ⋯).symm ∘ₗ ↑(LinearEquiv.ofBijective f ⋯) = LinearMap.id
⊢ ↑(LinearEquiv.ofBijective f ⋯).symm * f = 1
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R✝ : Type u_1
inst✝¹⁴ : CommSemiring R✝
M✝ N : 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)
A : Type u_4
inst✝⁹ : CommSemiring A
R : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : Algebra A R
M : Submonoid R
S : Type u_6
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra A S
inst✝⁴ : Algebra R S
inst✝³ : IsScalarTower A R S
P : Type u_7
inst✝² : CommSemiring P
inst✝¹ : Algebra A P
inst✝ : IsLocalization M S
f : R →ₐ[A] P
hf : ∀ (y : ↥M), IsUnit (f ↑y)
x : S
r : A
⊢ (↑↑(lift hf)).toFun ((algebraMap A S) r) = (algebraMap A P) r

Tactic:
by simp [IsScalarTower.algebraMap_apply A R S]

Goal state after:
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
A : Type u_4
inst✝ : CommRing A
K : Type u_5
x : ℤ
hx : x ∈ ℤ⁰
⊢ IsUnit ((algebraMap ℤ ℚ) ↑⟨x, hx⟩)

Tactic:
mem_nonZeroDivisors_iff_ne_zero

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
A : Type u_4
inst✝ : CommRing A
K : Type u_5
x : ℤ
hx✝ : x ∈ ℤ⁰
hx : x ≠ 0
⊢ IsUnit ((algebraMap ℤ ℚ) ↑⟨x, hx✝⟩)
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 : T
y : S₂
m : R
hm : m ∈ ↑M₁
hy : a * (algebraMap S₁ T) ((algebraMap R S₁) m) = (algebraMap S₂ T) (y, ⟨(algebraMap R S₂) m, ⋯⟩).1
z n : R
hn : n ∈ M₂
hz : y * (algebraMap R S₂) ↑(z, ⟨n, hn⟩).2 = (algebraMap R S₂) (z, ⟨n, hn⟩).1
hunit : IsUnit ((algebraMap R S₁) m)
| (algebraMap S₁ T) ((algebraMap R S₁) z) * (algebraMap S₁ T) ↑hunit.unit⁻¹

Tactic:
rw [← 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 : T
y : S₂
m : R
hm : m ∈ ↑M₁
hy : a * (algebraMap S₁ T) ((algebraMap R S₁) m) = (algebraMap S₂ T) (y, ⟨(algebraMap R S₂) m, ⋯⟩).1
z n : R
hn : n ∈ M₂
hz : y * (algebraMap R S₂) ↑(z, ⟨n, hn⟩).2 = (algebraMap R S₂) (z, ⟨n, hn⟩).1
hunit : IsUnit ((algebraMap R S₁) m)
| (algebraMap R T) z * (algebraMap S₁ T) ↑hunit.unit⁻¹
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
d : ↥M
⊢ mk a b + mk c d = mk (↑d * a + ↑b * c) (b * d)

Tactic:
mul_comm b d

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
d : ↥M
⊢ mk a b + mk c d = mk (↑d * a + ↑b * c) (d * b)
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: case mp
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
hM : M ≤ nonZeroDivisors R
h : (algebraMap R S) x = 0
c : ↥M
hc : ↑c * x = 0
⊢ x = 0

Tactic:
exact (hM c.2).1 x hc

Goal state after:
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: case neg
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
s : R
a : A
h : s ∉ σ a
h' : IsUnit (r • ↑ₐ (r⁻¹ • s) - a)
⊢ r • ↑⋯.unit⁻¹ = r • ↑h'.unit⁻¹

Tactic:
simp only [Algebra.algebraMap_eq_smul_one, smul_assoc, smul_inv_smul]

Goal state after: