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

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ annihilator R M ≤ ⊥ ↔ FaithfulSMul R M

Tactic:
refine ⟨fun H ↦ ⟨fun {r s} H' ↦ ?_⟩, fun ⟨H⟩ {a} ha ↦ ?_⟩

Goal state after:
case refine_1
R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : annihilator R M ≤ ⊥
r s : R
H' : ∀ (a : M), r • a = s • a
⊢ r = s

case refine_2
R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : FaithfulSMul R M
a : R
ha : a ∈ annihilator R M
H : ∀ {m₁ m₂ : R}, (∀ (a : M), m₁ • a = m₂ • a) → m₁ = m₂
⊢ a ∈ ⊥
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
I J : Ideal R
e : I ≤ J
n : ℕ
⊢ I ^ n ≤ J ^ n

Tactic:
induction n with
  | zero => rw [Submodule.pow_zero, Submodule.pow_zero]
  | succ _ hn =>
    rw [Submodule.pow_succ, Submodule.pow_succ]
    exact Ideal.mul_mono hn e

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

Goal state before:
pp: case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
y r s g : R
h : ¬g = 0
hs : y = gcd (g * r) y * s
⊢ g * (g * r * y / g) = g * r * y

Tactic:
rw [mul_assoc, mul_div_cancel_left₀ _ h]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I : Ideal R
ι : Type u_1
s : Finset ι
J : ι → Ideal R
inst✝ : ∀ (i : ι), (J i).IsTwoSided
h : ∀ i ∈ s, I ⊔ J i = ⊤
i : ι
t : Finset ι
his : i ∈ s
hts : t ⊆ s
hit : i ∉ t
eq_top : I ⊔ ⨅ i ∈ t, J i = ⊤
⊢ ⊤ ≤ I ⊔ (⨅ x ∈ t, J x) * J i

Tactic:
simpa only [sup_mul_eq_of_coprime_right (h _ his)] using eq_top.ge

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
⊢ I ^ n = ⊤ ↔ I = ⊤ ∨ n = 0

Tactic:
by
  refine ⟨fun h ↦ or_iff_not_imp_right.mpr
      fun hn ↦ (eq_top_iff_one _).mpr <| pow_le_self hn <| (eq_top_iff_one _).mp h, ?_⟩
  rintro (h | h)
  · rw [h, top_pow]
  · rw [h, Submodule.pow_zero, one_eq_top]

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

Goal state before:
pp: case succ.zero
R : Type u
inst✝ : Semiring R
ih : 0 ≠ 0 → ↑0 = ⊤
hn : 0 + 1 ≠ 0
⊢ ↑(0 + 1) = ⊤

Tactic:
Nat.cast_one,

Goal state after:
case succ.zero
R : Type u
inst✝ : Semiring R
ih : 0 ≠ 0 → ↑0 = ⊤
hn : 0 + 1 ≠ 0
⊢ 1 = ⊤
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this✝ : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ J.IsPrime}
hJ' : map f J = j
this : J.IsPrime
⊢ j ∈ {J | map f I ≤ J ∧ J.IsPrime}

Tactic:
exact ⟨hJ' ▸ map_mono hJ.left, hJ' ▸ map_isPrime_of_surjective hf (le_trans h hJ.left)⟩

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
f : β → α
inst✝ : DecidableEq β
g : γ → β
s : Finset γ
⊢ (image g s).lcm f = s.lcm (f ∘ g)

Tactic:
induction s using Finset.induction

Goal state after:
case empty
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
f : β → α
inst✝ : DecidableEq β
g : γ → β
⊢ (image g ∅).lcm f = ∅.lcm (f ∘ g)

case insert
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
f : β → α
inst✝ : DecidableEq β
g : γ → β
a✝² : γ
s✝ : Finset γ
a✝¹ : a✝² ∉ s✝
a✝ : (image g s✝).lcm f = s✝.lcm (f ∘ g)
⊢ (image g (insert a✝² s✝)).lcm f = (insert a✝² s✝).lcm (f ∘ g)
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
f : β → α
inst✝ : DecidableEq β
g : γ → β
s : Finset γ
⊢ (image g s).gcd f = s.gcd (f ∘ g)

Tactic:
induction s using Finset.induction

Goal state after:
case empty
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
f : β → α
inst✝ : DecidableEq β
g : γ → β
⊢ (image g ∅).gcd f = ∅.gcd (f ∘ g)

case insert
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
f : β → α
inst✝ : DecidableEq β
g : γ → β
a✝² : γ
s✝ : Finset γ
a✝¹ : a✝² ∉ s✝
a✝ : (image g s✝).gcd f = s✝.gcd (f ∘ g)
⊢ (image g (insert a✝² s✝)).gcd f = (insert a✝² s✝).gcd (f ∘ g)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
s : Finset ι
J : ι → Ideal R
h : ∀ i ∈ s, J i ⊔ I = ⊤
⊢ (∏ i ∈ s, J i) ⊔ I = ⊤

Tactic:
by rw [sup_comm, sup_prod_eq_top]; intro i hi; rw [sup_comm, h i hi]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
b : α
h : b ∈ f
⊢ (b * ↑u ::ₘ f.erase b).prod = f.prod * ↑u

Tactic:
· rw [Multiset.prod_cons, mul_comm b, mul_assoc, Multiset.prod_erase h, mul_comm]

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

Goal state before:
pp: ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
a b i j : ι
hfji : f j ≤ f i
u : Finset ι
hju : j ∉ u
hit : i ∉ insert j u
hn : (insert j u).card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ insert i ↑(insert j u), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ insert j u, (f x).IsPrime
hjt : j ∈ insert j u
hp' : ∀ k ∈ insert i u, (f k).IsPrime
hiu : i ∉ u
hn' : (insert i u).card = n
⊢ ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ k ∈ insert i ↑u, ↑(f k)

Tactic:
rw [Finset.coe_insert] at h

Goal state after:
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
a b i j : ι
hfji : f j ≤ f i
u : Finset ι
hju : j ∉ u
hit : i ∉ insert j u
hn : (insert j u).card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ insert i (insert j ↑u), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ insert j u, (f x).IsPrime
hjt : j ∈ insert j u
hp' : ∀ k ∈ insert i u, (f k).IsPrime
hiu : i ∉ u
hn' : (insert i u).card = n
⊢ ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ k ∈ insert i ↑u, ↑(f k)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime
Ht : ¬∃ j ∈ t, f j ≤ f i
Ha : ¬f a ≤ f i
Hb : f b ≤ f i
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
have h' : (I : Set R) ⊆ f a ∪ f i ∪ ⋃ j ∈ (↑t : Set ι), f j := by
        rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_assoc,
          Set.union_assoc (f a : Set R),
          Set.union_eq_self_of_subset_left Hb] at h
        exact h

Goal state after:
case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime
Ht : ¬∃ j ∈ t, f j ≤ f i
Ha : ¬f a ≤ f i
Hb : f b ≤ f i
h' : ↑I ⊆ ↑(f a) ∪ ↑(f i) ∪ ⋃ j ∈ ↑t, ↑(f j)
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case i
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : RankCondition R
ι : Type u_2
inst✝¹ : Fintype ι
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ Surjective ⇑(↑b.repr ∘ₗ Finsupp.linearCombination R Subtype.val)

Tactic:
apply Surjective.comp (g := b.repr.toLinearMap)

Goal state after:
case i.hg
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : RankCondition R
ι : Type u_2
inst✝¹ : Fintype ι
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ Surjective ⇑↑b.repr

case i.hf
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : RankCondition R
ι : Type u_2
inst✝¹ : Fintype ι
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ Surjective ⇑(Finsupp.linearCombination R Subtype.val)
Module: Mathlib.LinearAlgebra.Matrix.Defs

Goal state before:
pp: R : Type u_7
inst✝ : Zero R
m n : ℕ
A : Array R
hA : A.size = m * n
⊢ ofArray A hA = of fun i j ↦ A.getD (n * ↑i + ↑j) 0

Tactic:
ext i j
  have : n * i.val + j.val < m * n := (Fin.mkDivMod i j).isLt
  simp [ofArray, hA, this]

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

Goal state before:
pp: case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this : Nontrivial R
val✝ : Fintype ↑J
⊢ #↑(range ⇑v) ≤ #↑J

Tactic:
rw [← Cardinal.lift_le, Cardinal.mk_range_eq_of_injective v.injective, Cardinal.mk_fintype J]
    convert! Cardinal.lift_le.{v}.2 (basis_le_span' v hJ)
    simp

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
b : Basis ι R M
inst✝ : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
m : i.Maximal
⊢ #κ = #ι

Tactic:
apply le_antisymm
  · exact linearIndependent_le_basis b v i
  · have : Nontrivial R := nontrivial_of_invariantBasisNumber R
    exact infinite_basis_le_maximal_linearIndependent b v i m

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : m → n → α
⊢ ∑ i, ∑ j, single i j (x i j) = of x

Tactic:
ext i j
  rw [← Fintype.sum_prod_type']
  simp [single, Matrix.sum_apply, Matrix.of_apply, ← Prod.mk_inj]

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

Goal state before:
pp: case inr
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j ↦ Commute (single i j 1) M
h✝ : Nonempty n
i : n
⊢ M ∈ Set.range ⇑(scalar n)

Tactic:
refine ⟨M i i, Matrix.ext fun j k => ?_⟩

Goal state after:
case inr
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j ↦ Commute (single i j 1) M
h✝ : Nonempty n
i j k : n
⊢ (scalar n) (M i i) j k = M j k
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: case a.h
ι : Type u_1
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : LinearOrder M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ a ≤ s.sup' hs fun i ↦ f i + a

pp: case h2
ι : Type u_1
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : LinearOrder M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ s.sup' hs f ≤ (s.sup' hs fun i ↦ f i + a) - a

Tactic:
· exact Finset.le_sup'_of_le _ hs.choose_spec le_add_self

Goal state after:
case h2
ι : Type u_1
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : LinearOrder M
inst✝³ : CanonicallyOrderedAdd M
inst✝² : Sub M
inst✝¹ : AddLeftReflectLE M
inst✝ : OrderedSub M
s : Finset ι
f : ι → M
a : M
hs : s.Nonempty
⊢ s.sup' hs f ≤ (s.sup' hs fun i ↦ f i + a) - a
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
a : α
n : ℕ
⊢ toMultiset (single a n) = n • {a}

Tactic:
rw [toMultiset_apply, sum_single_index]; apply zero_nsmul

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

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
P : Type v
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : Small.{w, u} R
inst✝ : Small.{w, v} P
⊢ Projective R P ↔ ∃ M x x_1, ∃ (_ : Free R M), ∃ i s, s ∘ₗ i = LinearMap.id

Tactic:
let e : (Shrink.{w, v} P →₀ Shrink.{w, u} R) ≃ₗ[R] P →₀ R :=
    Finsupp.mapDomain.linearEquiv _ R (equivShrink P).symm ≪≫ₗ
      Finsupp.mapRange.linearEquiv (Shrink.linearEquiv R R)

Goal state after:
R : Type u
inst✝⁴ : Semiring R
P : Type v
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : Small.{w, u} R
inst✝ : Small.{w, v} P
e : (Shrink.{w, v} P →₀ Shrink.{w, u} R) ≃ₗ[R] P →₀ R :=
  mapDomain.linearEquiv (Shrink.{w, u} R) R (equivShrink P).symm ≪≫ₗ mapRange.linearEquiv (Shrink.linearEquiv R R)
⊢ Projective R P ↔ ∃ M x x_1, ∃ (_ : Free R M), ∃ i s, s ∘ₗ i = LinearMap.id
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
u : Rˣ
⊢ (star ↑u)⁻¹ʳ = star (↑u)⁻¹ʳ

Tactic:
rw [Ring.inverse_unit, ← Units.coe_star, Ring.inverse_unit, ← Units.coe_star_inv]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
a : R
⊢ IsIdempotentElem (star a) ↔ IsIdempotentElem a

Tactic:
simp [IsIdempotentElem, ← star_mul]

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

Goal state before:
pp: case pos
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
b : n → α
inst✝ : DecidableEq m
i' : m
h : i' = i
⊢ M.updateRow i b i' j = if i' = i then b j else M i' j

pp: case neg
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
b : n → α
inst✝ : DecidableEq m
i' : m
h : ¬i' = i
⊢ M.updateRow i b i' j = if i' = i then b j else M i' j

Tactic:
· rw [h, updateRow_self, if_pos rfl]

Goal state after:
case neg
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
b : n → α
inst✝ : DecidableEq m
i' : m
h : ¬i' = i
⊢ M.updateRow i b i' j = if i' = i then b j else M i' j
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inr.inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j k : n
hjk : j ≠ k
hki : k ≠ i
⊢ (diagonal v).updateCol i (Pi.single i x) j k = 0

Tactic:
rw [updateCol_ne hki, diagonal_apply_ne _ hjk]

Goal state after:
Module: Mathlib.Algebra.AffineMonoid.Irreducible

Goal state before:
pp: M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m : M → ℕ
hm : ∏ a ∈ S, a ^ m a = a
n : M → ℕ
hn : ∏ a ∈ S, a ^ n a = b
⊢ ∏ a ∈ S, a ^ m a = r ^ m r * ∏ s ∈ S.erase r, s ^ m s

Tactic:
← Finset.mul_prod_erase _ _ hrS

Goal state after:
M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m : M → ℕ
hm : ∏ a ∈ S, a ^ m a = a
n : M → ℕ
hn : ∏ a ∈ S, a ^ n a = b
⊢ r ^ m r * ∏ x ∈ S.erase r, x ^ m x = r ^ m r * ∏ s ∈ S.erase r, s ^ m s
Module: Mathlib.Algebra.AffineMonoid.Irreducible

Goal state before:
pp: M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hn : ∏ a ∈ S, a ^ n a = b
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
⊢ ∏ a ∈ S, a ^ n a = r ^ n r * ∏ s ∈ S.erase r, s ^ n s

Tactic:
← Finset.mul_prod_erase _ _ hrS

Goal state after:
M : Type u_1
inst✝² : CancelCommMonoid M
inst✝¹ : Subsingleton Mˣ
inst✝ : Monoid.FG M
S : Finset M
hSgen : closure ↑S = ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun S ↦ closure ↑S = ⊤) y → y ⊆ S → S ⊆ y
r : M
hrS : r ∈ ↑S
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ x x_1, ∃ (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hn : ∏ a ∈ S, a ^ n a = b
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
⊢ r ^ n r * ∏ x ∈ S.erase r, x ^ n x = r ^ n r * ∏ s ∈ S.erase r, s ^ n s
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case c.c.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₂ : X
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
⊢ (sa • r₁ + ra • r₂) /ₒ (sa * s₁) + r₃ /ₒ s₃ = r₁ /ₒ s₁ + (r₂ /ₒ s₂ + r₃ /ₒ s₃)

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

Goal state after:
case c.c.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₂ : X
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * ↑(sa * s₁) = rc * ↑s₃
q : (sa • r₁ + ra • r₂) /ₒ (sa * s₁) + r₃ /ₒ s₃ = (sc • (sa • r₁ + ra • r₂) + rc • r₃) /ₒ (sc * (sa * s₁))
⊢ (sa • r₁ + ra • r₂) /ₒ (sa * s₁) + r₃ /ₒ s₃ = r₁ /ₒ s₁ + (r₂ /ₒ s₂ + r₃ /ₒ s₃)
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
l : Type u_3
m : Type u_4
n : Type u_5
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
f : (n → R) →ₗ[R] m → R
g : (l → R) →ₗ[R] n → R
this : f ∘ₗ g = toLin' (toMatrix' f * toMatrix' g)
⊢ toMatrix' (f ∘ₗ g) = toMatrix' f * toMatrix' g

Tactic:
by
    rw [this, LinearMap.toMatrix'_toLin']

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁷ : Fintype n
inst✝⁶ : Finite m
inst✝⁵ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₁
inst✝¹ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝ : DecidableEq M₁
f : M₁ →ₗ[R] M₂
k : m
i : n
⊢ (v₂.reindexRange.repr (f (v₁.reindexRange ⟨v₁ i, ⋯⟩))) ⟨v₂ k, ⋯⟩ = (v₂.repr (f (v₁ i))) k

Tactic:
Basis.reindexRange_self,

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁷ : Fintype n
inst✝⁶ : Finite m
inst✝⁵ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₁
inst✝¹ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝ : DecidableEq M₁
f : M₁ →ₗ[R] M₂
k : m
i : n
⊢ (v₂.reindexRange.repr (f (v₁ i))) ⟨v₂ k, ⋯⟩ = (v₂.repr (f (v₁ i))) k
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommMonoid X
inst✝ : Module R X
y z : OreLocalization S R
x : OreLocalization S X
⊢ (y + z) • x = y • x + z • x

Tactic:
induction x with | _ r₁ s₁
  induction y with | _ r₂ s₂
  induction z with | _ r₃ s₃
  rcases oreDivAddChar' r₂ r₃ s₂ s₃ with ⟨ra, sa, ha, q⟩
  rw [q]
  clear q
  rw [OreLocalization.expand' r₂ s₂ sa]
  rcases oreDivSMulChar' (sa • r₂) r₁ (sa * s₂) s₁ with ⟨rb, sb, hb, q⟩
  rw [q]
  clear q
  have hs₃rasb : sb * ra * s₃ ∈ S := by
    rw [mul_assoc, ← ha]
    norm_cast
    apply SetLike.coe_mem
  rw [OreLocalization.expand _ _ _ hs₃rasb]
  have ha' : ↑((sb * sa) * s₂) = sb * ra * s₃ := by simp [ha, mul_assoc]
  rw [← Subtype.coe_eq_of_eq_mk ha']
  rcases oreDivSMulChar' ((sb * ra) • r₃) r₁ (sb * sa * s₂) s₁ with ⟨rc, sc, hc, hc'⟩
  rw [hc']
  rw [oreDiv_add_char _ _ 1 sc (by simp [mul_assoc])]
  rw [OreLocalization.expand' (sa • r₂ + ra • r₃) (sa * s₂) (sc * sb)]
  simp only [smul_eq_mul, one_smul, Submonoid.smul_def, mul_add, Submonoid.coe_mul] at hb hc ⊢
  rw [mul_assoc, hb, mul_assoc, ← mul_assoc _ ra, hc, ← mul_assoc, ← add_mul]
  rw [OreLocalization.smul_cancel']
  simp only [add_smul, ← mul_assoc, smul_smul]

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
n : Type u_4
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
M₁ : Type u_5
inst✝² : AddCommMonoid M₁
inst✝¹ : Module R M₁
v₁ : Basis n R M₁
inst✝ : DecidableEq M₁
f : M₁ →ₗ[R] M₁
k i : n
⊢ (v₁.reindexRange.repr (f (v₁.reindexRange ⟨v₁ i, ⋯⟩))) ⟨v₁ k, ⋯⟩ = (v₁.repr (f (v₁ i))) k

Tactic:
Basis.reindexRange_self,

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
n : Type u_4
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
M₁ : Type u_5
inst✝² : AddCommMonoid M₁
inst✝¹ : Module R M₁
v₁ : Basis n R M₁
inst✝ : DecidableEq M₁
f : M₁ →ₗ[R] M₁
k i : n
⊢ (v₁.reindexRange.repr (f (v₁ i))) ⟨v₁ k, ⋯⟩ = (v₁.repr (f (v₁ i))) k
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✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
inst✝¹ : Fintype ι
s : ι → M
hs : span R (range s) = ⊤
inst✝ : IsTorsionFree R M
⊢ (n : ℕ) × Basis (Fin n) R M

Tactic:
have := exists_maximal_linearIndepOn R s
    let I : Set ι := this.choose
    obtain
      ⟨indepI : LinearIndependent R (s ∘ (fun x => x) : I → M), hI :
        ∀ i ∉ I, ∃ a : R, a ≠ 0 ∧ a • s i ∈ span R (s '' I)⟩ :=
      this.choose_spec
    let N := span R (range <| (s ∘ (fun x => x) : I → M))
    -- same as `span R (s '' I)` but more convenient
    let _sI : I → N := fun i ↦ ⟨s i.1, subset_span (mem_range_self i)⟩
    -- `s` restricted to `I` is a basis of `N`
    let sI_basis : Basis I R N := Basis.span indepI
    -- Our first goal is to build `A ≠ 0` such that `A • M ⊆ N`
    have exists_a : ∀ i : ι, ∃ a : R, a ≠ 0 ∧ a • s i ∈ N := by
      intro i
      by_cases hi : i ∈ I
      · use 1, zero_ne_one.symm
        rw [one_smul]
        exact subset_span (mem_range_self (⟨i, hi⟩ : I))
      · simpa [image_eq_range s I] using! hI i hi
    choose a ha ha' using exists_a
    let A := ∏ i, a i
    have hA : A ≠ 0 := by
      rw [Finset.prod_ne_zero_iff]
      simpa using! ha
    -- `M ≃ A • M` because `M` is torsion free and `A ≠ 0`
    let φ : M →ₗ[R] M := LinearMap.lsmul R M A
    have : LinearMap.ker φ = ⊥ := LinearMap.ker_lsmul hA
    let ψ := LinearEquiv.ofInjective φ (LinearMap.ker_eq_bot.mp this)
    have : LinearMap.range φ ≤ N := by
      -- as announced, `A • M ⊆ N`
      suffices ∀ i, φ (s i) ∈ N by
        rw [LinearMap.range_eq_map, ← hs, map_span_le]
        rintro _ ⟨i, rfl⟩
        apply this
      intro i
      calc
        (∏ j ∈ {i}ᶜ, a j) • a i • s i ∈ N := N.smul_mem _ (ha' i)
        _ = (∏ j, a j) • s i := by rw [Fintype.prod_eq_prod_compl_mul i, mul_smul]
    -- Since a submodule of a free `R`-module is free, we get that `A • M` is free
    obtain ⟨n, b : Basis (Fin n) R (LinearMap.range φ)⟩ := Submodule.basisOfPidOfLE this sI_basis
    -- hence `M` is free.
    exact ⟨n, b.map ψ.symm⟩

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

Goal state before:
pp: case surj
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✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
⊢ ∀ (z : P), ∃ x, z * (algebraMap R P) ↑x.2 = (algebraMap R P) x.1

Tactic:
intro y
    obtain ⟨⟨x, s⟩, e⟩ := IsLocalization.surj M (h.symm y)
    apply_fun (show S → P from h) at e
    simp only [map_mul, h.apply_symm_apply, h.commutes] at e
    exact ⟨⟨x, s⟩, e⟩

Goal state after: