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

Goal state before:
pp: R : Type u
inst✝² : Semiring R
inst✝¹ : NoZeroDivisors R
I J : Ideal R
inst✝ : I.IsTwoSided
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ ⊥ < I ⊓ J

Tactic:
← mul_le_inf,

Goal state after:
R : Type u
inst✝² : Semiring R
inst✝¹ : NoZeroDivisors R
I J : Ideal R
inst✝ : I.IsTwoSided
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ ⊥ < I * J
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n✝ n : ℕ
ih : ⊤ ^ n = ⊤
⊢ ⊤ ^ n.succ = ⊤

Tactic:
by rw [Submodule.pow_succ, ih, top_mul]

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

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
h : b ∈ s
⊢ (insert b s).lcm f = GCDMonoid.lcm (f b) (s.lcm f)

Tactic:
insert_eq_of_mem h,

Goal state after:
case pos
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
h : b ∈ s
⊢ s.lcm f = GCDMonoid.lcm (f b) (s.lcm f)
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
⊢ (insert b s).lcm f = GCDMonoid.lcm (f b) (s.lcm f)

Tactic:
by_cases h : b ∈ s
  · rw [insert_eq_of_mem h,
      (lcm_eq_right_iff (f b) (s.lcm f) (Multiset.normalize_lcm (s.1.map f))).2 (dvd_lcm h)]
  apply fold_insert h

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
⊢ normalize (s.lcm f) = s.lcm f

Tactic:
simp [lcm_def]

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

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
h : b ∈ s
⊢ (insert b s).gcd f = GCDMonoid.gcd (f b) (s.gcd f)

Tactic:
insert_eq_of_mem h,

Goal state after:
case pos
α : Type u_2
β : Type u_3
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
h : b ∈ s
⊢ s.gcd f = GCDMonoid.gcd (f b) (s.gcd f)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
hI : I.IsRadical
hJ : J.IsRadical
⊢ (I ⊓ J).IsRadical

Tactic:
rw [IsRadical, radical_inf]

Goal state after:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
hI : I.IsRadical
hJ : J.IsRadical
⊢ I.radical ⊓ J.radical ≤ I ⊓ J
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
⊢ IsPrimal 0

pp: case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : a ≠ 0
⊢ IsPrimal a

Tactic:
· exact isPrimal_zero

Goal state after:
case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : a ≠ 0
⊢ IsPrimal a
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
h : I ^ n ≤ P
⊢ I ≤ P

Tactic:
by
  by_cases hn : n = 0
  · rw [hn, pow_zero, one_eq_top] at h
    exact fun ⦃_⦄ _ ↦ h Submodule.mem_top
  · exact (pow_le_iff hn).mp h

Goal state after:
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

pp: case neg
ι : 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
      specialize ih hp.2 hn h'
      rcases ih with (ih | ih | ⟨k, hkt, ih⟩)
      · exact Or.inl ih
      · exact Or.inr (Or.inr ⟨i, Finset.mem_insert_self i t, ih⟩)
      · exact Or.inr (Or.inr ⟨k, Finset.mem_insert_of_mem hkt, ih⟩)

Goal state after:
case neg
ι : 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
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
n : Type u_4
m : Type u_5
inst✝¹ : Fintype n
inst✝ : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis m R ↥I
a : ↥I
ha : a ≠ 0
hb : ∀ (g : n → R), ∑ i, g i • b i = 0 → ∀ (i : n), g i = 0
g : n → R
hg : ∑ i, g i • b i • a = 0
⊢ ∀ (i : n), g i = 0

Tactic:
apply hb g

Goal state after:
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : StrongRankCondition R
inst✝⁴ : Ring S
inst✝³ : IsDomain S
inst✝² : Algebra R S
n : Type u_4
m : Type u_5
inst✝¹ : Fintype n
inst✝ : Fintype m
b : Basis n R S
I : Ideal S
hI : I ≠ ⊥
c : Basis m R ↥I
a : ↥I
ha : a ≠ 0
hb : ∀ (g : n → R), ∑ i, g i • b i = 0 → ∀ (i : n), g i = 0
g : n → R
hg : ∑ i, g i • b i • a = 0
⊢ ∑ i, g i • b i = 0
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → diagonal v i j * w j = 0
⊢ diagonal v i ⬝ᵥ w = v i * w i

Tactic:
convert! Finset.sum_eq_single i (fun j _ => this j) _ using 1 <;> simp

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → v j * diagonal w i j = 0
⊢ v ⬝ᵥ diagonal w i = v i * w i

Tactic:
convert! Finset.sum_eq_single i (fun j _ => this j) _ using 1 <;> simp

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → v j * diagonal w j i = 0
⊢ (v ⬝ᵥ fun j ↦ diagonal w j i) = v i * w i

Tactic:
convert! Finset.sum_eq_single i (fun j _ => this j) _ using 1 <;> simp

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
x : α
i : m
this : ∀ (j : m), j ≠ i → Pi.single i x j * v j = 0
⊢ Pi.single i x ⬝ᵥ v = x * v i

Tactic:
convert! Finset.sum_eq_single i (fun j _ => this j) _ using 1 <;> simp

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
x : α
i : m
this : ∀ (j : m), j ≠ i → v j * Pi.single i x j = 0
⊢ v ⬝ᵥ Pi.single i x = v i * x

Tactic:
convert! Finset.sum_eq_single i (fun j _ => this j) _ using 1 <;> simp

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

Goal state before:
pp: n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
⊢ Pi.single j x ᵥ* diagonal v = Pi.single j (x * v j)

Tactic:
ext i
  rw [vecMul_diagonal]
  exact Pi.apply_single (fun i x => x * v i) (fun i => zero_mul _) j x i

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Basic

Goal state before:
pp: case intro.intro
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Finite ι₁
inst✝ : Finite ι₂
val✝¹ : Fintype ι₁
val✝ : Fintype ι₂
⊢ Module.Finite R (Matrix ι₁ ι₂ M)

Tactic:
exact Module.Finite.of_basis <| (Free.chooseBasis _ _).matrix _ _

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype n
⊢ Function.Injective mulVec

Tactic:
intro A

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype n
A : Matrix m n α
⊢ ∀ ⦃a₂ : Matrix m n α⦄, A.mulVec = a₂.mulVec → A = a₂
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype m
⊢ Function.Injective fun x v ↦ v ᵥ* x

Tactic:
intro A

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype m
A : Matrix m n α
⊢ ∀ ⦃a₂ : Matrix m n α⦄, (fun x v ↦ v ᵥ* x) A = (fun x v ↦ v ᵥ* x) a₂ → A = a₂
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype m
⊢ Function.Injective fun x v ↦ v ᵥ* x

Tactic:
intro A B h
  ext i j
  classical
  simpa using congrFun₂ h (Pi.single i 1) j

Goal state after:
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]

Goal state after:
α : Type u_1
a : α
n : ℕ
⊢ 0 • {a} = 0
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
⊢ (toMultiset 0).toFinset = support 0

Tactic:
rw [toMultiset_zero, Multiset.toFinset_zero, support_zero]

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✝⁶ : NonUnitalNonAssocSemiring B
inst✝⁵ : NonUnitalNonAssocSemiring C
inst✝⁴ : Module R A
inst✝³ : Module R B
inst✝² : Module R C
S✝ : NonUnitalSubalgebra R A
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
f : F
S : NonUnitalSubalgebra R A
r : R
b : B
hb : b ∈ (NonUnitalSubsemiring.map (↑f) S.toNonUnitalSubsemiring).carrier
⊢ r • b ∈ (NonUnitalSubsemiring.map (↑f) S.toNonUnitalSubsemiring).carrier

Tactic:
by
      rcases hb with ⟨a, ha, rfl⟩
      exact map_smulₛₗ f r a ▸ Set.mem_image_of_mem f (S.smul_mem' r ha)

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
S : NonUnitalSubalgebra R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : NonUnitalSubalgebra R A
hT : T = iSup K
⊢ ↥T →ₙₐ[R] B

Tactic:
subst hT

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
S : NonUnitalSubalgebra R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
⊢ ↥(iSup K) →ₙₐ[R] B
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case a
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ Submonoid.closure s ≤ (adjoin R s).toSubmonoid

Tactic:
exact Submonoid.closure_le.2 subset_adjoin

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

Goal state before:
pp: 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✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : NonUnitalSubalgebra R A
hT : T = iSup K
i : ι
x : ↥(K i)
hx : ↑x ∈ T
⊢ (iSupLift K dir f hf T hT) ⟨↑x, hx⟩ = (f i) x

Tactic:
subst hT

Goal state after:
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✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i : ι
x : ↥(K i)
hx : ↑x ∈ iSup K
⊢ (iSupLift K dir f hf (iSup K) ⋯) ⟨↑x, hx⟩ = (f i) x
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: 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✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : NonUnitalSubalgebra R A
hT : T = iSup K
i : ι
x : ↥T
hx : ↑x ∈ K i
⊢ (iSupLift K dir f hf T hT) x = (f i) ⟨↑x, hx⟩

Tactic:
subst hT

Goal state after:
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✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i : ι
x : ↥(iSup K)
hx : ↑x ∈ K i
⊢ (iSupLift K dir f hf (iSup K) ⋯) x = (f i) ⟨↑x, hx⟩
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b c : A
⊢ r • (a * (b * c)) = r • (a * b * c)

Tactic:
ha.left_assoc

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b c : A
⊢ r • (a * b * c) = r • (a * b * c)
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
m : M
p : ι →₀ N
⊢ (finsuppRight R S M N ι) (m ⊗ₜ[R] p) = p.sum fun i n ↦ Finsupp.single i (m ⊗ₜ[R] n)

Tactic:
by
  induction p using Finsupp.induction_linear with
  | zero => simp
  | add f g hf hg => simp [tmul_add, map_add, hf, hg, Finsupp.sum_add_index]
  | single => simp [finsuppRight]

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

Goal state before:
pp: case H
R : Type u
inst✝¹⁰ : Semiring R
P : Type v
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
R₀ : Type u_2
M : Type u_1
N : Type u_3
inst✝⁷ : CommSemiring R₀
inst✝⁶ : Algebra R₀ R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R₀ M
inst✝³ : Module R M
inst✝² : IsScalarTower R₀ R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R₀ N
sM : M →ₗ[R] M →₀ R
hsM : Function.LeftInverse ⇑(linearCombination R id) ⇑sM
sN : N →ₗ[R₀] N →₀ R₀
hsN : Function.LeftInverse ⇑(linearCombination R₀ id) ⇑sN
⊢ AlgebraTensorModule.map (linearCombination R id) LinearMap.id ∘ₗ AlgebraTensorModule.map sM LinearMap.id =
    LinearMap.id

Tactic:
· ext; simp [hsM _]

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
inst✝¹ : StarRing R
S : Type u_1
inst✝ : NonAssocSemiring S
x✝¹ : S →+* R
x✝ : S
⊢ ((fun f ↦ (starRingEnd R).comp f) ((fun f ↦ (starRingEnd R).comp f) x✝¹)) x✝ = x✝¹ x✝

Tactic:
simp only [RingHom.coe_comp, Function.comp_apply, starRingEnd_self_apply]

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

Goal state before:
pp: n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M : Matrix n n α
v : n → α
⊢ M = (diagonal v).map star ↔ M = diagonal (star v)

Tactic:
rw [map_diagonal_star]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬⊥ < Submodule.map ψ N
inst✝ : (Submodule.map ϕ N).IsPrincipal
hgen : generator (Submodule.map ϕ N) = 0
x : M
hx : x ∈ N
i : ι
⊢ (b.repr x) i = (b.repr 0) i

Tactic:
rw [map_zero, Finsupp.zero_apply]

Goal state after:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
N : Submodule R M
ϕ : M →ₗ[R] R
hϕ : ∀ (ψ : M →ₗ[R] R), ¬⊥ < Submodule.map ψ N
inst✝ : (Submodule.map ϕ N).IsPrincipal
hgen : generator (Submodule.map ϕ N) = 0
x : M
hx : x ∈ N
i : ι
⊢ (b.repr x) i = 0
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
N O : Submodule R M
b : Basis ι R ↥O
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬⊥ < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
hgen : generator (ϕ.submoduleImage N) = 0
x : M
hx : x ∈ N
i : ι
⊢ (b.repr ⟨x, ⋯⟩) i = (b.repr 0) i

Tactic:
rw [map_zero, Finsupp.zero_apply]

Goal state after:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
N O : Submodule R M
b : Basis ι R ↥O
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬⊥ < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
hgen : generator (ϕ.submoduleImage N) = 0
x : M
hx : x ∈ N
i : ι
⊢ (b.repr ⟨x, ⋯⟩) i = 0
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₂ • ψ
⊢ R ∙ d ≤ ψ'.submoduleImage N

Tactic:
rw [span_le, singleton_subset_iff, SetLike.mem_coe, LinearMap.mem_submoduleImage_of_le hNO]

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₂ • ψ
⊢ ∃ y, ∃ (yN : y ∈ N), ψ' ⟨y, ⋯⟩ = d
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
r₁ : X
s₁ : ↥S
r₂ : X
s₂ sb : ↥S
rb : R
hb : sb • (r₂, s₂).fst = rb • (r₁, s₁).fst
hb' : ↑sb * ↑(r₂, s₂).snd = rb * ↑(r₁, s₁).snd
⊢ add' (r₁, s₁).fst (r₁, s₁).snd x = add' (r₂, s₂).fst (r₂, s₂).snd x

Tactic:
induction x with | _ r₃ s₃

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₂ : X
s₂ sb : ↥S
rb : R
hb : sb • (r₂, s₂).fst = rb • (r₁, s₁).fst
hb' : ↑sb * ↑(r₂, s₂).snd = rb * ↑(r₁, s₁).snd
r₃ : X
s₃ : ↥S
⊢ add' (r₁, s₁).fst (r₁, s₁).snd (r₃ /ₒ s₃) = add' (r₂, s₂).fst (r₂, s₂).snd (r₃ /ₒ 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
⊢ f (f.sec 0).1 = 0

Tactic:
rw [LocalizationMap.sec_spec', mul_zero]

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

Goal state before:
pp: case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddGroup X
inst✝ : DistribMulAction R X
r : X
s : ↥S
⊢ -(r /ₒ s) + r /ₒ s = 0

Tactic:
| _ r s => 

Goal state after:
case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddGroup X
inst✝ : DistribMulAction R X
r : X
s : ↥S
⊢ -(r /ₒ s) + r /ₒ s = 0
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
ι₁ : Type u_6
ι₂ : Type u_7
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Fintype ι₁
inst✝¹ : Fintype ι₂
inst✝ : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
ij : ι₂ × ι₁
k : ι₁
this : DecidableEq ι₂
⊢ (if ij.1 ∈ Finset.univ then if ij.2 = k then b₂ ij.1 else 0 else 0) = if ij.2 = k then b₂ ij.1 else 0

Tactic:
Finset.mem_univ,

Goal state after:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
ι₁ : Type u_6
ι₂ : Type u_7
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Fintype ι₁
inst✝¹ : Fintype ι₂
inst✝ : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
ij : ι₂ × ι₁
k : ι₁
this : DecidableEq ι₂
⊢ (if True then if ij.2 = k then b₂ ij.1 else 0 else 0) = if ij.2 = k then b₂ ij.1 else 0
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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm✝ : (c.sum fun i x ↦ x • ↑(snf.bN i)) ∈ N
hm : ⟨c.sum fun i t ↦ t • ↑(snf.bN i), hm✝⟩ = c.sum fun i t ↦ t • ⟨↑(snf.bN i), ⋯⟩
⊢ c i = 0 → 0 = snf.a i * c i

Tactic:
exact fun a ↦ (mul_eq_zero_of_right _ a).symm

Goal state after: