mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case inl
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : TwoUniqueProds G
A B : Finset H
hc : 1 < #A * #B
hc' : 1 < #(image (⇑f) A) * #(image (⇑f) B)
a1 b1 : G
h1 : (a1, b1) ∈ image (⇑f) A ×ˢ image (⇑f) B
a2 b2 : G
h2 : (a2, b2) ∈ image (⇑f) A ×ˢ image (⇑f) B
hne : (a1, b1) ≠ (a2, b2)
hu1 : UniqueMul (image (⇑f) A) (image (⇑f) B) (a1, b1).1 (a1, b1).2
hu2 : UniqueMul (image (⇑f) A) (image (⇑f) B) (a2, b2).1 (a2, b2).2
⊢ ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
simp_rw [mem_product, mem_image] at h1 h2 ⊢

Goal state after:
case inl
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : TwoUniqueProds G
A B : Finset H
hc : 1 < #A * #B
hc' : 1 < #(image (⇑f) A) * #(image (⇑f) B)
a1 b1 a2 b2 : G
hne : (a1, b1) ≠ (a2, b2)
hu1 : UniqueMul (image (⇑f) A) (image (⇑f) B) (a1, b1).1 (a1, b1).2
hu2 : UniqueMul (image (⇑f) A) (image (⇑f) B) (a2, b2).1 (a2, b2).2
h1 : (∃ a ∈ A, f a = a1) ∧ ∃ a ∈ B, f a = b1
h2 : (∃ a ∈ A, f a = a2) ∧ ∃ a ∈ B, f a = b2
⊢ ∃ p1,
    (p1.1 ∈ A ∧ p1.2 ∈ B) ∧ ∃ p2, (p2.1 ∈ A ∧ p2.2 ∈ B) ∧ p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: case disjoint
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x : E
hpx : x ∈ ↑p
hfx : x ∈ ↑f.ker
⊢ x ∈ ⊥

Tactic:
SetLike.mem_coe,

Goal state after:
case disjoint
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x : E
hpx : x ∈ ↑p
hfx : x ∈ f.ker
⊢ x ∈ ⊥
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
a : ℕ∞
inst✝ : Nonempty ι
f : ι → ℕ∞
⊢ a + ⨆ i, f i = ⨆ i, a + f i

Tactic:
obtain rfl | ha := eq_or_ne a ⊤

Goal state after:
case inl
ι : Sort u_2
inst✝ : Nonempty ι
f : ι → ℕ∞
⊢ ⊤ + ⨆ i, f i = ⨆ i, ⊤ + f i

case inr
ι : Sort u_2
a : ℕ∞
inst✝ : Nonempty ι
f : ι → ℕ∞
ha : a ≠ ⊤
⊢ a + ⨆ i, f i = ⨆ i, a + f i
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: E : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
T f : E →ₗ[R] E
hf : IsIdempotentElem f
⊢ Commute f T ↔ f.range ∈ Module.End.invtSubmodule T ∧ f.ker ∈ Module.End.invtSubmodule T

Tactic:
by
  simp_rw [hf.range_mem_invtSubmodule_iff, hf.ker_mem_invtSubmodule_iff, ← Module.End.mul_eq_comp]
  exact ⟨fun h => (by simp [← h.eq, ← mul_assoc, hf.eq]), fun ⟨h1, h2⟩ => h2.symm.trans h1⟩

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ height (f x) = height x

Tactic:
by
  apply le_antisymm
  · simpa using height_le_height_apply_of_strictMono _ f.symm.strictMono (f x)
  · exact height_le_height_apply_of_strictMono _ f.strictMono x

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
⊢ -0 + 0 = 0

Tactic:
rw [add_zero]

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
⊢ -0 = 0
Module: Mathlib.Algebra.Module.Submodule.Finsupp

Goal state before:
pp: α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
sR : Set R
s✝ : Set S
N : Submodule R M
inst✝ : SMulCommClass R R M
s t : Set R
x : Submodule R M
r : R
m : M
hr : r ∈ s
hm : m ∈ t • x
⊢ r • m ∈ (s * t) • x

Tactic:
have : SMulCommClass R R x := ⟨fun r s m => Subtype.ext <| smul_comm _ _ _⟩

Goal state after:
α : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
sR : Set R
s✝ : Set S
N : Submodule R M
inst✝ : SMulCommClass R R M
s t : Set R
x : Submodule R M
r : R
m : M
hr : r ∈ s
hm : m ∈ t • x
this : SMulCommClass R R ↥x
⊢ r • m ∈ (s * t) • x
Module: Mathlib.LinearAlgebra.TensorProduct.Map

Goal state before:
pp: R : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
B' : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A'
inst✝² : AddCommMonoid B'
inst✝¹ : Module R A'
inst✝ : Module R B'
eA : A ≃ A'
eB : B ≃ B'
x : A ⊗[R] B
⊢ (TensorProduct.comm R A B) x =
    (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
        (TensorProduct.comm R A' B' ≪≫ₗ TensorProduct.congr (linearEquiv R eB).symm (linearEquiv R eA).symm))
      x

Tactic:
induction x

Goal state after:
case zero
R : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
B' : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A'
inst✝² : AddCommMonoid B'
inst✝¹ : Module R A'
inst✝ : Module R B'
eA : A ≃ A'
eB : B ≃ B'
⊢ (TensorProduct.comm R A B) 0 =
    (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
        (TensorProduct.comm R A' B' ≪≫ₗ TensorProduct.congr (linearEquiv R eB).symm (linearEquiv R eA).symm))
      0

case tmul
R : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
B' : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A'
inst✝² : AddCommMonoid B'
inst✝¹ : Module R A'
inst✝ : Module R B'
eA : A ≃ A'
eB : B ≃ B'
x✝ : A
y✝ : B
⊢ (TensorProduct.comm R A B) (x✝ ⊗ₜ[R] y✝) =
    (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
        (TensorProduct.comm R A' B' ≪≫ₗ TensorProduct.congr (linearEquiv R eB).symm (linearEquiv R eA).symm))
      (x✝ ⊗ₜ[R] y✝)

case add
R : Type u_1
A : Type u_2
A' : Type u_3
B : Type u_4
B' : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A'
inst✝² : AddCommMonoid B'
inst✝¹ : Module R A'
inst✝ : Module R B'
eA : A ≃ A'
eB : B ≃ B'
x✝ y✝ : A ⊗[R] B
a✝¹ :
  (TensorProduct.comm R A B) x✝ =
    (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
        (TensorProduct.comm R A' B' ≪≫ₗ TensorProduct.congr (linearEquiv R eB).symm (linearEquiv R eA).symm))
      x✝
a✝ :
  (TensorProduct.comm R A B) y✝ =
    (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
        (TensorProduct.comm R A' B' ≪≫ₗ TensorProduct.congr (linearEquiv R eB).symm (linearEquiv R eA).symm))
      y✝
⊢ (TensorProduct.comm R A B) (x✝ + y✝) =
    (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB) ≪≫ₗ
        (TensorProduct.comm R A' B' ≪≫ₗ TensorProduct.congr (linearEquiv R eB).symm (linearEquiv R eA).symm))
      (x✝ + y✝)
Module: Mathlib.Tactic.Order.ToInt

Goal state before:
pp: case neg.refine_1
α : Type u_1
inst✝ : LinearOrder α
n : ℕ
val : Fin n → α
li : List α := List.ofFn val
sli : List α := li.mergeSort fun a b ↦ decide (a ≤ b)
this✝ : ∀ (i : Fin n), ∃ j, sli[j] = val i
i j : Fin n
pf✝ : ∀ (j : Fin sli.length), ↑j < sli.length
hi : ∃ j, sli[↑j] = val i
hj : ∃ j_1, sli[↑j_1] = val j
h_eq : ¬sli[↑hi.choose] = sli[↑hj.choose]
this :
  ∀ (i j : Fin (li.mergeSort fun a b ↦ decide (a ≤ b)).length),
    i < j →
      decide ((li.mergeSort fun a b ↦ decide (a ≤ b)).get i ≤ (li.mergeSort fun a b ↦ decide (a ≤ b)).get j) = true
h : ↑hj.choose < ↑hi.choose
⊢ sli[↑hj.choose] < sli[↑hi.choose]

Tactic:
exact lt_of_le_of_ne (by simpa using (this hj.choose hi.choose (by simpa)))
      (fun h ↦ h_eq (h.symm))

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
⊢ (algebraMap R A) r ∈ 1

Tactic:
by
  simp [one_eq_range]

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
⊢ x ∈ 1 ↔ ∃ y, (algebraMap R A) y = x

Tactic:
by
  simp [one_eq_range]

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : Aᵐᵒᵖ
⊢ x ∈ map (↑(opLinearEquiv R)) 1 ↔ x ∈ 1

Tactic:
induction x

Goal state after:
case h
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
X✝ : A
⊢ op X✝ ∈ map (↑(opLinearEquiv R)) 1 ↔ op X✝ ∈ 1
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case cons.mp.refine_2
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ : μ a * ∏ j ∈ t, s j + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
⊢ IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)

Tactic:
have : IsCoprime (s b) (s a) :=
          ⟨μ a * ∏ i ∈ t \ {b}, s i, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j, ?_⟩
        · exact ⟨this.symm, this⟩
        rw [mul_assoc, ← prod_eq_prod_sdiff_singleton_mul hb, sum_mul, ← hμ, sum_congr rfl]
        intro x hx
        rw [mul_assoc]
        congr
        rw [prod_eq_prod_sdiff_singleton_mul (mem x hx) _]
        congr 2
        rw [sdiff_sdiff_comm, sdiff_singleton_eq_erase a, erase_insert hat]

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

Goal state before:
pp: ι : Sort uι
R : Type u
inst✝⁶ : CommSemiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
S✝ T✝ : Set A
M N P Q : Submodule R A
m n : A
α : Type u_1
inst✝³ : Monoid α
inst✝² : DistribMulAction α A
inst✝¹ : SMulCommClass α R A
inst✝ : SMulCommClass α A A
a : α
S T : Submodule R A
⊢ a • S • T = S • a • T

Tactic:
by
    rw [← S.span_eq, ← T.span_eq, smul_span, smul_eq_mul, smul_eq_mul, span_mul_span, span_mul_span,
      smul_span, mul_smul_comm]

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
P : Submodule R A
x y : A
⊢ x ∈ (R ∙ y) * P ↔ ∃ z ∈ P, y * z = x

Tactic:
simp_rw [mul_eq_map₂, map₂_span_singleton_eq_map, mem_map, LinearMap.mul_apply_apply]

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
a : A
M : Submodule R A
⊢ span R (SetSemiring.down (Set.up {a})) * span R ↑M = map (LinearMap.mulLeft R a) M

Tactic:
SetSemiring.down_up,

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
a : A
M : Submodule R A
⊢ (R ∙ a) * span R ↑M = map (LinearMap.mulLeft R a) M
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: case inl.e_I
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
s : Set R
t : Set S
hs : s.Nonempty
ht : t.Nonempty
⊢ map (RingHom.fst R S) (span (s ×ˢ t)) = span s

Tactic:
Ideal.map_span

Goal state after:
case inl.e_I
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
s : Set R
t : Set S
hs : s.Nonempty
ht : t.Nonempty
⊢ span (⇑(RingHom.fst R S) '' s ×ˢ t) = span s
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: case inl.e_J
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
s : Set R
t : Set S
hs : s.Nonempty
ht : t.Nonempty
⊢ map (RingHom.snd R S) (span (s ×ˢ t)) = span t

Tactic:
Ideal.map_span

Goal state after:
case inl.e_J
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
s : Set R
t : Set S
hs : s.Nonempty
ht : t.Nonempty
⊢ span (⇑(RingHom.snd R S) '' s ×ˢ t) = span t
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: case refine_1.refine_2
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
s : Set S
N : Submodule R M
x : M
x_in : x ∈ ⇑(algebraMap S R) '' s • N
r : R
y : M
h : y ∈ ⇑(algebraMap S R) '' s • N
h' : y ∈ s • restrictScalars S N
c : R →₀ ↥N
c_supp : ↑c.support ⊆ ⇑(algebraMap S R) '' s
hc : r • y = ↑(c.sum fun r m ↦ r • m)
⊢ r • y ∈ s • restrictScalars S N

Tactic:
simp only [hc, Finsupp.sum, AddSubmonoidClass.coe_finsetSum, SetLike.val_smul]

Goal state after:
case refine_1.refine_2
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
s : Set S
N : Submodule R M
x : M
x_in : x ∈ ⇑(algebraMap S R) '' s • N
r : R
y : M
h : y ∈ ⇑(algebraMap S R) '' s • N
h' : y ∈ s • restrictScalars S N
c : R →₀ ↥N
c_supp : ↑c.support ⊆ ⇑(algebraMap S R) '' s
hc : r • y = ↑(c.sum fun r m ↦ r • m)
⊢ ∑ x ∈ c.support, x • ↑(c x) ∈ s • restrictScalars S N
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : FunLike F R S
f : F
G : Type u_2
inst✝¹ : FunLike G S R
inst✝ : RingHomClass G S R
g : G
I : Ideal R
hf : Set.LeftInvOn ⇑g ⇑f ↑I
x : R
hx : x ∈ ↑I
⊢ f x ∈ ↑(comap g I)

Tactic:
SetLike.mem_coe,

Goal state after:
R : Type u
S : Type v
F : Type u_1
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : FunLike F R S
f : F
G : Type u_2
inst✝¹ : FunLike G S R
inst✝ : RingHomClass G S R
g : G
I : Ideal R
hf : Set.LeftInvOn ⇑g ⇑f ↑I
x : R
hx : x ∈ ↑I
⊢ f x ∈ comap g I
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : (Ideal.span ↑I).IsTwoSided
s : Set M
x : M
⊢ x ∈ span R (↑I • s) ↔ x ∈ span R (↑(Ideal.span ↑I) • s)

Tactic:
I.span_eq

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : (Ideal.span ↑I).IsTwoSided
s : Set M
x : M
⊢ x ∈ span R (↑I • s) ↔ x ∈ span R (↑I • s)
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH : ∀ {s t s' t' : R}, P a b (b✝ % a✝, s, t) → P a b (a✝, s', t') → P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p :
  match (a✝, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (b✝, s', t') with
  | (r, s, t) => r = a * s + b * t
⊢ b✝ % a✝ = a * (s' - b✝ / a✝ * s) + b * (t' - b✝ / a✝ * t)

Tactic:
rw [mul_sub, mul_sub, add_sub, sub_add_eq_add_sub, ← p', sub_sub, mul_comm _ s, ← mul_assoc,
      mul_comm _ t, ← mul_assoc, ← add_mul, ← p, mod_eq_sub_mul_div]

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

Goal state before:
pp: case mp.refine_3.refine_1
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
ax : ι →₀ R
hax : ∀ (i : ι), ax i ∈ I
ay : ι →₀ R
hay : ∀ (i : ι), ay i ∈ I
a✝ : ι
⊢ 0 • f a✝ = 0

Tactic:
simp only [zero_smul, add_smul]

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

Goal state before:
pp: case mp.refine_3.refine_2
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
ax : ι →₀ R
hax : ∀ (i : ι), ax i ∈ I
ay : ι →₀ R
hay : ∀ (i : ι), ay i ∈ I
a✝ : ι
b₁✝ b₂✝ : R
⊢ (b₁✝ + b₂✝) • f a✝ = b₁✝ • f a✝ + b₂✝ • f a✝

Tactic:
simp only [zero_smul, add_smul]

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

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

Tactic:
· rw [h, Submodule.pow_zero, one_eq_top]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
I : Ideal R
n m : ℕ
hnI : I ^ n = 0
hmn : n ≤ m
x : R
hx : x ∈ I
⊢ x ^ m = 0

Tactic:
by
  simpa [hnI] using pow_le_pow_right hmn <| pow_mem_pow hx m

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

Goal state before:
pp: a b : ℤ
⊢ a.natAbs ∣ b.natAbs ∧ b.natAbs ∣ a.natAbs ↔ a.natAbs = b.natAbs

Tactic:
dvd_dvd_iff_associated

Goal state after:
a b : ℤ
⊢ Associated a.natAbs b.natAbs ↔ a.natAbs = b.natAbs
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommSemiring R
s✝ : Multiset (Ideal R)
a : Ideal R
s : Multiset (Ideal R)
ih : s.prod ≤ s.inf
⊢ a * s.prod ≤ a ⊓ s.inf

Tactic:
exact le_trans mul_le_inf (inf_le_inf le_rfl ih)

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

Goal state before:
pp: α : Type u_1
inst✝² : MonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : IsLeftCancelMulZero α
x y : α
⊢ Associated x y ↔ x ∣ y ∧ y ∣ x

Tactic:
dvd_dvd_iff_associated

Goal state after:
α : Type u_1
inst✝² : MonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : IsLeftCancelMulZero α
x y : α
⊢ Associated x y ↔ Associated x y
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
x y : R
⊢ (∃ a b, y ∣ b ∧ a * x + b = 1) → IsCoprime x y

Tactic:
rintro ⟨a, _, ⟨b, rfl⟩, e⟩; exact ⟨a, b, mul_comm b y ▸ e⟩

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

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : gcd k (m * n) = m' * n'
hm'n' : m' * n' ∣ k
⊢ n' ∣ gcd k n

Tactic:
have hn'k : n' ∣ k := (dvd_mul_left n' m').trans hm'n'
    exact dvd_gcd hn'k hn'

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
k : ℕ
hg : a = 0 ∧ b = 0
⊢ gcd a (b ^ k) ∣ gcd a b ^ k

Tactic:
rcases hg with ⟨rfl, rfl⟩

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
k : ℕ
⊢ gcd 0 (0 ^ k) ∣ gcd 0 0 ^ k
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
h✝ : Nontrivial α
ha : a = 0
⊢ Associated (0 ^ k) a

Tactic:
obtain rfl | hk := eq_or_ne k 0

Goal state after:
case h.inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
h✝ : Nontrivial α
ha : a = 0
h : a * b = c ^ 0
⊢ Associated (0 ^ 0) a

case h.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
h✝ : Nontrivial α
ha : a = 0
hk : k ≠ 0
⊢ Associated (0 ^ k) a
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
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ Classical.choose ⋯ = Classical.choose ⋯ * Classical.choose ⋯

Tactic:
Units.ext_iff,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
f : Associates α →* α
hinv : Function.RightInverse (⇑f) Associates.mk
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ ↑(Classical.choose ⋯) = ↑(Classical.choose ⋯ * Classical.choose ⋯)
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
normalize_gcd : ∀ (a b : α), normalize (gcd a b) = gcd a b
a : α
⊢ (if a = 0 then 0 else normalize (Classical.choose ⋯)) = 0

Tactic:
split_ifs with a0
      · rfl
      let := gcdMonoidOfGCD gcd gcd_dvd_left gcd_dvd_right dvd_gcd
      simpa [gcd_ne_zero_of_left a0] using show GCDMonoid.gcd .. * _ = _
        from (Classical.choose_spec ((gcd_dvd_left a 0).trans (.intro 0 rfl))).symm

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Semiring R
inst✝¹ : Module R M
S : Submodule R M
inst✝ : S.IsPrincipal
x : M
⊢ x ∈ S ↔ ∃ s, s • generator S = x

Tactic:
← mem_span_singleton,

Goal state after:
R : Type u
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Semiring R
inst✝¹ : Module R M
S : Submodule R M
inst✝ : S.IsPrincipal
x : M
⊢ x ∈ S ↔ x ∈ R ∙ generator S
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
a b : α
h : ¬a = 0
h_1 : b = 0
⊢ Associated (a * lcm a 0) (a * 0)

Tactic:
eq_zero_of_zero_dvd (dvd_lcm_right _ _)

Goal state after:
case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
a b : α
h : ¬a = 0
h_1 : b = 0
⊢ Associated (a * 0) (a * 0)
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
α : Type u_1
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : NormalizedGCDMonoid R
s : Finset α
f : α → R
⊢ ∃ g, s.gcd f = ∑ a ∈ s, f a * g a

Tactic:
by classical
  induction s using Finset.induction with
  | empty => simp
  | insert a s ha ih =>
    obtain ⟨x, y, hxy⟩ := IsBezout.gcd_eq_sum (f a) (s.gcd f)
    obtain ⟨u, hu⟩ := IsBezout.associated_gcd_gcd R (x := f a) (y := s.gcd f)
    rw [← hxy, add_mul, mul_comm x, mul_comm y] at hu
    obtain ⟨g, hg⟩ := ih
    refine ⟨Function.update (g · * (y * u)) a (x * u), ?_⟩
    rw [gcd_insert, sum_insert ha, ← hu, hg]
    simp only [Function.update_self, add_right_inj, sum_mul, mul_assoc]
    exact sum_congr rfl fun b hb ↦ congrArg (f b * ·) <|
      (Function.update_of_ne (show b ≠ a by grind) (x * u) (g · * (y * u))).symm

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

Goal state before:
pp: case neg
l : Type u_1
m : Type u_2
α : Type v
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq l
d : m → α
e : l → m
he : Function.Injective e
i j : l
h : ¬i = j
⊢ diagonal d (e i) (e j) = diagonal (d ∘ e) i j

Tactic:
rw [diagonal_apply_ne _ h, diagonal_apply_ne _ (he.ne h)]

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

Goal state before:
pp: R : Type u
S : Type u_1
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι✝ : Type w
ι' : Type w'
inst✝ : StrongRankCondition R
ι : Type u_2
b : Basis ι R R
⊢ Unique ι

Tactic:
have : Cardinal.mk ι = ↑(Module.finrank R R) := (Module.mk_finrank_eq_card_basis b).symm
  have : Subsingleton ι ∧ Nonempty ι := by simpa [Cardinal.eq_one_iff_unique]
  exact Nonempty.some ((unique_iff_subsingleton_and_nonempty _).2 this)

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

Goal state before:
pp: case neg
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert a t), ↑(f i)
has : a ∈ insert a t
hbt : b ∉ t
⊢ ∃ i ∈ insert a t, I ≤ f i

Tactic:
have hp' : ∀ j ∈ t, IsPrime (f j) := by
          intro j hj
          refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]
        rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_self (f a : Set R),
          subset_union_prime' hp', ← or_assoc, or_self_iff] at h
        rwa [Finset.exists_mem_insert]

Goal state after: