mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case h.refine_1
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
i : ι
f : ι →₀ N
hf : ∀ (i_1 : ι), f i_1 ∈ ⨆ (_ : i_1 ≠ i), p i_1
hx : (f.sum fun _i xi ↦ xi) ∈ p i
hsup : (f.sum fun _i xi ↦ xi) ∈ ⨆ j, ⨆ (_ : j ≠ i), p j
h : (f.sum fun _i xi ↦ xi) ≠ 0
j : ι
hj : j ∈ insert i f.support
⊢ (fun j ↦ if j = i then -f.sum fun x x_1 ↦ x_1 else f j) j ∈ p j

Tactic:
beta_reduce

Goal state after:
case h.refine_1
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
i : ι
f : ι →₀ N
hf : ∀ (i_1 : ι), f i_1 ∈ ⨆ (_ : i_1 ≠ i), p i_1
hx : (f.sum fun _i xi ↦ xi) ∈ p i
hsup : (f.sum fun _i xi ↦ xi) ∈ ⨆ j, ⨆ (_ : j ≠ i), p j
h : (f.sum fun _i xi ↦ xi) ≠ 0
j : ι
hj : j ∈ insert i f.support
⊢ (if j = i then -f.sum fun x x_1 ↦ x_1 else f j) ∈ p j
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_6
K : Type u_7
M : Type u_8
inst✝⁷ : CommRing R
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R K
inst✝³ : Module K M
inst✝² : Module R M
inst✝¹ : IsScalarTower R K M
inst✝ : FaithfulSMul R K
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
x : M
hx : x ∉ span K (range v)
c : R
y : M
hcy : y ∈ span R (range v)
heq : c • x + y = 0
hc : ¬c = 0
⊢ (algebraMap R K) c ≠ 0

Tactic:
ne_eq,

Goal state after:
R : Type u_6
K : Type u_7
M : Type u_8
inst✝⁷ : CommRing R
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R K
inst✝³ : Module K M
inst✝² : Module R M
inst✝¹ : IsScalarTower R K M
inst✝ : FaithfulSMul R K
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
x : M
hx : x ∉ span K (range v)
c : R
y : M
hcy : y ∈ span R (range v)
heq : c • x + y = 0
hc : ¬c = 0
⊢ ¬(algebraMap R K) c = 0
Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn

Goal state before:
pp: case zero
α : Type u_1
inst✝ : Monoid α
n : ℕ
a : α
s : Fin 0 → Set α
⊢ a ∈ 1 ↔ a = 1

Tactic:
Set.mem_one

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.ListOfFn

Goal state before:
pp: case succ
α : Type u_1
inst✝ : Monoid α
n✝ n : ℕ
ih : ∀ {a : α} {s : Fin n → Set α}, a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i ↦ ↑(f i)).prod = a
a : α
s : Fin (n + 1) → Set α
⊢ (∃ x, x ∈ s 0 ∧ ∃ a_1, x * (List.ofFn fun i ↦ ↑(a_1 i)).prod = a) ↔
    ∃ a_1 v, ↑a_1 * (List.ofFn fun i ↦ ↑(v i)).prod = a

Tactic:
SetCoe.exists,

Goal state after:
case succ
α : Type u_1
inst✝ : Monoid α
n✝ n : ℕ
ih : ∀ {a : α} {s : Fin n → Set α}, a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i ↦ ↑(f i)).prod = a
a : α
s : Fin (n + 1) → Set α
⊢ (∃ x, x ∈ s 0 ∧ ∃ a_1, x * (List.ofFn fun i ↦ ↑(a_1 i)).prod = a) ↔ ∃ x h v, x * (List.ofFn fun i ↦ ↑(v i)).prod = a
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t t' : Finset β
inst✝ : DecidableEq β
⊢ ↑(image₂ f s (t ∪ t')) = ↑(image₂ f s t ∪ image₂ f s t')

Tactic:
by
    push_cast
    exact image2_union_right

Goal state after:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
u : Finset γ
s : Set α
t : Set β
hu : ↑u ⊆ image2 f s t
⊢ ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ image₂ f s' t'

Tactic:
rw [← Set.image_prod, subset_set_image_iff] at hu

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
u : Finset γ
s : Set α
t : Set β
hu : ∃ s', ↑s' ⊆ s ×ˢ t ∧ image (fun x ↦ f x.1 x.2) s' = u
⊢ ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ image₂ f s' t'
Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
⊢ (f * g).coeff (a0 * b0) = f.coeff a0 * g.coeff b0

Tactic:
classical
  simp_rw [coeff_mul, sum, ← Finset.sum_product']
  refine (Finset.sum_eq_single (a0, b0) ?_ ?_).trans (if_pos rfl) <;> simp_rw [Finset.mem_product]
  · refine fun ab hab hne ↦ if_neg (fun he ↦ hne <| Prod.ext ?_ ?_)
    exacts [(h hab.1 hab.2 he).1, (h hab.1 hab.2 he).2]
  · refine fun hnotMem ↦ ite_eq_right_iff.mpr (fun _ ↦ ?_)
    rcases not_and_or.mp hnotMem with af | bg
    · rw [notMem_support_iff.mp af, zero_mul]
    · rw [notMem_support_iff.mp bg, mul_zero]

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
h : ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = a0 * b0
⊢ ∀ (x : G × G),
    x ∈ A ×ˢ B ∧ x.1 * x.2 = a0 * b0 → (∀ (y : G × G), y ∈ A ×ˢ B ∧ y.1 * y.2 = a0 * b0 → y = x) → UniqueMul A B a0 b0

Tactic:
rintro ⟨x1, x2⟩ _ J x y hx hy l

Goal state after:
G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
h : ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = a0 * b0
x1 x2 : G
a✝ : (x1, x2) ∈ A ×ˢ B ∧ (x1, x2).1 * (x1, x2).2 = a0 * b0
J : ∀ (y : G × G), y ∈ A ×ˢ B ∧ y.1 * y.2 = a0 * b0 → y = (x1, x2)
x y : G
hx : x ∈ A
hy : y ∈ B
l : x * y = a0 * b0
⊢ x = a0 ∧ y = b0
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : DivisionMonoid α
inst✝ : Fintype α
⊢ univ / univ = univ

Tactic:
by simp [div_eq_mul_inv]

Goal state after:
Module: Mathlib.Order.Sublattice

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
L : Sublattice β
a : α × β
⊢ a ∈ ⊤.prod L ↔ a ∈ comap LatticeHom.snd L

Tactic:
simp [mem_prod, LatticeHom.coe_snd]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case hs1
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hf1 : f.ker.FG
hf2 : g.ker.FG
hsur : Surjective ⇑f
⊢ (map f (comap f g.ker)).FG

pp: case hs2
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hf1 : f.ker.FG
hf2 : g.ker.FG
hsur : Surjective ⇑f
⊢ (comap f g.ker ⊓ f.ker).FG

Tactic:
· rwa [Submodule.map_comap_eq, LinearMap.range_eq_top.2 hsur, top_inf_eq]

Goal state after:
case hs2
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hf1 : f.ker.FG
hf2 : g.ker.FG
hsur : Surjective ⇑f
⊢ (comap f g.ker ⊓ f.ker).FG
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: M : Type u_2
N : Type u_4
P : Type u_6
f : M → N
g : N → P
inst✝ : One P
hg : 1 ∈ Set.range g
this✝ : One ↑(Set.range g) := { one := ⟨1, hg⟩ }
this : ↑1 = 1
⊢ MulExact f g ↔ MulExact Subtype.val (Set.rangeFactorization g)

Tactic:
simp [MulExact, Subtype.ext_iff, this]

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f k + g k ≤ f i + g j
⊢ ⨅ a, ⨅ a', f a + g a' = iInf f + iInf g

Tactic:
simp_rw [iInf_add, add_iInf]

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
κ : Sort u_4
g : κ → ℕ∞
h : ∀ (i : ι) (j : κ), a ≤ f i + g j
⊢ a ≤ iInf f + iInf g

Tactic:
simp_rw [iInf_add, add_iInf]

Goal state after:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
κ : Sort u_4
g : κ → ℕ∞
h : ∀ (i : ι) (j : κ), a ≤ f i + g j
⊢ a ≤ ⨅ i, ⨅ b, f i + g b
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
hT : IsUnit T
hf : IsIdempotentElem f
⊢ Commute f T ↔ map T f.range = f.range ∧ map T f.ker = f.ker

Tactic:
lift T to GeneralLinearGroup R E using hT

Goal state after:
E : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
f : E →ₗ[R] E
hf : IsIdempotentElem f
T : (E →ₗ[R] E)ˣ
⊢ Commute f ↑T ↔ map (↑T) f.range = f.range ∧ map (↑T) f.ker = f.ker
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
l : List α
l_ne_nil : l ≠ []
hl : List.IsChain (fun x1 x2 ↦ (x1, x2) ∈ r) l
⊢ (fromListIsChain l l_ne_nil hl).head = l.head l_ne_nil

Tactic:
simp [← apply_zero, List.getElem_zero_eq_head]

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_1
G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
a1 : G
ha1 : a1 ∈ A
b1 : G
he0 : (A * B).min' ⋯ = (A * B).max' ⋯
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
he : a0 = a1 ∧ b0 = b1
⊢ False

Tactic:
obtain ⟨⟨a2, b2⟩, h2, hne⟩ := exists_mem_ne hc (a0, b0)

Goal state after:
case refine_1
G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
a1 : G
ha1 : a1 ∈ A
b1 : G
he0 : (A * B).min' ⋯ = (A * B).max' ⋯
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
he : a0 = a1 ∧ b0 = b1
a2 b2 : G
h2 : (a2, b2) ∈ A ×ˢ B
hne : (a2, b2) ≠ (a0, b0)
⊢ False
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
newLast : α
rel : (p.last, newLast) ∈ r
x : α
⊢ x ∈ p.snoc newLast rel ↔ x ∈ p ∨ x = newLast

Tactic:
simp only [snoc, append, mem_def, Set.mem_range]
  constructor
  · rintro ⟨i, rfl⟩
    exact Fin.lastCases (Or.inr <| Fin.append_right _ _ 0) (fun i => Or.inl ⟨⟨i.1, i.2⟩,
      (Fin.append_left _ _ _).symm⟩) i
  · intro h
    rcases h with (⟨i, rfl⟩ | rfl)
    · exact ⟨i.castSucc, Fin.append_left _ _ _⟩
    · exact ⟨Fin.last _, Fin.append_right _ _ 0⟩

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
p : LTSeries α
h : ↑p.length = height (RelSeries.last p)
i : Fin (p.length + 1)
⊢ ∀ (p_1 : LTSeries α), RelSeries.last p_1 = p.toFun i → ↑p_1.length ≤ ↑↑i

Tactic:
intro p'

Goal state after:
α : Type u_1
inst✝ : Preorder α
p : LTSeries α
h : ↑p.length = height (RelSeries.last p)
i : Fin (p.length + 1)
p' : LTSeries α
⊢ RelSeries.last p' = p.toFun i → ↑p'.length ≤ ↑↑i
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
inst✝ : Nonempty α
⊢ r.FiniteDimensional ∨ ¬r.FiniteDimensional

Tactic:
exact em r.FiniteDimensional

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case succ.refine_2.refine_2
α : Type u_3
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
n : ℕ
IH :
  ∀ (s : Fin (n + 1) → α) (h : ∀ (i : Fin n), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}),
    ∃ t i,
      t.toFun ∘ ⇑i = { length := n, toFun := s, step := h }.toFun ∧
        i 0 = 0 ∧ i (Fin.last { length := n, toFun := s, step := h }.length) = Fin.last t.length
s : Fin (n + 1 + 1) → α
h : ∀ (i : Fin (n + 1)), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}
t₁ : RelSeries {(a, b) | a ⋖ b}
i : Fin ({ length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length + 1) ↪ Fin (t₁.length + 1)
ht : t₁.toFun ∘ ⇑i = { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length) = Fin.last t₁.length
t₂ : ℕ → α
h₁ : t₂ 0 = s (Fin.last n).castSucc
m : ℕ
h₂ : t₂ m = s (Fin.last n).succ
ht₂ : ∀ i < m, t₂ i ⋖ t₂ (i + 1)
t₃ : RelSeries {(a, b) | a ⋖ b} := { length := m, toFun := fun x ↦ t₂ ↑x, step := ⋯ }
H : t₁.last = t₂ 0
j : Fin { length := n + 1, toFun := s, step := h }.length
⊢ ((t₁.smash t₃ H).toFun ∘ ⇑{ toFun := Fin.snoc (Fin.castLE ⋯ ∘ ⇑i) (Fin.last (t₁.smash t₃ H).length), inj' := ⋯ })
      j.castSucc =
    { length := n + 1, toFun := s, step := h }.toFun j.castSucc

Tactic:
convert! congr_fun ht j using 1

Goal state after:
case e'_2
α : Type u_3
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
n : ℕ
IH :
  ∀ (s : Fin (n + 1) → α) (h : ∀ (i : Fin n), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}),
    ∃ t i,
      t.toFun ∘ ⇑i = { length := n, toFun := s, step := h }.toFun ∧
        i 0 = 0 ∧ i (Fin.last { length := n, toFun := s, step := h }.length) = Fin.last t.length
s : Fin (n + 1 + 1) → α
h : ∀ (i : Fin (n + 1)), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}
t₁ : RelSeries {(a, b) | a ⋖ b}
i : Fin ({ length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length + 1) ↪ Fin (t₁.length + 1)
ht : t₁.toFun ∘ ⇑i = { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last { length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length) = Fin.last t₁.length
t₂ : ℕ → α
h₁ : t₂ 0 = s (Fin.last n).castSucc
m : ℕ
h₂ : t₂ m = s (Fin.last n).succ
ht₂ : ∀ i < m, t₂ i ⋖ t₂ (i + 1)
t₃ : RelSeries {(a, b) | a ⋖ b} := { length := m, toFun := fun x ↦ t₂ ↑x, step := ⋯ }
H : t₁.last = t₂ 0
j : Fin { length := n + 1, toFun := s, step := h }.length
⊢ ((t₁.smash t₃ H).toFun ∘ ⇑{ toFun := Fin.snoc (Fin.castLE ⋯ ∘ ⇑i) (Fin.last (t₁.smash t₃ H).length), inj' := ⋯ })
      j.castSucc =
    (t₁.toFun ∘ ⇑i) j
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ krullDim α ≠ ⊥ ↔ Nonempty α

Tactic:
ne_eq,

Goal state after:
α : Type u_1
inst✝ : Preorder α
⊢ ¬krullDim α = ⊥ ↔ Nonempty α
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ krullDim α ≠ ⊥ ↔ Nonempty α

Tactic:
by
  rw [ne_eq, krullDim_eq_bot_iff, not_isEmpty_iff]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ FiniteDimensionalOrder α ↔ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤

Tactic:
by
  by_cases h : Nonempty α
  · simp [← not_infiniteDimensionalOrder_iff, ← krullDim_eq_top_iff]
  · constructor
    · exact (fun h1 ↦ False.elim (h (LTSeries.nonempty_of_finiteDimensionalOrder α)))
    · exact (fun h1 ↦ False.elim (h1.1 (krullDim_eq_bot_iff.mpr (not_nonempty_iff.mp h))))

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: n : ℕ
⊢ height n = ↑n

Tactic:
induction n using Nat.strongRecOn with | ind n ih =>
  apply le_antisymm
  · apply height_le_coe_iff.mpr
    simp +contextual only [ih, Nat.cast_lt, implies_true]
  · exact length_le_height_last (p := LTSeries.range n)

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
⊢ height x + 1 ≤ height ↑x

Tactic:
rw [height_add_const]
    apply iSup₂_le
    intro p hlast
    let p' := (p.map _ WithBot.coe_strictMono).cons ⊥ (by simp)
    apply le_iSup₂_of_le p' (by simp [p', hlast]) (by simp [p'])

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: case empty
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
a : α
⊢ a ∈ 1 ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ ∅ → g i ∈ f i), 1 = a

Tactic:
Set.mem_one

Goal state after:
case empty
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
a : α
⊢ a = 1 ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ ∅ → g i ∈ f i), 1 = a
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: case insert
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
a : α
⊢ a ∈ f i * ∏ x ∈ is, f x ↔ ∃ g, ∃ (_ : ∀ {i_1 : ι}, i_1 ∈ insert i is → g i_1 ∈ f i_1), ∏ i ∈ insert i is, g i = a

Tactic:
Set.mem_mul

Goal state after:
case insert
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
i : ι
is : Finset ι
hi : i ∉ is
ih : ∀ (a : α), a ∈ ∏ i ∈ is, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ is → g i ∈ f i), ∏ i ∈ is, g i = a
a : α
⊢ (∃ x ∈ f i, ∃ y ∈ ∏ x ∈ is, f x, x * y = a) ↔
    ∃ g, ∃ (_ : ∀ {i_1 : ι}, i_1 ∈ insert i is → g i_1 ∈ f i_1), ∏ i ∈ insert i is, g i = a
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: case nil
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
g : ι → α
hg : ∀ i ∈ [], g i ∈ f i
⊢ 1 ∈ 1

Tactic:
Set.mem_one

Goal state after:
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 : Set R
x y : Submodule R M
⊢ ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ s → n ∈ x + y → r • n ∈ s • x + s • y

Tactic:
rintro r m hr hm
      rw [add_eq_sup, Submodule.mem_sup] at hm
      obtain ⟨a, ha, b, hb, rfl⟩ := hm
      rw [smul_add, add_eq_sup, Submodule.mem_sup]
      exact ⟨r • a, mem_set_smul_of_mem_mem (mem1 := hr) (mem2 := ha),
        r • b, mem_set_smul_of_mem_mem (mem1 := hr) (mem2 := hb), rfl⟩

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.BigOperators

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
l : Finset ι
S : ι → Set α
x✝ : α
⊢ x✝ ∈ (fun f ↦ ∏ i ∈ l, f i) '' (↑l).pi S ↔ x✝ ∈ ∏ i ∈ l, S i

Tactic:
mem_finsetProd,

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
l : Finset ι
S : ι → Set α
x✝ : α
⊢ x✝ ∈ (fun f ↦ ∏ i ∈ l, f i) '' (↑l).pi S ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ l → g i ∈ S i), ∏ i ∈ l, g i = x✝
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : a∗ = a
⊢ a∗ * a∗ = a∗

Tactic:
kstar_mul_kstar

Goal state after:
α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : a∗ = a
⊢ a∗ = a∗
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
⊢ span R (x • {1}) = R ∙ x

Tactic:
smul_set_singleton,

Goal state after:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
⊢ R ∙ x • 1 = R ∙ x
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
M N : Submodule R A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
⊢ map f.toLinearMap (map₂ (LinearMap.mul R A) M N) = ⨆ i, map f.toLinearMap (map ((LinearMap.mul R A) ↑i) N)

Tactic:
apply map_iSup

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

Goal state before:
pp: case succ
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mul_mem : ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → ∀ (m : A) (hm : m ∈ M), C i.succ (x * m) ⋯
n : ℕ
n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx
x : A
⊢ ∀ (hx : x ∈ M ^ (n + 1)), C (n + 1) x hx

Tactic:
simp_rw [pow_succ]

Goal state after:
case succ
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
algebraMap : ∀ (r : R), C 0 ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯
mul_mem : ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → ∀ (m : A) (hm : m ∈ M), C i.succ (x * m) ⋯
n : ℕ
n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx
x : A
⊢ ∀ (hx : x ∈ M ^ n * M), C (n + 1) x ⋯
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: case mpr.inl
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : Ideal R
h : p.IsPrime
⊢ (p.prod ⊤).IsPrime

pp: case mpr.inr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : Ideal S
h : p.IsPrime
⊢ (⊤.prod p).IsPrime

Tactic:
· exact isPrime_ideal_prod_top

Goal state after:
case mpr.inr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : Ideal S
h : p.IsPrime
⊢ (⊤.prod p).IsPrime
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: R : Type u
inst✝ : EuclideanDomain R
a : R
a0 : a ≠ 0
⊢ a / a = 1

Tactic:
simpa only [one_mul] using mul_div_cancel_right₀ 1 a0

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
hK : K.IsRadical
⊢ (Ideal.comap f K).radical.IsRadical

Tactic:
apply radical_isRadical

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑f
x : R
h : ∀ (m : M), x • m = 0
m : M
⊢ x • f m = 0

Tactic:
rw [← map_smul, h, f.map_zero]

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
⊢ lcm x y ∣ z

Tactic:
by
  rw [lcm]
  by_cases hxy : gcd x y = 0
  · rw [hxy, div_zero]
    rw [EuclideanDomain.gcd_eq_zero_iff] at hxy
    rwa [hxy.1] at hxz
  rcases gcd_dvd x y with ⟨⟨r, hr⟩, ⟨s, hs⟩⟩
  suffices x * y ∣ z * gcd x y by
    obtain ⟨p, hp⟩ := this
    use p
    generalize gcd x y = g at hxy hs hp ⊢
    subst hs
    rw [mul_left_comm, mul_div_cancel_left₀ _ hxy, ← mul_left_inj' hxy, hp]
    rw [← mul_assoc]
    simp only [mul_right_comm]
  rw [gcd_eq_gcd_ab, mul_add]
  apply dvd_add
  · rw [mul_left_comm]
    gcongr
    apply hyz.mul_right
  · rw [mul_left_comm, mul_comm]
    gcongr
    apply hxz.mul_right

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
I : Ideal R
⊢ I ≤ N.annihilator ↔ I • N = ⊥

Tactic:
simp_rw [← le_bot_iff, smul_le, SetLike.le_def, mem_annihilator]; rfl

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

Goal state before:
pp: case neg
z : ℤ
hz : normalize z = z
h : z < 0
⊢ 0 ≤ z

Tactic:
rw [normalize_of_nonpos h.le] at hz
    lia

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

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f g : β → α
hs : ∃ x ∈ s, f x ≠ 0
hg : ∀ b ∈ s, f b = s.gcd f * g b
⊢ Associated (s.gcd f * 1) (s.gcd fun x ↦ s.gcd f * g x)

pp: case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f g : β → α
hs : ∃ x ∈ s, f x ≠ 0
hg : ∀ b ∈ s, f b = s.gcd f * g b
⊢ s.gcd f ≠ 0

Tactic:
· simp [← gcd_congr rfl hg]

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f g : β → α
hs : ∃ x ∈ s, f x ≠ 0
hg : ∀ b ∈ s, f b = s.gcd f * g b
⊢ s.gcd f ≠ 0
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
h : gcd 0 0 = 0
⊢ ∃ x' y', 0 = gcd 0 0 * x' ∧ 0 = gcd 0 0 * y' ∧ IsUnit (gcd x' y')

Tactic:
simp_rw [← associated_one_iff_isUnit]

Goal state after:
case pos
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
h : gcd 0 0 = 0
⊢ ∃ x' y', 0 = gcd 0 0 * x' ∧ 0 = gcd 0 0 * y' ∧ Associated (gcd x' y') 1
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
hn : n ≠ 0
h : I ^ n ≤ P ↔ ∃ I_1, (n ≠ 0 ∧ I_1 = I) ∧ I_1 ≤ P
⊢ I ^ n ≤ P ↔ I ≤ P

Tactic:
ne_eq,

Goal state after:
R : Type u
inst✝ : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
hn : n ≠ 0
h : I ^ n ≤ P ↔ ∃ I_1, (¬n = 0 ∧ I_1 = I) ∧ I_1 ≤ P
⊢ I ^ n ≤ P ↔ I ≤ P
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a : α
⊢ lcm a 0 = 0

Tactic:
apply lcm_zero_right

Goal state after: