mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Sigma

Goal state before:
pp: case neg
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst ∉ s₁
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁

Tactic:
by_cases h₂ : x.2 ∈ t₁ x.1

Goal state after:
case pos
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst ∉ s₁
h₂ : x.snd ∈ t₁ x.fst
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁

case neg
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst ∉ s₁
h₂ : x.snd ∉ t₁ x.fst
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
π : β → Type u_1
s : Finset β
e : α ≃ β
⊢ s.restrict ∘ ⇑(Equiv.piCongrLeft π e) =
    ⇑(Equiv.piCongrLeft (fun b ↦ π ↑b) (e.restrictPreimageFinset s)) ∘ (s.preimage ⇑e ⋯).restrict

Tactic:
ext x b
  simp only [comp_apply, restrict, Equiv.piCongrLeft_apply_eq_cast,
    Equiv.restrictPreimageFinset_symm_apply_coe]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
hIcc : h₀_finset_Icc = h₁_finset_Icc
hIco : h₀_finset_Ico = h₁_finset_Ico
a b x : α
⊢ a < x ∧ x ≤ b ↔ x ∈ h₁_finset_Ioc a b

Tactic:
h₁_finset_mem_Ioc

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
hIcc : h₀_finset_Icc = h₁_finset_Icc
hIco : h₀_finset_Ico = h₁_finset_Ico
a b x : α
⊢ a < x ∧ x ≤ b ↔ a < x ∧ x ≤ b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
hI : a₂ ≤ b₂
ha : a₂ ≤ a₁
hb : b₁ < b₂
⊢ Set.Icc a₁ b₁ ⊂ Set.Icc a₂ b₂

Tactic:
exact Set.Icc_ssubset_Icc_right hI ha hb

Goal state after:
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: case H
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
a b : α
h : a < b
ih : ∀ t ⊂ Icc a b, ∀ (b : α), a < b → Icc a b = t → False
⊢ False

Tactic:
obtain ⟨c, hac, hcb⟩ := exists_between h

Goal state after:
case H
α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
a b : α
h : a < b
ih : ∀ t ⊂ Icc a b, ∀ (b : α), a < b → Icc a b = t → False
c : α
hac : a < c
hcb : c < b
⊢ False
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case inr.refine_1.inr.inl
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
hc : ∀ (m n : ℕ), m < n → ¬f m ≤ f n
m : ℕ
a✝ : (f ∘ ⇑g) m ≠ (f ∘ ⇑g) m
hf : (f ∘ ⇑g) m ≤ (f ∘ ⇑g) m
⊢ False

pp: case inr.refine_1.inr.inr
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
hc : ∀ (m n : ℕ), m < n → ¬f m ≤ f n
m n : ℕ
a✝ : (f ∘ ⇑g) m ≠ (f ∘ ⇑g) n
hf : (f ∘ ⇑g) m ≤ (f ∘ ⇑g) n
h : n < m
⊢ False

Tactic:
· contradiction

Goal state after:
case inr.refine_1.inr.inr
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
hc : ∀ (m n : ℕ), m < n → ¬f m ≤ f n
m n : ℕ
a✝ : (f ∘ ⇑g) m ≠ (f ∘ ⇑g) n
hf : (f ∘ ⇑g) m ≤ (f ∘ ⇑g) n
h : n < m
⊢ False
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
⊢ centralizer s ≤ normalizer s

Tactic:
refine fun g hg h ↦ ⟨fun hh ↦ ?_, fun hh ↦ ?_⟩

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : g ∈ centralizer s
h : G
hh : h ∈ s
⊢ g * h * g⁻¹ ∈ s

case refine_2
G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : g ∈ centralizer s
h : G
hh : g * h * g⁻¹ ∈ s
⊢ h ∈ s
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
assoc : Std.Associative op
s : Multiset α
comm : {x | x ∈ s}.Pairwise fun x y ↦ op x y = op y x
x : α
hx : x ∈ {x | x ∈ s}
y : α
hy : y ∈ {x | x ∈ s}
h : x ≠ y
b : α
⊢ op x (op y b) = op y (op x b)

Tactic:
← assoc.assoc,

Goal state after:
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
assoc : Std.Associative op
s : Multiset α
comm : {x | x ∈ s}.Pairwise fun x y ↦ op x y = op y x
x : α
hx : x ∈ {x | x ∈ s}
y : α
hy : y ∈ {x | x ∈ s}
h : x ≠ y
b : α
⊢ op (op x y) b = op y (op x b)
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case mp
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : C ≤ A
x✝ : G
⊢ (∃ x, (x ∈ ↑A ∧ x ∈ ↑B) ∧ ∃ y ∈ ↑C, x * y = x✝) → x✝ ∈ ↑A ∧ ∃ x ∈ ↑B, ∃ y ∈ ↑C, x * y = x✝

pp: case mpr
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : C ≤ A
x✝ : G
⊢ (x✝ ∈ ↑A ∧ ∃ x ∈ ↑B, ∃ y ∈ ↑C, x * y = x✝) → ∃ x, (x ∈ ↑A ∧ x ∈ ↑B) ∧ ∃ y ∈ ↑C, x * y = x✝

Tactic:
· rintro ⟨y, ⟨hyA, hyB⟩, z, hz, rfl⟩
    refine ⟨A.mul_mem hyA (h hz), ?_⟩
    exact ⟨y, hyB, z, hz, rfl⟩

Goal state after:
case mpr
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : C ≤ A
x✝ : G
⊢ (x✝ ∈ ↑A ∧ ∃ x ∈ ↑B, ∃ y ∈ ↑C, x * y = x✝) → ∃ x, (x ∈ ↑A ∧ x ∈ ↑B) ∧ ∃ y ∈ ↑C, x * y = x✝
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
M : Type u_3
f : ι → M
inst✝¹ : CommMonoid M
inst✝ : IsEmpty ι
s : Finset ι
⊢ ∏ i ∈ s, f i = 1

Tactic:
eq_empty_of_isEmpty s,

Goal state after:
ι : Type u_1
M : Type u_3
f : ι → M
inst✝¹ : CommMonoid M
inst✝ : IsEmpty ι
s : Finset ι
⊢ ∏ i ∈ ∅, f i = 1
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
d : { d // c ≤ d }
⊢ ker c.mkMulHom ≤ ↑d

Tactic:
rw [Con.ker_mkMulHom_eq]

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
d : { d // c ≤ d }
⊢ c ≤ ↑d
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
f : ℕ → M
n : ℕ
⊢ ∏ k ∈ range (n + 1 + 1), f k = (∏ k ∈ range (n + 1), f (k + 1)) * f 0

Tactic:
by rw [prod_range_succ _ n, mul_right_comm, ← prod_range_succ' _ n, prod_range_succ]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
ι : Type u_3
s : Finset ι
P : ι → Submonoid M
hP : ∀ i ∈ s, (P i).FG
⊢ (⨆ i ∈ s, P i).FG

Tactic:
simpa only [Finset.sup_eq_iSup] using finset_sup s P hP

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
M : Type u_4
inst✝¹ : Group G
inst✝ : Monoid M
N : Subgroup G
nN : N.Normal
φ : G →* M
HN : N ≤ φ.ker
⊢ Injective ⇑(lift N φ HN) ↔ N = φ.ker

Tactic:
by
  rw [← MonoidHom.ker_eq_bot_iff, QuotientGroup.ker_lift, Subgroup.map_eq_bot_iff]
  grind [QuotientGroup.ker_mk']

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: G : Type u_3
inst✝ : Group G
ι : Type u_5
s : Finset ι
P : ι → Subgroup G
hP : ∀ i ∈ s, (P i).FG
⊢ (⨆ i ∈ s, P i).FG

Tactic:
simpa only [Finset.sup_eq_iSup] using finset_sup s P hP

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x : M
⊢ g (f.sec (f x)).1 = g (↑(f.sec (f x)).2 * x)

Tactic:
exact f.eq_of_eq hg (by rw [sec_spec', map_mul])

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
x : M
y : ↥S
⊢ (k.toMonoidHom.comp g) x = (k.toMonoidHom.comp g) ↑y * k.mk' (g x) ⟨g ↑y, ⋯⟩

Tactic:
change k (g x) = k (g y) * _

Goal state after:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
x : M
y : ↥S
⊢ k (g x) = k (g ↑y) * k.mk' (g x) ⟨g ↑y, ⋯⟩
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), l ↑w ∈ U
z : N
⊢ k ((k.sec ((f.map hy k) z)).1 * g ↑(f.sec z).2) = k (↑(k.sec ((f.map hy k) z)).2 * g (f.sec z).1)

Tactic:
map_mul k,

Goal state after:
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), l ↑w ∈ U
z : N
⊢ k (k.sec ((f.map hy k) z)).1 * k (g ↑(f.sec z).2) = k (↑(k.sec ((f.map hy k) z)).2 * g (f.sec z).1)
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), l ↑w ∈ U
z : N
⊢ k (k.sec ((f.map hy k) z)).1 * k (g ↑(f.sec z).2) = k (↑(k.sec ((f.map hy k) z)).2 * g (f.sec z).1)

Tactic:
map_mul k,

Goal state after:
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), l ↑w ∈ U
z : N
⊢ k (k.sec ((f.map hy k) z)).1 * k (g ↑(f.sec z).2) = k ↑(k.sec ((f.map hy k) z)).2 * k (g (f.sec z).1)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
x : OreLocalization S X
⊢ 1 • x = x

Tactic:
cases x with | _ r s

Goal state after:
case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r : X
s : ↥S
⊢ 1 • (r /ₒ s) = r /ₒ s
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x : OreLocalization S R
⊢ x * 1 = x

Tactic:
cases x with | _ r s

Goal state after:
case c
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s : ↥S
⊢ r /ₒ s * 1 = r /ₒ s
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
a₁ b₁ : M
a₂ b₂ : ↥S
⊢ f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ (Localization.r S) (a₁, a₂) (b₁, b₂)

Tactic:
by
  rw [f.eq, Localization.r_iff_exists]

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
y : ↥S
⊢ mk (↑y) 1 * mk 1 y = 1

Tactic:
rw [mk_mul, mul_one, one_mul, mk_self]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
⊢ a * b = if a = 0 ∨ b = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) a b

Tactic:
cases a <;> cases b <;> aesop

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : a = 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b

pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b

Tactic:
· rw [ha, zero_mul, ← coe_zero, untopD_coe, zero_mul]

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b

Tactic:
by_cases ha : a = 0; · rw [ha, zero_mul, ← coe_zero, untopD_coe, zero_mul]
  by_cases hb : b = 0; · rw [hb, mul_zero, ← coe_zero, untopD_coe, mul_zero]
  cases a; · rw [top_mul hb, untopD_top, zero_mul]
  cases b; · rw [mul_top ha, untopD_top, mul_zero]
  rw [← coe_mul, untopD_coe, untopD_coe, untopD_coe]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : MulZeroClass α
inst✝ : LT α
a b : WithTop α
ha : a < ⊤
hb : b < ⊤
⊢ a * b < ⊤

Tactic:
rw [WithTop.lt_top_iff_ne_top] at *

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : MulZeroClass α
inst✝ : LT α
a b : WithTop α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ a * b ≠ ⊤
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
a : α
⊢ 1 * ↑a = ↑a

Tactic:
← coe_one,

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
a : α
⊢ ↑1 * ↑a = ↑a
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
a : α
⊢ ↑a * 1 = ↑a

Tactic:
← coe_one,

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
a : α
⊢ ↑a * ↑1 = ↑a
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
x : OreLocalization S R
⊢ φ x = (universalMulHom f fS hf) x

Tactic:
cases x with | _ r s

Goal state after:
case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
r : R
s : ↥S
⊢ φ (r /ₒ s) = (universalMulHom f fS hf) (r /ₒ s)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
⊢ a * b = if a = 0 ∨ b = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) a b

Tactic:
cases a <;> cases b <;> aesop

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α✝ : Type u_1
inst✝³ : Preorder α✝
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n m : ℕ
h : n ≤ m
⊢ succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r

Tactic:
left

Goal state after:
α✝ : Type u_1
inst✝³ : Preorder α✝
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n m : ℕ
h : n ≤ m
⊢ succ^[n] r ≤ succ^[m] r
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a✝ : αᵒᵈ
h : a✝ ≤ (⇑toDual ∘ SuccOrder.succ ∘ ⇑ofDual) a✝
⊢ IsMin a✝

Tactic:
apply SuccOrder.max_of_succ_le h

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case inr
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
nh : ¬v₂ ≤ v₁
h : v₂ ≤ v₁
⊢ v₁ < v₂

Tactic:
· contradiction

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Nonempty α
inst✝³ : Preorder β
f : α → β
inst✝² : NoMaxOrder α
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
hm' : ∀ (a : α), f a ≤ m
⊢ False

Tactic:
obtain ⟨a₀⟩ := ‹Nonempty α›

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Nonempty α
inst✝³ : Preorder β
f : α → β
inst✝² : NoMaxOrder α
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
hm' : ∀ (a : α), f a ≤ m
a₀ : α
⊢ False
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
x : WithTop α
⊢ IsSuccPrelimit x ↔ x = ⊤ ∨ ∃ y, x = ↑y ∧ IsSuccPrelimit y

Tactic:
by
  cases x with
  | coe x => simp [IsSuccPrelimit, WithTop.forall]
  | top => simp [IsSuccPrelimit]

Goal state after:
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : Nonempty α
inst✝ : NoMaxOrder α
x : WithTop α
⊢ IsSuccLimit x ↔ x = ⊤ ∨ ∃ y, x = ↑y ∧ IsSuccLimit y

Tactic:
by
  cases x with
  | coe x => simp [Order.isSuccLimit_iff, WithTop.isSuccPrelimit_iff, WithTop.exists]
  | top => simp [Order.isSuccLimit_iff, WithTop.exists]

Goal state after:
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: case neg
α : Type u_1
a b : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
h : ¬IsMax a
⊢ succ a < b

Tactic:
rw [lt_iff_le_and_ne, succ_le_iff_of_not_isMax h]

Goal state after:
case neg
α : Type u_1
a b : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
h : ¬IsMax a
⊢ a < b ∧ succ a ≠ b
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
s : Set α
b : α
hb : b ∈ s
hs : IsLUB s b
ha : b ∉ s
⊢ ¬IsMin b

pp: case inr
α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb✝ : b ∈ s
hb : b < a
⊢ ¬IsMin a

Tactic:
· contradiction

Goal state after:
case inr
α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb✝ : b ∈ s
hb : b < a
⊢ ¬IsMin a
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a b : α
inst✝ : NoMaxOrder α
⊢ Ioo a b = ∅ ↔ b ≤ succ a

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · contrapose! h
    exact ⟨succ a, lt_succ_iff_not_isMax.mpr (not_isMax a), h⟩
  · ext x
    suffices a < x → b ≤ x by simpa
    exact fun hx ↦ le_of_lt_succ <| lt_of_le_of_lt h <| succ_strictMono hx

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: case coe
α : Type u_1
inst✝⁶ : PartialOrder α
inst✝⁵ : AddZeroClass α
inst✝⁴ : OrderBot α
inst✝³ : IsBotZeroClass α
inst✝² : One α
inst✝¹ : NoMaxOrder α
inst✝ : SuccAddOrder α
a : α
⊢ (↑a).succ = 0 ↔ ↑a = ⊥

Tactic:
simp only [WithBot.succ_coe, WithBot.coe_ne_bot, iff_false, succ_eq_add_one]

Goal state after:
case coe
α : Type u_1
inst✝⁶ : PartialOrder α
inst✝⁵ : AddZeroClass α
inst✝⁴ : OrderBot α
inst✝³ : IsBotZeroClass α
inst✝² : One α
inst✝¹ : NoMaxOrder α
inst✝ : SuccAddOrder α
a : α
⊢ ¬a + 1 = 0
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝¹ a✝ : α
h : a✝ < a✝¹
ha : IsMax a✝
⊢ ⊤ ≤ ↑a✝¹

Tactic:
exact (ha.not_lt h).elim

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

Goal state before:
pp: n : ℕ∞
hn0 : n ≠ 0
hxt : n ≠ ⊤
⊢ 0 < n.toNat

Tactic:
rw [pos_iff_ne_zero, ne_eq, ENat.toNat_eq_zero, not_or]
  exact ⟨hn0, hxt⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
X : Type u_3
Y : Type u_4
inst✝² : Preorder X
inst✝¹ : Preorder Y
inst✝ : SuccOrder X
f : X ≃o Y
y : Y
⊢ y ≤ f (succ (f.symm y))

Tactic:
← map_inv_le_iff f

Goal state after:
α : Type u_1
β : Type u_2
X : Type u_3
Y : Type u_4
inst✝² : Preorder X
inst✝¹ : Preorder Y
inst✝ : SuccOrder X
f : X ≃o Y
y : Y
⊢ EquivLike.inv f y ≤ succ (f.symm y)
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case none
hx : none < ⊤
⊢ lift none hx = toNat none

pp: case some
x : ℕ
hx : some x < ⊤
⊢ lift (some x) hx = toNat (some x)

Tactic:
· contradiction

Goal state after:
case some
x : ℕ
hx : some x < ⊤
⊢ lift (some x) hx = toNat (some x)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case pos.h₀
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∈ s
⊢ ∀ b_1 ∈ s, b_1 ≠ a → (if h : a = b_1 then b b_1 h else 1) = 1

pp: case pos.h₁
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∈ s
⊢ a ∉ s → (if h : a = a then b a h else 1) = 1

Tactic:
· intro _ _ h
      rw [dif_neg]
      exact h.symm

Goal state after:
case pos.h₁
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∈ s
⊢ a ∉ s → (if h : a = a then b a h else 1) = 1
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Fintype β
u : Finset (α ⊕ β)
⊢ u.toLeft = ∅ ↔ u ⊆ map Function.Embedding.inr univ

Tactic:
by simp [subset_map_inr]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : CommMonoid M
f : ι → M
a : ι
s : Finset ι
ha : a ∈ s
⊢ f a ∣ ∏ i ∈ s, f i

Tactic:
by
  classical
    rw [Finset.prod_eq_mul_prod_sdiff_singleton_of_mem ha]
    exact dvd_mul_right _ _

Goal state after: