mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case coe
m : ℕ
n : ℕ∞
⊢ ↑n + 1 ≤ ↑m ↔ ↑n < ↑m

Tactic:
norm_cast
    simp [add_one_le_iff']

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma

Goal state before:
pp: κ : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset γ
t : Finset α
u : Finset κ
f : γ → α → κ → β
⊢ ∏ x ∈ s, ∏ y ∈ t, ∏ z ∈ u, f x y z = ∏ z ∈ u, ∏ x ∈ s, ∏ y ∈ t, f x y z

Tactic:
prod_comm (s := t),

Goal state after:
κ : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset γ
t : Finset α
u : Finset κ
f : γ → α → κ → β
⊢ ∏ x ∈ s, ∏ y ∈ u, ∏ x_1 ∈ t, f x x_1 y = ∏ z ∈ u, ∏ x ∈ s, ∏ y ∈ t, f x y z
Module: Mathlib.Data.Vector.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p✝ : α → Prop
i : Fin n
l : List α
p : l.length = n
⊢ (l.eraseIdx ↑i).length = n - 1

Tactic:
l.length_eraseIdx_of_lt

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p✝ : α → Prop
i : Fin n
l : List α
p : l.length = n
⊢ l.length - 1 = n - 1

α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p✝ : α → Prop
i : Fin n
l : List α
p : l.length = n
⊢ ↑i < l.length
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
inst✝ : IsRightCancelMul M
f g : ι → M
i : ι
hi : i ∈ s
hfg : ∀ j ∈ s, j ≠ i → f j = g j
⊢ ∏ j ∈ s, f j = ∏ j ∈ s, g j ↔ f i = g i

Tactic:
classical
  rw [prod_eq_mul_prod_sdiff_singleton_of_mem hi, prod_eq_mul_prod_sdiff_singleton_of_mem hi,
    prod_congr rfl (by simpa), mul_left_inj]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
f : ι → M
⊢ (∏ j, if j = i then f j else 1) = f i

Tactic:
Finset.prod_ite_eq',

Goal state after:
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
f : ι → M
⊢ (if i ∈ univ then f i else 1) = f i
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case h
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h✝ : a ∈ s
m : Multiset α
h : ↑s = a ::ₘ m
this : m.card = n
⊢ s = a ::ₛ ⟨m, this⟩

Tactic:
apply Subtype.ext

Goal state after:
case h
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h✝ : a ∈ s
m : Multiset α
h : ↑s = a ::ₘ m
this : m.card = n
⊢ ↑s = ↑(a ::ₛ ⟨m, this⟩)
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
x : Vector α n
i : Fin (n - 1)
⊢ x.tail.get i = x.get ⟨↑i + 1, ⋯⟩

Tactic:
obtain ⟨i, ih⟩ := i; dsimp
  rcases x with ⟨_ | _, h⟩ <;> try rfl
  rw [List.length] at h
  rw [← h] at ih
  contradiction

Goal state after:
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b✝ : α
inst✝ : Subsingleton α
n✝ : ℕ
s s' : Sym α (n✝ + 1)
b : α
⊢ s = s'

Tactic:
rw [eq_replicate_of_subsingleton b s', eq_replicate_of_subsingleton b s]

Goal state after:
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n.succ
h : none ∉ s
⊢ map (fun x ↦ ↑x) s.attach = s

Tactic:
convert! s.attach_map_coe

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ↪r s
hf : ∀ (a : α) (b : β), s b (f a) → b ∈ Set.range ⇑f
g : r ↪r s
hg : ∀ (a : α) (b : β), s b (g a) → b ∈ Set.range ⇑g
h :
  (fun f ↦ f.toFun) { toRelEmbedding := f, mem_range_of_rel' := hf } =
    (fun f ↦ f.toFun) { toRelEmbedding := g, mem_range_of_rel' := hg }
⊢ { toRelEmbedding := f, mem_range_of_rel' := hf } = { toRelEmbedding := g, mem_range_of_rel' := hg }

Tactic:
congr with x

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ↪r s
hf : ∀ (a : α) (b : β), s b (f a) → b ∈ Set.range ⇑f
g : r ↪r s
hg : ∀ (a : α) (b : β), s b (g a) → b ∈ Set.range ⇑g
h :
  (fun f ↦ f.toFun) { toRelEmbedding := f, mem_range_of_rel' := hf } =
    (fun f ↦ f.toFun) { toRelEmbedding := g, mem_range_of_rel' := hg }
x : α
⊢ f x = g x
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝⁸ : LE α
inst✝⁷ : LE β
inst✝⁶ : LE γ
inst✝⁵ : LE α₁
inst✝⁴ : LE α₂
inst✝³ : LE β₁
inst✝² : LE β₂
inst✝¹ : LE γ₁
inst✝ : LE γ₂
a : α
b : β
c : γ
ea : α₁ ≃o α₂
eb : β₁ ≃o β₂
⊢ ∀ {a b : α₁ ⊕ₗ β₁},
    (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) a ≤ (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) b ↔ a ≤ b

Tactic:
simp_rw [Lex.forall]; rintro (a | a) (b | b) <;> simp

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case h.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
H : IsWellOrder α r
a : α
b : β
h : s b ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a)
m : α
hm : m ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) b}
hm' : ∀ x ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) b}, ¬r x m
lt : s b ↑(collapseF f m)
⊢ (ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) m = b

pp: case h.inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
H : IsWellOrder α r
a m : α
h : s (↑(collapseF f m)) ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a)
hm : m ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) ↑(collapseF f m)}
hm' : ∀ x ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) ↑(collapseF f m)}, ¬r x m
⊢ (ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) m = ↑(collapseF f m)

pp: case h.inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
H : IsWellOrder α r
a : α
b : β
h : s b ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a)
m : α
hm : m ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) b}
hm' : ∀ x ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) b}, ¬r x m
gt : s (↑(collapseF f m)) b
⊢ (ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) m = b

Tactic:
· refine (collapseF_not_lt f m (fun c h ↦ ?_) lt).elim
      by_contra hn
      exact hm' _ hn h

Goal state after:
case h.inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
H : IsWellOrder α r
a m : α
h : s (↑(collapseF f m)) ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a)
hm : m ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) ↑(collapseF f m)}
hm' : ∀ x ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) ↑(collapseF f m)}, ¬r x m
⊢ (ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) m = ↑(collapseF f m)

case h.inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
H : IsWellOrder α r
a : α
b : β
h : s b ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a)
m : α
hm : m ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) b}
hm' : ∀ x ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) b}, ¬r x m
gt : s (↑(collapseF f m)) b
⊢ (ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) m = b
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
⊢ Monotone fun x ↦ (f x) (g x)

pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
⊢ (f (ωSup c)) (g (ωSup c)) = ωSup (c.map { toFun := fun x ↦ (f x) (g x), monotone' := ?m.25 })

Tactic:
· intro x y hxy
    exact OrderHom.apply_mono (hf.monotone hxy) (hg.monotone hxy)

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
⊢ (f (ωSup c)) (g (ωSup c)) = ωSup (c.map { toFun := fun x ↦ (f x) (g x), monotone' := ⋯ })
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
⊢ Nonempty (Quotient.out (f i) ↪ Quotient.out (g i))

Tactic:
have := H i; rwa [← mk_out (f i), ← mk_out (g i)] at this

Goal state after:
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: c : Cardinal.{u}
d : Cardinal.{v}
h : ∀ (n : ℕ), ↑n ≤ c ↔ ↑n ≤ d
⊢ toNat c = toNat d

Tactic:
by
  have h' := forall_congr' h
  rw [← Cardinal.aleph0_le, ← Cardinal.aleph0_le] at h'
  rcases iff_iff_and_or_not_and_not.mp h' with ⟨hc, hd⟩ | ⟨hc, hd⟩
  · simp [Cardinal.toNat_apply_of_aleph0_le, hc, hd]
  · apply eq_of_forall_le_iff
    rw [← cast_toNat_of_lt_aleph0 (not_le.mp hc), ← cast_toNat_of_lt_aleph0 (not_le.mp hd)] at h
    simpa using h

Goal state after:
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: c : Cardinal.{u}
c' : ℕ
⊢ toENat c ≤ toENat ↑c' ↔ c ≤ ↑c'

Tactic:
simp_rw [toENat_nat, ← toENat_le_natCast]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: c : Cardinal.{u}
⊢ toENat c < ⊤ ↔ c < ℵ₀

Tactic:
by simp [lt_top_iff_ne_top]

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

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
M✝ : Type u_3
M₂ : Type u_4
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
r s : R✝
x✝ : M✝
R : Type u_5
S : Type u_6
M : Type u_7
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : SMul S M
f : R →+* S
hf : Surjective ⇑f
hsmul : ∀ (c : R) (x : M), f c • x = c • x
x : M
⊢ 0 • x = 0

Tactic:
zero_smul

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
M✝ : Type u_3
M₂ : Type u_4
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
r s : R✝
x✝ : M✝
R : Type u_5
S : Type u_6
M : Type u_7
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : SMul S M
f : R →+* S
hf : Surjective ⇑f
hsmul : ∀ (c : R) (x : M), f c • x = c • x
x : M
⊢ 0 = 0
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
⊢ IsSMulRegular R g

Tactic:
by
  intro x y h
  convert congr_arg (g⁻¹ • ·) h <;> simp [← smul_assoc]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Cardinal.{v}
⊢ lift.{u, v} (⨆ i, f i) ≤ sum f

Tactic:
rw [lift_iSup bddAbove_of_small]

Goal state after:
ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Cardinal.{v}
⊢ ⨆ i, lift.{u, v} (f i) ≤ sum f
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c < 1 ↔ c = 0

Tactic:
by
  simpa using lt_succ_bot_iff (a := c)

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: n : ℕ
⊢ ↑n + 1 ≤ ℵ₀

Tactic:
← Nat.cast_add_one,

Goal state after:
n : ℕ
⊢ ↑(n + 1) ≤ ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
n : ℕ
t : Set α
H : #↑t ≤ ↑n
s : Finset α
hs : ↑s ⊆ t
⊢ s.card ≤ n

Tactic:
simpa using (mk_le_mk_of_subset hs).trans H

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r✝ s : R
x✝ : M
x y : R
r : M
⊢ ((↑(DistribMulAction.toAddMonoidEnd R M)).toFun (x + y)) r =
    ((↑(DistribMulAction.toAddMonoidEnd R M)).toFun x + (↑(DistribMulAction.toAddMonoidEnd R M)).toFun y) r

Tactic:
simp [(AddMonoidHom.add_apply), add_smul]

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

Goal state before:
pp: I : Type u
f : I → Type v
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst✝ : (i : I) → Module (f i) (g i)
x✝¹ : (i : I) → g i
x✝ : I
⊢ (0 • x✝¹) x✝ = 0 x✝

Tactic:
zero_smul

Goal state after:
I : Type u
f : I → Type v
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst✝ : (i : I) → Module (f i) (g i)
x✝¹ : (i : I) → g i
x✝ : I
⊢ 0 x✝ = 0 x✝
Module: Mathlib.Algebra.Module.Submodule.Defs

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
module_M : Module R M
p : Submodule R M
r : R
x : M
inst✝ : Invertible r
⊢ r • x ∈ p ↔ x ∈ p

Tactic:
by
  refine ⟨fun h ↦ ?_, p.smul_mem r⟩
  rw [← invOf_smul_smul r x]
  exact p.smul_mem _ h

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S T : Submodule R M
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T

Tactic:
have : S ≤ S ⊔ T := le_sup_left

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S T : Submodule R M
this : S ≤ S ⊔ T
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
p : Submodule R M :=
  let __AddSubmonoid := sSup (toAddSubmonoid '' s);
  { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ }
⊢ sSup (toAddSubmonoid '' s) ≤ (sSup s).toAddSubmonoid

Tactic:
exact sSup_le fun _ ⟨q, hq, hq'⟩ ↦ hq'.symm ▸ le_sSup hq

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
S T : Subsemigroup M
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T

Tactic:
have : S ≤ S ⊔ T := le_sup_left

Goal state after:
M : Type u_2
inst✝ : Mul M
S T : Subsemigroup M
this : S ≤ S ⊔ T
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
p : (x y : R) → x ∈ closure s → y ∈ closure s → Prop
mem_mem : ∀ (x : R) (hx : x ∈ s) (y : R) (hy : y ∈ s), p x y ⋯ ⋯
zero_left : ∀ (x : R) (hx : x ∈ closure s), p 0 x ⋯ hx
zero_right : ∀ (x : R) (hx : x ∈ closure s), p x 0 hx ⋯
add_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : R) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : R
hx : x ∈ closure s
hy : y ∈ closure s
⊢ p x y hx hy

Tactic:
induction hy using closure_induction with
  | mem z hz => induction hx using closure_induction with
    | mem _ h => exact mem_mem _ h _ hz
    | zero => exact zero_left _ _
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
  | zero => exact zero_right x hx
  | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ _ h₁ h₂
  | add _ _ _ _ h₁ h₂ => exact add_right _ _ _ _ _ _ h₁ h₂

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
r : M₀
⊢ r ∈ M₀⁰ ↔ ∀ (x : M₀), x * r = 0 → x = 0

Tactic:
rw [← nonZeroDivisorsRight_eq_nonZeroDivisors]; rfl

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
⊢ Associates.mk a ∈ (Associates M₀)⁰ ↔ a ∈ M₀⁰

Tactic:
mem_nonZeroDivisors_iff_right,

Goal state after:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
⊢ (∀ (x : Associates M₀), x * Associates.mk a = 0 → x = 0) ↔ a ∈ M₀⁰
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ (∀ (a_1 a_2 : M),
      Associates.mk a ∣ Associates.mk (a_1 * a_2) →
        ∃ x x_1,
          Associates.mk x ∣ Associates.mk a_1 ∧
            Associates.mk x_1 ∣ Associates.mk a_2 ∧ Associates.mk a = Associates.mk (x * x_1)) ↔
    ∀ ⦃b c : M⦄, a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

Tactic:
mk_dvd_mk

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ (∀ (a_1 a_2 : M), a ∣ a_1 * a_2 → ∃ x x_1, x ∣ a_1 ∧ x_1 ∣ a_2 ∧ Associates.mk a = Associates.mk (x * x_1)) ↔
    ∀ ⦃b c : M⦄, a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case right
M : Type u_1
inst✝ : CommMonoidWithZero M
a : Associates M
x : Associates M
ndvd : IsUnit x
⊢ a * x ∣ a

Tactic:
rcases ndvd with ⟨u, rfl⟩

Goal state after:
case right
M : Type u_1
inst✝ : CommMonoidWithZero M
a : Associates M
u : (Associates M)ˣ
⊢ a * ↑u ∣ a
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
m : M
⊢ m ∈ sSup s ↔ ∀ (N : Submodule R M), (∀ p ∈ s, p ≤ N) → m ∈ N

Tactic:
simp_rw [sSup_eq_iSup, Submodule.mem_iSup, iSup_le_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_1.refine_1
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x✝ : M
hx✝ : x✝ ∈ span R S
x : M
hx : x ∈ S
⊢ ↑{x} ⊆ S

pp: case refine_1.refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x✝ : M
hx✝ : x✝ ∈ span R S
x : M
hx : x ∈ S
⊢ x ∈ span R ↑{x}

Tactic:
· rwa [Finset.coe_singleton, Set.singleton_subset_iff]

Goal state after:
case refine_1.refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set M
x✝ : M
hx✝ : x✝ ∈ span R S
x : M
hx : x ∈ S
⊢ x ∈ span R ↑{x}
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderTop α
inst✝¹ : IsCoatomic α
inst✝ : OrderTop β
l : α → β
u : β → α
gi : GaloisInsertion l u
h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a
b : β
⊢ IsCoatom (u b) ↔ IsCoatom b

Tactic:
refine ⟨fun hb => gi.isCoatom_of_image hb, fun hb => ?_⟩
  obtain ⟨a, ha, hab⟩ :=
    (eq_top_or_exists_le_coatom (u b)).resolve_left fun h =>
      hb.1 <| (gi.gc.u_top ▸ gi.l_u_eq ⊤ : l ⊤ = ⊤) ▸ gi.l_u_eq b ▸ congr_arg l h
  have : l a = b :=
    (hb.le_iff.mp (gi.l_u_eq b ▸ gi.gc.monotone_l hab : b ≤ l a)).resolve_left fun hla =>
      ha.1 (gi.gc.u_top ▸ h_coatom a ha ▸ congr_arg u hla)
  exact this ▸ (h_coatom a ha).symm ▸ ha

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι✝ : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst✝² : (i : ι) → PartialOrder (π i)
inst✝¹ : (i : ι) → OrderBot (π i)
inst✝ : ∀ (i : ι), IsAtomic (π i)
b : (i : ι) → π i
h : ¬b = ⊥
i : ι
hi : ¬b i = ⊥
a : π i
ha : IsAtom a
hab : a ≤ b i
⊢ ∃ a, IsAtom a ∧ a ≤ b

Tactic:
exact ⟨Function.update ⊥ i a, isAtom_single ha, update_le_iff.2 ⟨hab, by simp⟩⟩

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case h.right
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := ⋯
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = c.sup id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = d.sup id
⊢ x ⊔ y = (c ∪ d).sup id

Tactic:
· simp only [hc.right, hd.right, Finset.sup_union]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case insert
α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
t : Set ι
hjt : j ∉ t
hst : Disjoint (↑s₀) (insert j t)
ih : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i)
this : Disjoint (f j) ((⨆ i ∈ t, f i) ⊔ ⨆ i ∈ ↑s₀, f i)
⊢ Disjoint (⨆ i ∈ insert j s₀, f i) (⨆ i ∈ t, f i)

Tactic:
rw [s₀.iSup_insert j f, disjoint_comm, sup_comm]

Goal state after:
case insert
α : Type u_1
ι : Type u_3
inst✝¹ : CompleteLattice α
inst✝ : IsModularLattice α
f : ι → α
hf : iSupIndep f
j : ι
s₀ : Finset ι
hj : j ∉ s₀
t : Set ι
hjt : j ∉ t
hst : Disjoint (↑s₀) (insert j t)
ih : Disjoint (⨆ i ∈ s₀, f i) (f j ⊔ ⨆ i ∈ t, f i)
this : Disjoint (f j) ((⨆ i ∈ t, f i) ⊔ ⨆ i ∈ ↑s₀, f i)
⊢ Disjoint (⨆ i ∈ t, f i) ((⨆ x ∈ s₀, f x) ⊔ f j)
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
f : ι → α
s : Set ι
h₁ : iSupIndep f
h₂ : ⨆ i ∈ s, f i = ⊤
i : ι
hi : f i ≠ ⊥
⊢ i ∈ s

Tactic:
by_contra contra

Goal state after:
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
f : ι → α
s : Set ι
h₁ : iSupIndep f
h₂ : ⨆ i ∈ s, f i = ⊤
i : ι
hi : f i ≠ ⊥
contra : i ∉ s
⊢ False
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case refine_2
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ x ∈ S, ¬t.sup id < x
⊢ t.sup id ≤ sSup s

Tactic:
Finset.sup_id_eq_sSup

Goal state after:
case refine_2
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : WellFoundedGT α
s : Set α
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ t.sup id = x}
t : Finset α
ht₁ : ↑t ⊆ s
hm : ∀ x ∈ S, ¬t.sup id < x
⊢ sSup ↑t ≤ sSup s
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f g : α → M
h : EqOn f g s
x : α
⊢ s.mulIndicator f x = s.mulIndicator g x

Tactic:
by
    simp only [mulIndicator]
    split_ifs with h_1
    · exact h h_1
    rfl

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
t : Set A
k : S
hks : k ∈ span R s
x : A
hx : x ∈ t
⊢ 0 • x ∈ span R (s • t)

Tactic:
zero_smul

Goal state after:
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
t : Set A
k : S
hks : k ∈ span R s
x : A
hx : x ∈ t
⊢ 0 ∈ span R (s • t)
Module: Mathlib.Algebra.Algebra.Tower

Goal state before:
pp: case refine_1
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝ : A
hp : x✝ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
⊢ 0 • y ∈ span R (s • t)

Tactic:
zero_smul

Goal state after:
case refine_1
R : Type u
S : Type v
A : Type w
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
s : Set S
hs : span R s = ⊤
t : Set A
x✝ : A
hp : x✝ ∈ restrictScalars R (span S t)
s0 : S
y : A
hy : y ∈ t
⊢ 0 ∈ span R (s • t)
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ sSup s ⊓ a = ⨆ b ∈ s, b ⊓ a

Tactic:
inf_comm _ a,

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
⊢ a ⊓ sSup s = ⨆ b ∈ s, a ⊓ b
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set α
h : ∀ (t : Finset α), ↑t ⊆ s → sSupIndep ↑t
a : α
ha : a ∈ s
t : Finset α
⊢ ↑t ⊆ s \ {a} → a ⊓ t.sup id = ⊥

Tactic:
Finset.sup_id_eq_sSup

Goal state after:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set α
h : ∀ (t : Finset α), ↑t ⊆ s → sSupIndep ↑t
a : α
ha : a ∈ s
t : Finset α
⊢ ↑t ⊆ s \ {a} → a ⊓ sSup ↑t = ⊥