mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
I : Ideal R
m n : ℕ
h : m + 1 ≤ m + 1 + n
⊢ I ^ (m + 1 + n) ≤ I ^ (m + 1)

Tactic:
add_comm,

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
I : Ideal R
m n : ℕ
h : m + 1 ≤ m + 1 + n
⊢ I ^ (n + (m + 1)) ≤ I ^ (m + 1)
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
x✝ : R
⊢ x✝ ∈ annihilator R (M × M') ↔ x✝ ∈ annihilator R M ⊓ annihilator R M'

Tactic:
Ideal.mem_inf,

Goal state after:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
x✝ : R
⊢ x✝ ∈ annihilator R (M × M') ↔ x✝ ∈ annihilator R M ∧ x✝ ∈ annihilator R M'
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
n : ℕ
⊢ I ^ (n + 1) = I * I ^ n

Tactic:
add_comm,

Goal state after:
R : Type u
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
n : ℕ
⊢ I ^ (1 + n) = I * I ^ n
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ (x + y * z) / y = x / y + z

Tactic:
eq_comm

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ x / y + z = (x + y * z) / y
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ (x - y * z) / y = x / y - z

Tactic:
eq_comm

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ≠ 0
h2 : y ∣ x
⊢ x / y - z = (x - y * z) / y
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ (z * x + y) / z = x + y / z

Tactic:
eq_comm

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ x + y / z = (z * x + y) / z
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ (z * x - y) / z = x - y / z

Tactic:
eq_comm

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ x - y / z = (z * x - y) / z
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ y = z * x ↔ z * x = y

Tactic:
eq_comm

Goal state after:
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : z ≠ 0
h2 : z ∣ y
⊢ z * x = y ↔ z * x = y
Module: Mathlib.RingTheory.Ideal.Nonunits

Goal state before:
pp: α : Type u_2
a : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
⊢ Ideal.span {a} ≠ ⊤

Tactic:
intro H

Goal state after:
α : Type u_2
a : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
H : Ideal.span {a} = ⊤
⊢ False
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
h2 : d₁ ^ k ∣ a * b
⊢ d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a

Tactic:
rw [mul_comm] at h2

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
⊢ d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd b a)
k : ℕ
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc✝ : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
h : b * (d₁ ^ k * a') = c ^ k
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
hb' : b = d₂ ^ k * b'
⊢ Associated (d₁ ^ k) a

Tactic:
hb',

Goal state after:
case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd b a)
k : ℕ
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc✝ : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
h0₂ : d₂ ^ k ≠ 0
b' : α
h : d₂ ^ k * b' * (d₁ ^ k * a') = c ^ k
hb' : b = d₂ ^ k * b'
⊢ Associated (d₁ ^ k) a
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h : a = 0 ∨ b = 0
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c

Tactic:
rcases h with (rfl | rfl)

Goal state after:
case pos.inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
b c : α
⊢ lcm 0 b ∣ c ↔ 0 ∣ c ∧ b ∣ c

case pos.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a c : α
⊢ lcm a 0 ∣ c ↔ a ∣ c ∧ 0 ∣ c
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : lcm a b = 0
⊢ Associated (gcd a b * lcm a b) 0

Tactic:
by rw [h, mul_zero]

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

Goal state before:
pp: R : Type u
ι : Type u_1
inst✝ : CommSemiring R
s : Finset ι
x : ι → R
p : Ideal R
hp : p.IsPrime
⊢ ∏ i ∈ s, x i ∈ p ↔ ∃ i ∈ s, x i ∈ p

Tactic:
simp_rw [← span_singleton_le_iff_mem, ← prod_span_singleton]
  exact hp.prod_le

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
f : Associates α →* α
hinv : Function.RightInverse (⇑f) Associates.mk
u : αˣ
⊢ (if ↑u = 0 then 1 else Classical.choose ⋯) = u⁻¹

Tactic:
by
    nontriviality α
    simp_rw [if_neg (Units.ne_zero u), Units.ext_iff]
    apply mul_left_cancel₀ (Units.ne_zero u)
    rw [Units.mul_inv, map_mk_unit_aux hinv u,
      Associates.mk_eq_mk_iff_associated.2 (associated_one_iff_isUnit.2 ⟨u, rfl⟩),
      Associates.mk_one, map_one]

Goal state after:
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
I✝ : Ideal R
ι : Type v
inst✝ : Fintype ι
ι' : Type w
I : Ideal R
e : (ι → R) →ₗ[R] ι' → R
x : (ι → R) ⧸ Ideal.pi fun x ↦ I
a b : ι → R
hab : (Submodule.quotientRel (Ideal.pi fun x ↦ I)) a b
h : ι'
⊢ (e a - e b) h ∈ (fun x ↦ I) h

Tactic:
Submodule.quotientRel_def

Goal state after:
R : Type u
inst✝¹ : CommRing R
I✝ : Ideal R
ι : Type v
inst✝ : Fintype ι
ι' : Type w
I : Ideal R
e : (ι → R) →ₗ[R] ι' → R
x : (ι → R) ⧸ Ideal.pi fun x ↦ I
a b : ι → R
hab : a - b ∈ Ideal.pi fun x ↦ I
h : ι'
⊢ (e a - e b) h ∈ (fun x ↦ I) h
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝ : Semiring R
hR : ¬IsPrincipalIdealRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
⊢ ∃ I ∈ nonPrincipals R, ∀ J ∈ c, J ≤ I

Tactic:
by_cases H : c.Nonempty

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
hR : ¬IsPrincipalIdealRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
H : c.Nonempty
⊢ ∃ I ∈ nonPrincipals R, ∀ J ∈ c, J ≤ I

case neg
R : Type u
inst✝ : Semiring R
hR : ¬IsPrincipalIdealRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
H : ¬c.Nonempty
⊢ ∃ I ∈ nonPrincipals R, ∀ J ∈ c, J ≤ I
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
hi : j = j'
⊢ (b.repr (b i • 1)) i' = (single (i, j) 1) (i', j')

pp: case neg
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
hi : ¬j = j'
⊢ (b.repr (b i • 0)) i' = (single (i, j) 1) (i', j')

Tactic:
· simp [hi, Finsupp.single_apply]

Goal state after:
case neg
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
hi : ¬j = j'
⊢ (b.repr (b i • 0)) i' = (single (i, j) 1) (i', j')
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
⊢ lift.{w, v} (Module.rank F K) * lift.{v, w} (Module.rank K A) = lift.{v, w} (Module.rank F A)

Tactic:
by
  let b := Module.Free.chooseBasis F K
  let c := Module.Free.chooseBasis K A
  rw [← (Module.rank F K).lift_id, ← b.mk_eq_rank, ← (Module.rank K A).lift_id, ← c.mk_eq_rank,
    ← lift_umax.{w, v}, ← (b.smulTower c).mk_eq_rank, mk_prod, lift_mul, lift_lift, lift_lift,
    lift_lift, lift_lift, lift_umax.{v, w}]

Goal state after:
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.rank R M = 0
⊢ Subsingleton M

Tactic:
rw [← Basis.mk_eq_rank'' (Module.Free.chooseBasis R M), Cardinal.mk_eq_zero_iff] at h

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 : IsEmpty (ChooseBasisIndex R M)
⊢ Subsingleton M
Module: Mathlib.RingTheory.SimpleRing.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
A : Type u_2
inst✝ : DivisionRing A
I : TwoSidedIdeal A
⊢ ¬I = ⊥ → 1 ∈ I

Tactic:
intro H

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
A : Type u_2
inst✝ : DivisionRing A
I : TwoSidedIdeal A
H : ¬I = ⊥
⊢ 1 ∈ I
Module: Mathlib.RingTheory.SimpleRing.Basic

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝² : NonAssocRing R
inst✝¹ : IsSimpleRing R
inst✝ : NonAssocSemiring S
f : R →+* S
h : TwoSidedIdeal.ker f = ⊤
mem : 1 = 0
⊢ 0 = 1

Tactic:
eq_comm

Goal state after:
R : Type u_2
S : Type u_3
inst✝² : NonAssocRing R
inst✝¹ : IsSimpleRing R
inst✝ : NonAssocSemiring S
f : R →+* S
h : TwoSidedIdeal.ker f = ⊤
mem : 0 = 1
⊢ 0 = 1
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J K : TwoSidedIdeal R
h1 : I ≤ J
h2 : I ≤ K
⊢ I ≤ { ringCon := J.ringCon ⊓ K.ringCon }

Tactic:
by rw [ringCon_le_iff] at h1 h2 ⊢; exact le_inf h1 h2

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

Goal state before:
pp: M : Type v
ι : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
x : ⨁ (x : ι), M
⊢ x = (of (fun i ↦ M) default) (x default)

Tactic:
eq_comm

Goal state after:
M : Type v
ι : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
x : ⨁ (x : ι), M
⊢ (of (fun i ↦ M) default) (x default) = x
Module: Mathlib.Algebra.DirectSum.Basic

Goal state before:
pp: ι : Type v
inst✝⁴ : DecidableEq ι
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
x : ⨁ (i : ι), ↥(A i)
⊢ ({ toFun := DFinsupp.sumAddHom, invFun := fun F i ↦ F.comp (DFinsupp.singleAddHom (fun i ↦ ↥(A i)) i), left_inv := ⋯,
          right_inv := ⋯ }
        fun i ↦ AddSubmonoidClass.subtype (A i))
      x =
    DFinsupp.sum x fun i x ↦ ↑x

Tactic:
exact DFinsupp.sumAddHom_apply _ x

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

Goal state before:
pp: R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
ι : Sort u_1
inst✝ : Nonempty ι
S : ι → Subalgebra R A
⊢ (iSup S).toSubsemiring = ⨆ i, (S i).toSubsemiring

Tactic:
by
  simp only [iSup, Set.range_nonempty, sSup_toSubsemiring, ← Set.range_comp, Function.comp_def]

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

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : NonUnitalNonAssocSemiring C
inst✝² : Module R C
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
φ : F
r : R
a : B
⊢ a ∈ (NonUnitalRingHom.srange ↑φ).carrier → r • a ∈ (NonUnitalRingHom.srange ↑φ).carrier

Tactic:
rintro ⟨a, rfl⟩

Goal state after:
F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : NonUnitalNonAssocSemiring C
inst✝² : Module R C
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
φ : F
r : R
a : A
⊢ r • ↑φ a ∈ (NonUnitalRingHom.srange ↑φ).carrier
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
A : ι → Submodule R M
inst✝ : DecidableEq M
x : ⨁ (i : ι), ↥(A i)
⊢ (DFinsupp.sumAddHom fun i ↦ (A i).subtype.toAddMonoidHom) x = DFinsupp.sum x fun i x ↦ ↑x

Tactic:
rw [DFinsupp.sumAddHom_apply]

Goal state after:
R : Type u
inst✝³ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
A : ι → Submodule R M
inst✝ : DecidableEq M
x : ⨁ (i : ι), ↥(A i)
⊢ (DFinsupp.sum x fun x ↦ ⇑(A x).subtype.toAddMonoidHom) = DFinsupp.sum x fun i x ↦ ↑x
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
S : Subalgebra R A
s : Set A
hS : S = adjoin R s
φ₁ φ₂ : ↥S →ₐ[R] B
h : ∀ (x : A) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
⊢ φ₁ = φ₂

Tactic:
subst hS

Goal state after:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
φ₁ φ₂ : ↥(adjoin R s) →ₐ[R] B
h : ∀ (x : A) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
⊢ φ₁ = φ₂
Module: Mathlib.Algebra.Module.Projective

Goal state before:
pp: case refine_2
R : Type u
inst✝² : Semiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
H : ∀ (i : ι), Projective R (M i)
⊢ Projective R (⨁ (i : ι), M i)

Tactic:
let e : (⨁ i, M i) ≃ₗ[R] Π₀ i, M i := .refl ..
    exact Projective.of_equiv' e.symm

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

Goal state before:
pp: case inr.inl
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ j₂ : J
hj : j₁ ≠ j₂
⊢ diagonal (fun j ↦ d i₁ j) j₁ j₂ = diagonal (fun ij ↦ d ij.1 ij.2) (i₁, j₁) (i₁, j₂)

pp: case inr.inr
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ : J
⊢ diagonal (fun j ↦ d i₁ j) j₁ j₁ = diagonal (fun ij ↦ d ij.1 ij.2) (i₁, j₁) (i₁, j₁)

Tactic:
· rw [diagonal_apply_ne _ hj, diagonal_apply_ne _ (ne_of_apply_ne Prod.snd hj)]

Goal state after:
case inr.inr
I : Type u_1
J : Type u_2
R : Type u_5
inst✝² : DecidableEq I
inst✝¹ : DecidableEq J
inst✝ : Zero R
d : I → J → R
i₁ : I
j₁ : J
⊢ diagonal (fun j ↦ d i₁ j) j₁ j₁ = diagonal (fun ij ↦ d ij.1 ij.2) (i₁, j₁) (i₁, j₁)
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x y z : R
⊢ z * x = x * y ↔ x * y = z * x

Tactic:
eq_comm

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

Goal state before:
pp: R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x y : R
⊢ op (star (x * y)) = op (star x) * op (star y)

Tactic:
by simp only [star_mul, op_mul]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : StarAddMonoid R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ IsSelfAdjoint (x + y)

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

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

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
inst✝¹ : StarMul R
x : R
inst✝ : Invertible x
⊢ IsSelfAdjoint ⅟x ↔ IsSelfAdjoint x

Tactic:
rw [isSelfAdjoint_iff, isSelfAdjoint_iff, star_invOf, invOf_inj]

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

Goal state before:
pp: 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
⊢ ⊤ ≤ baseChange A ⊤

Tactic:
← span_eq_top_of_span_eq_top R A _ (span_tmul_eq_top R ..)

Goal state after:
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
⊢ span A {t | ∃ m n, m ⊗ₜ[R] n = t} ≤ baseChange A ⊤
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
⊢ ↑sd * (↑sb * ↑s₁) = rd * rc * ↑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
⊢ ↑sd * (rb * ↑s₁') = rd * rc * ↑s₂
Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
f : S.LocalizationMap N
inst✝ : IsCancelMulZero M
⊢ IsCancelMulZero N

Tactic:
simp_rw [isCancelMulZero_iff_forall_isRegular, Commute.isRegular_iff (Commute.all _),
    ← Commute.isRightRegular_iff (Commute.all _)]

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoidWithZero N
f : S.LocalizationMap N
inst✝ : IsCancelMulZero M
⊢ ∀ {a : N}, a ≠ 0 → IsRightRegular a
Module: Mathlib.RingTheory.OreLocalization.NonZeroDivisors

Goal state before:
pp: case c
R : Type u_1
inst✝³ : MonoidWithZero R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
r : R
s : ↥R⁰
h : r /ₒ s ≠ 0
hr : r ≠ 0
⊢ (r /ₒ s * if hr : r = 0 then 0 else ↑s /ₒ ⟨r, ⋯⟩) = 1 /ₒ 1

Tactic:
simp only [hr]

Goal state after:
case c
R : Type u_1
inst✝³ : MonoidWithZero R
inst✝² : Nontrivial R
inst✝¹ : OreSet R⁰
inst✝ : NoZeroDivisors R
r : R
s : ↥R⁰
h : r /ₒ s ≠ 0
hr : r ≠ 0
⊢ (r /ₒ s * if h : False then 0 else ↑s /ₒ ⟨r, ⋯⟩) = 1 /ₒ 1
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: case neg
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
b : ι → M
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
inst✝¹ : Fintype ι
s : ι → M
hs : span R (range s) = ⊤
inst✝ : IsTorsionFree R M
this : ∃ s_1, LinearIndepOn R s s_1 ∧ ∀ i ∉ s_1, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' s_1)
I : Set ι := this.choose
indepI : LinearIndependent (ι := ↑I) R (s ∘ fun x ↦ ↑x)
hI : ∀ i ∉ I, ∃ a, a ≠ 0 ∧ a • s i ∈ span R (s '' I)
N : Submodule R M := span R (range (s ∘ fun x ↦ ↑x))
_sI : ↑I → ↥N := fun i ↦ ⟨s ↑i, ⋯⟩
sI_basis : Basis (↑I) R ↥N := Basis.span indepI
i : ι
hi : i ∉ I
⊢ ∃ a, a ≠ 0 ∧ a • s i ∈ N

Tactic:
simpa [image_eq_range s I] using! hI i hi

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
b✝ : ι → M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : Finite ι
b : Basis ι R M
N : Submodule R M
m n : ℕ
bM : Basis (Fin m) R ↥⊤
bN : Basis (Fin n) R ↥(comap ⊤.subtype N)
f : Fin n ↪ Fin m
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • bM (f i)
bM' : Basis (Fin m) R M := bM.map (LinearEquiv.ofTop ⊤ ⋯)
e : Fin m ≃ ι := bM'.indexEquiv b
i : Fin n
⊢ ↑((bN.map (comapSubtypeEquivOfLe ⋯)) i) = a i • (bM'.reindex e) ((f.trans e.toEmbedding) i)

Tactic:
simp only [bM', snf, Basis.map_apply, LinearEquiv.ofTop_apply, Submodule.coe_smul_of_tower,
      Submodule.comapSubtypeEquivOfLe_apply_coe, Basis.reindex_apply,
      Equiv.toEmbedding_apply, Function.Embedding.trans_apply, Equiv.symm_apply_apply]

Goal state after:
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
inst✝ : IsLocalization M S
x : R
y : ↥M
n : ℕ
⊢ (algebraMap R S) (x ^ n) = mk' S x y ^ n * (algebraMap R S) (↑y ^ n)

Tactic:
map_pow,

Goal state after:
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
y : ↥M
n : ℕ
⊢ (algebraMap R S) x ^ n = mk' S x y ^ n * (algebraMap R S) ↑y ^ n
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
inst✝ : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : ↥M
⊢ (algebraMap R S) (↑(y₁ * y₂) * x₁) + (algebraMap R S) ↑y₁ * (algebraMap R S) ↑(y₁ * y₂) * mk' S x₂ y₂ =
    (algebraMap R S) (x₁ * ↑y₂ + x₂ * ↑y₁) * (algebraMap R S) ↑y₁

Tactic:
add_comm,

Goal state after:
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₁ x₂ : R
y₁ y₂ : ↥M
⊢ (algebraMap R S) ↑y₁ * (algebraMap R S) ↑(y₁ * y₂) * mk' S x₂ y₂ + (algebraMap R S) (↑(y₁ * y₂) * x₁) =
    (algebraMap R S) (x₁ * ↑y₂ + x₂ * ↑y₁) * (algebraMap R S) ↑y₁
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 x).1 * ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2 +
      g ↑((toLocalizationMap M S).sec x).2 *
        (↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2 * ((toLocalizationMap M S).lift hg) y) =
    g ↑((toLocalizationMap M S).sec x).2 * ↑g.toMonoidWithZeroHom ((toLocalizationMap M S).sec (x + y)).1

Tactic:
add_comm,

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 x).2 *
        (↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2 * ((toLocalizationMap M S).lift hg) y) +
      g ((toLocalizationMap M S).sec x).1 * ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2 =
    g ↑((toLocalizationMap M S).sec x).2 * ↑g.toMonoidWithZeroHom ((toLocalizationMap M S).sec (x + y)).1