mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: case cons
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f₁ f₂ : ι → Set α
h : ι
tl : List ι
ih : (∀ i ∈ tl, f₁ i ⊆ f₂ i) → (List.map f₁ tl).prod ⊆ (List.map f₂ tl).prod
hf : ∀ i ∈ h :: tl, f₁ i ⊆ f₂ i
⊢ (f₁ h :: List.map f₁ tl).prod ⊆ (f₂ h :: List.map f₂ tl).prod

Tactic:
List.prod_cons

Goal state after:
case cons
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f₁ f₂ : ι → Set α
h : ι
tl : List ι
ih : (∀ i ∈ tl, f₁ i ⊆ f₂ i) → (List.map f₁ tl).prod ⊆ (List.map f₂ tl).prod
hf : ∀ i ∈ h :: tl, f₁ i ⊆ f₂ i
⊢ f₁ h * (List.map f₁ tl).prod ⊆ f₂ h * (List.map f₂ tl).prod
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: case h
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
g : ι → α
a✝ : List ι
hg : ∀ i ∈ ⟦a✝⟧, g i ∈ f i
⊢ (↑(List.map g a✝)).prod ∈ (↑(List.map f a✝)).prod

Tactic:
Multiset.prod_coe

Goal state after:
case h
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
g : ι → α
a✝ : List ι
hg : ∀ i ∈ ⟦a✝⟧, g i ∈ f i
⊢ (List.map g a✝).prod ∈ (List.map f a✝).prod
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: case h
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f₁ f₂ : ι → Set α
a✝ : List ι
hf : ∀ i ∈ ⟦a✝⟧, f₁ i ⊆ f₂ i
⊢ (↑(List.map f₁ a✝)).prod ⊆ (↑(List.map f₂ a✝)).prod

Tactic:
Multiset.prod_coe

Goal state after:
case h
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f₁ f₂ : ι → Set α
a✝ : List ι
hf : ∀ i ∈ ⟦a✝⟧, f₁ i ⊆ f₂ i
⊢ (List.map f₁ a✝).prod ⊆ (List.map f₂ a✝).prod
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x y : R
h : y ∣ x
⊢ IsCoprime (-x + 1) y

Tactic:
exact add_one_left_of_dvd h.neg_right

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
h : y ∣ x
⊢ IsRelPrime (-x + 1) y

Tactic:
exact add_one_left_of_dvd h.neg_right

Goal state after:
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case insert.refine_1
R : Type u
I : Type v
inst✝ : CommSemiring R
z : R
s : I → R
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r).Pairwise (IsCoprime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r)).Pairwise (IsCoprime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
⊢ IsCoprime (s a) (∏ x ∈ r, s x)

Tactic:
refine IsCoprime.prod_right fun i hir ↦ ?_

Goal state after:
case insert.refine_1
R : Type u
I : Type v
inst✝ : CommSemiring R
z : R
s : I → R
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r).Pairwise (IsCoprime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r)).Pairwise (IsCoprime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
i : I
hir : i ∈ r
⊢ IsCoprime (s a) (s i)
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case e'_2.e'_6
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 * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
hμ :
  ∑ x ∈ t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x +
        μ x * ∏ j ∈ insert a t \ {x}, s j) =
    1
x : I
hx : x ∈ t
⊢ s a * ∏ x ∈ (insert a t \ {x}) \ {a}, s x = (fun x ↦ s a) x * ∏ j ∈ t \ {x}, s j

Tactic:
sdiff_sdiff_comm,

Goal state after:
case e'_2.e'_6
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 * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
hμ :
  ∑ x ∈ t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x +
        μ x * ∏ j ∈ insert a t \ {x}, s j) =
    1
x : I
hx : x ∈ t
⊢ s a * ∏ x ∈ (insert a t \ {a}) \ {x}, s x = (fun x ↦ s a) x * ∏ j ∈ t \ {x}, s j
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case cons.mp.refine_2.refine_1.e_a.e_a.e_s
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
x : I
hx : x ∈ t
⊢ t \ {x} = (insert a t \ {x}) \ {a}

Tactic:
sdiff_sdiff_comm,

Goal state after:
case cons.mp.refine_2.refine_1.e_a.e_a.e_s
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
x : I
hx : x ∈ t
⊢ t \ {x} = (insert a t \ {a}) \ {x}
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case h.e_a.e_a.e_a.e_s
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}
hs : Pairwise (IsCoprime on fun a ↦ s ↑a)
Hb : ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1
u v : R
huv : u * ∏ i ∈ t, s i + v * s a = 1
hμ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
x : I
hx : x ∈ t
⊢ (insert a t \ {x}) \ {a} = t \ {x}

Tactic:
sdiff_sdiff_comm,

Goal state after:
case h.e_a.e_a.e_a.e_s
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}
hs : Pairwise (IsCoprime on fun a ↦ s ↑a)
Hb : ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1
u v : R
huv : u * ∏ i ∈ t, s i + v * s a = 1
hμ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
x : I
hx : x ∈ t
⊢ (insert a t \ {a}) \ {x} = t \ {x}
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I J : Submodule R A
y : A
x✝ : y ∈ J
⊢ 0 * y ∈ I

Tactic:
rw [zero_mul]

Goal state after:
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I J : Submodule R A
y : A
x✝ : y ∈ J
⊢ 0 ∈ I
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module S P
ι : Type u_6
inst✝¹ : Finite ι
M✝ : PEmpty.{u_6 + 1} → Submodule R N
inst✝ : ∀ (i : PEmpty.{u_6 + 1}), IsNoetherian R ↥(M✝ i)
⊢ IsNoetherian R ↥(⨆ i, M✝ i)

Tactic:
iSup_of_empty

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module S P
ι : Type u_6
inst✝¹ : Finite ι
M✝ : PEmpty.{u_6 + 1} → Submodule R N
inst✝ : ∀ (i : PEmpty.{u_6 + 1}), IsNoetherian R ↥(M✝ i)
⊢ IsNoetherian R ↥⊥
Module: Mathlib.Algebra.EuclideanDomain.Field

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
b : K
⊢ (if 0 = 0 then b else 0) = b

Tactic:
if_pos rfl

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
b : K
⊢ b = b
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case inl
R : Type u
inst✝ : EuclideanDomain R
b c : R
h : 0 * b ∣ c
⊢ b ∣ c / 0

pp: case inr
R : Type u
inst✝ : EuclideanDomain R
a b c : R
h : a * b ∣ c
ha : a ≠ 0
⊢ b ∣ c / a

Tactic:
· simp only [div_zero, dvd_zero]

Goal state after:
case inr
R : Type u
inst✝ : EuclideanDomain R
a b c : R
h : a * b ∣ c
ha : a ≠ 0
⊢ b ∣ c / a
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
⊢ comap (↑f) (comap (↑f.symm) I) = I

Tactic:
by
  rw [← RingEquiv.toRingHom_eq_coe, ← RingEquiv.toRingHom_eq_coe, comap_comap,
    RingEquiv.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp, comap_id]

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
K : Ideal S
H : K.IsMaximal
J : Ideal R
hJ : comap f K < J
h : K = map f J
⊢ comap f ⊥ ≤ J

Tactic:
exact le_trans (comap_mono bot_le) (le_of_lt hJ)

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
n : ℕ
⊢ comap f K ^ n ≤ comap f (K ^ n)

Tactic:
by
  induction n with
  | zero =>
    rw [pow_zero, pow_zero, Ideal.one_eq_top, Ideal.one_eq_top]
    exact rfl.le
  | succ n n_ih =>
    rw [pow_succ, pow_succ]
    exact (Ideal.mul_mono_left n_ih).trans (Ideal.le_comap_mul f)

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* R
g : T →+* S
⊢ Ideal.comap g (ker f) = ker (f.comp g)

Tactic:
by
  rw [RingHom.ker_eq_comap_bot, Ideal.comap_comap, RingHom.ker_eq_comap_bot]

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

Goal state before:
pp: case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : gcd x y = 0
⊢ 0 ∣ z

Tactic:
EuclideanDomain.gcd_eq_zero_iff

Goal state after:
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : x = 0 ∧ y = 0
⊢ 0 ∣ z
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
hgxy : gcd x y = 0
⊢ y = 0

Tactic:
EuclideanDomain.gcd_eq_zero_iff

Goal state after:
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
hgxy : x = 0 ∧ y = 0
⊢ y = 0
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : gcd x y = 0
⊢ 0 = x * y

Tactic:
EuclideanDomain.gcd_eq_zero_iff

Goal state after:
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : x = 0 ∧ y = 0
⊢ 0 = x * y
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s₁ s₂ : Multiset α
⊢ (s₁ + s₂).gcd = fold GCDMonoid.gcd (GCDMonoid.gcd 0 0) (s₁ + s₂)

Tactic:
by simp [gcd]

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
r : R
I : Ideal R
f : R →+* S
⊢ map f (r • I) = f r • map f I

Tactic:
rw [← Submodule.ideal_span_singleton_smul, smul_eq_mul, Ideal.map_mul, Ideal.map_span,
    Set.image_singleton, ← smul_eq_mul, Submodule.ideal_span_singleton_smul]

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

Goal state before:
pp: case succ.inl
R : Type u
inst✝¹ : Semiring R
I J : Ideal R
inst✝ : J.IsTwoSided
h : I ⊔ J = ⊤
ih : I ⊔ J ^ 0 = ⊤
⊢ I ⊔ J ^ (0 + 1) = ⊤

pp: case succ.inr
R : Type u
inst✝¹ : Semiring R
I J : Ideal R
inst✝ : J.IsTwoSided
h : I ⊔ J = ⊤
n : ℕ
ih : I ⊔ J ^ n = ⊤
hn : n ≠ 0
⊢ I ⊔ J ^ (n + 1) = ⊤

Tactic:
· simpa [J.pow_one] using h

Goal state after:
case succ.inr
R : Type u
inst✝¹ : Semiring R
I J : Ideal R
inst✝ : J.IsTwoSided
h : I ⊔ J = ⊤
n : ℕ
ih : I ⊔ J ^ n = ⊤
hn : n ≠ 0
⊢ I ⊔ J ^ (n + 1) = ⊤
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∀ x ∈ s, f x = 0
⊢ ∃ g, (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1

Tactic:
refine ⟨fun _ ↦ 1, fun b hb ↦ by rw [h b hb, gcd_eq_zero_iff.2 h, mul_one], ?_⟩
      rw [gcd_eq_gcd_image, image_const hs, gcd_singleton, id, normalize_one]

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

Goal state before:
pp: case right
α : Type u_2
a : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
this : Ideal.span {a} ≠ ⊤
I : Ideal α
Imax : I.IsMaximal
H : Ideal.span {a} ≤ I
⊢ a ∈ Ideal.span {a}

Tactic:
apply Ideal.subset_span

Goal state after:
case right
α : Type u_2
a : α
inst✝ : CommSemiring α
h : a ∈ nonunits α
this : Ideal.span {a} ≠ ⊤
I : Ideal α
Imax : I.IsMaximal
H : Ideal.span {a} ≤ I
⊢ a ∈ {a}
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case ha
ι : Type u_1
α : Type u_2
inst✝³ : CommMonoidWithZero α
inst✝² : NormalizedGCDMonoid α
inst✝¹ : Div α
inst✝ : MulDivCancelClass α
f : ι → α
s : Finset ι
i : ι
his : i ∈ s
hfi : f i ≠ 0
g : ι → α
he : ∀ b ∈ s, f b = s.gcd f * g b
hg : s.gcd g = 1
a : ι
ha : a ∈ s
⊢ s.gcd f ≠ 0

Tactic:
exact mt Finset.gcd_eq_zero_iff.1 fun h ↦ hfi <| h i his

Goal state after:
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
⊢ gcd (d₁ ^ k) b ∣ gcd d₁ b ^ k

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
⊢ gcd d₁ b ^ k ∣ 1

Tactic:
· exact gcd_pow_left_dvd_pow_gcd

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
⊢ gcd d₁ b ^ k ∣ 1
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h✝ : ¬(a = 0 ∨ b = 0)
h1 : ¬a = 0
h2 : ¬b = 0
h : gcd a b ≠ 0
⊢ a * b ∣ gcd a b * c ↔ a ∣ c ∧ b ∣ c

Tactic:
←
      (gcd_mul_right' c a b).dvd_iff_dvd_right,

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h✝ : ¬(a = 0 ∨ b = 0)
h1 : ¬a = 0
h2 : ¬b = 0
h : gcd a b ≠ 0
⊢ a * b ∣ gcd (a * c) (b * c) ↔ a ∣ c ∧ b ∣ c
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
a_norm : NormalizationMonoid α
a_gcd : GCDMonoid α
normalize_gcd✝¹ : ∀ (a b : α), normalize (gcd a b) = gcd a b
normalize_lcm✝¹ : ∀ (a b : α), normalize (lcm a b) = lcm a b
b_norm : NormalizationMonoid α
b_gcd : GCDMonoid α
normalize_gcd✝ : ∀ (a b : α), normalize (gcd a b) = gcd a b
normalize_lcm✝ : ∀ (a b : α), normalize (lcm a b) = lcm a b
⊢ { toNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd✝¹,
      normalize_lcm := normalize_lcm✝¹ } =
    { toNormalizationMonoid := b_norm, toGCDMonoid := b_gcd, normalize_gcd := normalize_gcd✝,
      normalize_lcm := normalize_lcm✝ }

Tactic:
cases Subsingleton.elim a_gcd b_gcd

Goal state after:
case refl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
a_norm : NormalizationMonoid α
a_gcd : GCDMonoid α
normalize_gcd✝¹ : ∀ (a b : α), normalize (gcd a b) = gcd a b
normalize_lcm✝¹ : ∀ (a b : α), normalize (lcm a b) = lcm a b
b_norm : NormalizationMonoid α
normalize_gcd✝ : ∀ (a b : α), normalize (gcd a b) = gcd a b
normalize_lcm✝ : ∀ (a b : α), normalize (lcm a b) = lcm a b
⊢ { toNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd✝¹,
      normalize_lcm := normalize_lcm✝¹ } =
    { toNormalizationMonoid := b_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd✝,
      normalize_lcm := normalize_lcm✝ }
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
a_norm : StrongNormalizationMonoid α
a_gcd : GCDMonoid α
normalize_gcd✝¹ : ∀ (a b : α), normalize (gcd a b) = gcd a b
normalize_lcm✝¹ : ∀ (a b : α), normalize (lcm a b) = lcm a b
b_norm : StrongNormalizationMonoid α
b_gcd : GCDMonoid α
normalize_gcd✝ : ∀ (a b : α), normalize (gcd a b) = gcd a b
normalize_lcm✝ : ∀ (a b : α), normalize (lcm a b) = lcm a b
⊢ { toStrongNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd✝¹,
      normalize_lcm := normalize_lcm✝¹ } =
    { toStrongNormalizationMonoid := b_norm, toGCDMonoid := b_gcd, normalize_gcd := normalize_gcd✝,
      normalize_lcm := normalize_lcm✝ }

Tactic:
cases Subsingleton.elim a_gcd b_gcd

Goal state after:
case refl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
a_norm : StrongNormalizationMonoid α
a_gcd : GCDMonoid α
normalize_gcd✝¹ : ∀ (a b : α), normalize (gcd a b) = gcd a b
normalize_lcm✝¹ : ∀ (a b : α), normalize (lcm a b) = lcm a b
b_norm : StrongNormalizationMonoid α
normalize_gcd✝ : ∀ (a b : α), normalize (gcd a b) = gcd a b
normalize_lcm✝ : ∀ (a b : α), normalize (lcm a b) = lcm a b
⊢ { toStrongNormalizationMonoid := a_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd✝¹,
      normalize_lcm := normalize_lcm✝¹ } =
    { toStrongNormalizationMonoid := b_norm, toGCDMonoid := a_gcd, normalize_gcd := normalize_gcd✝,
      normalize_lcm := normalize_lcm✝ }
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
x y : R
inst✝ : IsPrincipal (Ideal.span {x, y})
⊢ gcd x y ∈ Ideal.span {gcd x y}

Tactic:
apply Ideal.subset_span

Goal state after:
R : Type u
inst✝¹ : CommRing R
x y : R
inst✝ : IsPrincipal (Ideal.span {x, y})
⊢ gcd x y ∈ {gcd x y}
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✝² : StrongRankCondition R
ι : Type u_2
inst✝¹ : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ⊆ ↑(span R w)
⊢ Injective ⇑(linearCombination R fun i ↦ Span.repr R w ⟨v i, ⋯⟩)

Tactic:
intro f g h

Goal state after:
case i
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
ι : Type u_2
inst✝¹ : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ⊆ ↑(span R w)
f g : ι →₀ R
h : (linearCombination R fun i ↦ Span.repr R w ⟨v i, ⋯⟩) f = (linearCombination R fun i ↦ Span.repr R w ⟨v i, ⋯⟩) g
⊢ f = g
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✝ : StrongRankCondition R
ι : Type v
v : ι → M
i : LinearIndependent R v
w : Set M
s : span R w = ⊤
⊢ Injective ⇑(linearCombination R fun i ↦ Span.repr R w ⟨v i, ⋯⟩)

Tactic:
intro f g h

Goal state after:
case i
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : ι → M
i : LinearIndependent R v
w : Set M
s : span R w = ⊤
f g : ι →₀ R
h : (linearCombination R fun i ↦ Span.repr R w ⟨v i, ⋯⟩) f = (linearCombination R fun i ↦ Span.repr R w ⟨v i, ⋯⟩) g
⊢ f = g
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case a
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ #ι ≤ ⨆ ι, #↑↑ι

pp: case a
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ ⨆ ι, #↑↑ι ≤ #ι

Tactic:
· trans
    swap
    · apply le_ciSup Cardinal.bddAbove_of_small
      exact
        ⟨Set.range v, by
          rw [LinearIndepOn]
          convert! v.reindexRange.linearIndependent
          simp⟩
    · exact (Cardinal.mk_range_eq v v.injective).ge

Goal state after:
case a
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ ⨆ ι, #↑↑ι ≤ #ι
Module: Mathlib.RingTheory.Ideal.Operations

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

Tactic:
have hp' : ∀ i ∈ u, IsPrime (f i) := by
          intro i hiu
          refine hp i (Finset.mem_insert_of_mem (Finset.mem_insert_of_mem hiu)) ?_ ?_ <;>
              rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]

Goal state after:
case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
u : Finset ι
hbu : b ∉ u
hat : a ∉ insert b u
hp : ∀ i ∈ insert a (insert b u), i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert a (insert b u)), ↑(f i)
has : a ∈ insert a (insert b u)
hbt : b ∈ insert b u
hp' : ∀ i ∈ u, (f i).IsPrime
⊢ ∃ i ∈ insert a (insert b u), I ≤ f i
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ (a.sum fun a b ↦ ↑(if h : b ∈ I then ⟨b, h⟩ else 0) • v a) = a.sum fun i c ↦ c • v i

Tactic:
apply Finsupp.sum_congr

Goal state after:
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ ∀ x ∈ a.support, ↑(if h : a x ∈ I then ⟨a x, h⟩ else 0) • v x = a x • v x
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M✝ : Type u_2
inst✝⁵ : AddCommMonoid M✝
inst✝⁴ : Module R M✝
A : Type ?u.13
B : Type ?u.15
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal R
M : Submodule R A
⊢ ∀ m ∈ { toFun := map (Algebra.linearMap R A), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } I,
    ∀ n ∈ M, Commute m n

Tactic:
rintro _ ⟨r, _, rfl⟩ a _; apply Algebra.commutes

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

Goal state before:
pp: 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
⊢ M ∈ Set.range ⇑(scalar n)

Tactic:
cases isEmpty_or_nonempty n

Goal state after:
case inl
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✝ : IsEmpty n
⊢ M ∈ Set.range ⇑(scalar n)

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
⊢ M ∈ Set.range ⇑(scalar n)
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : ¬x = a
hx' : x ∉ s
⊢ 0 = s.card * if False then 1 else 0

Tactic:
ite_false,

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
H : s.toFinset = {a}
x : α
hx : ¬x = a
hx' : x ∉ s
⊢ 0 = s.card * 0