mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
ih : toFunAux (ofNat s n) = n
h₁ : ↑(ofNat s n) ∉ {x ∈ range ↑(ofNat s n) | x ∈ s}
m : ℕ
h : m < ↑(succ (ofNat s n)) ∧ m ∈ s
⊢ m = ↑(ofNat s n) ∨ m < ↑(ofNat s n)

Tactic:
exact Or.symm (lt_or_eq_of_le ((@lt_succ_iff_le _ _ _ ⟨m, h.2⟩ _).1 h.1))

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
hx : x ∈ y :: l
⊢ a ≤ foldr max ⊥ (y :: l)

Tactic:
obtain hl | hl := hx

Goal state after:
case cons.head
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
⊢ a ≤ foldr max ⊥ (x :: l)

case cons.tail
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a x : α
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max ⊥ l
a✝ : Mem x l
⊢ a ≤ foldr max ⊥ (y :: l)
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ {a}.max = ↑a

Tactic:
← insert_empty_eq

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ (insert a ∅).max = ↑a
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ {a}.min = ↑a

Tactic:
← insert_empty_eq

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ (insert a ∅).min = ↑a
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
H : s.Nonempty
⊢ s.min = ↑(s.min' H)

Tactic:
simp only [Finset.min, min', id_eq, coe_inf', Function.comp_def]

Goal state after:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
n : ℕ
a : α
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ sublistsLenAux (n + 1) (a :: l) (g ∘ f) (map g r ++ s) = map g (sublistsLenAux (n + 1) (a :: l) f r) ++ s

Tactic:
unfold sublistsLenAux
    simp only [show (g ∘ f) ∘ List.cons a = g ∘ f ∘ List.cons a by rfl,
      sublistsLenAux_append]

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
i : Finset α
hi : i ⊆ s
j : Finset α
hj : j ⊆ s
⊢ (i = insert a j → i = j) ∧ (insert a i = j → i = j) ∧ (insert a i = insert a j → i = j)

Tactic:
refine ⟨?_, ?_, insert_erase_invOn.2.injOn (notMem_mono hi ha) (notMem_mono hj ha)⟩

Goal state after:
case refine_1
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
i : Finset α
hi : i ⊆ s
j : Finset α
hj : j ⊆ s
⊢ i = insert a j → i = j

case refine_2
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
i : Finset α
hi : i ⊆ s
j : Finset α
hj : j ⊆ s
⊢ insert a i = j → i = j
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
s : Finset (Option α)
⊢ #(eraseNone s) ≤ #s

Tactic:
rw [card_eraseNone_eq_card_erase]

Goal state after:
α : Type u_1
s : Finset (Option α)
⊢ #(s.erase none) ≤ #s
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
f : ι → α
⊢ univ.sup' ⋯ f = ⨆ i, f i

Tactic:
by
  simp [sup'_eq_csSup_image, iSup]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
x✝ : IsTop b ∧ a ⋖ b
hb : IsTop b
hab : a ⋖ b
⊢ Ioi a = {b}

Tactic:
cases b, hb using IsTop.rec

Goal state after:
case top
α : Type u_1
inst✝¹ : LinearOrder α
a : α
inst✝ : OrderTop α
x✝ : IsTop ⊤ ∧ a ⋖ ⊤
hab : a ⋖ ⊤
⊢ Ioi a = {⊤}
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case succ.inl.inr
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
l : ℕ
ha : 0 < a
hkl : n % a = l % a
hkn : n + a ≠ n
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ n ∈ ↑(Ico n (n + a))

Tactic:
simpa using Nat.lt_add_of_pos_right (n := n) ha

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

Goal state before:
pp: case succ.inr.inl
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = n % a
hln : n + a ≠ n
⊢ n ∈ ↑(Ico n (n + a))

Tactic:
simpa using Nat.lt_add_of_pos_right (n := n) ha

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → ¬IsMax a → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.univ.Nonempty
⊢ ∃ a, IsMin (a 0) ∧ ∃ n, IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)

Tactic:
let a : ℕ → α := Nat.rec (wfl.wf.min _ hα) fun _n a ↦ if ha : IsMax a then a else next ha

Goal state after:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → ¬IsMax a → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.univ.Nonempty
a : ℕ → α := fun t ↦ Nat.rec (⋯.min Set.univ hα) (fun _n a ↦ if ha : IsMax a then a else next ha) t
⊢ ∃ a, IsMin (a 0) ∧ ∃ n, IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case succ
n✝ : ℕ
⊢ Ico (n✝ + 1 - 1 + 1 - (n✝ + 1)) (n✝ + 1 - 1 + 1 - 0) = Ico 0 (n✝ + 1)

Tactic:
succ_sub_succ,

Goal state after:
case succ
n✝ : ℕ
⊢ Ico (n✝ - 0 - n✝) (n✝ - 0 + 1 - 0) = Ico 0 (n✝ + 1)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Set.Ioo a b ⊆ Set.Ico a b

Tactic:
exact Set.Ioo_subset_Ico_self

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a b c : α
h : ∀ (a_1 : α), a_1 ∈ (fun b ↦ [[b, a]]) b ↔ a_1 ∈ (fun b ↦ [[b, a]]) c
⊢ b = c

Tactic:
exact eq_of_mem_uIcc_of_mem_uIcc ((h _).1 left_mem_uIcc) ((h _).2 left_mem_uIcc)

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inr.refine_1
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
⊢ (f (g 0)).length.pred < (f (g 0)).length

Tactic:
exact Nat.pred_lt fun con => hnil _ (List.length_eq_zero_iff.1 con)

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.ConjAct

Goal state before:
pp: G : Type u_3
inst✝ : Group G
g : G
⊢ centralizer {g} = comap toConjAct.toMonoidHom (stabilizer (ConjAct G) g)

Tactic:
ext k
-- NOTE: `Subgroup.mem_centralizer_iff` should probably be stated
-- with the equality in the other direction
  simp only [mem_centralizer_iff, Set.mem_singleton_iff, forall_eq]
  rw [eq_comm]
  exact Iff.symm mul_inv_eq_iff_eq_mul

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
hs : closure s = ⊤
⊢ centralizer s = ⨅ g ∈ s, centralizer {g}

Tactic:
centralizer_eq_iInf

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
hs : closure s = ⊤
⊢ ⨅ g ∈ s, centralizer {g} = ⨅ g ∈ s, centralizer {g}
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
hα : WellFounded (rα on f)
hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)
⊢ WellFounded (Prod.Lex rα rβ on fun c ↦ (f c, g c))

Tactic:
by
  refine ((psigma_lex (wellFoundedOn_range.2 hα) fun a => hβ a).onFun
    (f := fun c => ⟨⟨_, c, rfl⟩, c, rfl⟩)).mono fun c c' h => ?_
  obtain h' | h' := Prod.lex_iff.1 h
  · exact PSigma.Lex.left _ _ h'
  · dsimp only [InvImage, (· on ·)] at h' ⊢
    convert! PSigma.Lex.right (⟨_, c', rfl⟩ : range f) _ using 1; swap
    exacts [⟨c, h'.1⟩, PSigma.subtype_ext (Subtype.ext h'.1) rfl, h'.2]

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

Goal state before:
pp: α : Type u_3
inst✝ : Monoid α
l : List α
comm : {x | x ∈ ↑l}.Pairwise Commute
⊢ (↑l).noncommProd comm = l.prod

Tactic:
noncommProd

Goal state after:
α : Type u_3
inst✝ : Monoid α
l : List α
comm : {x | x ∈ ↑l}.Pairwise Commute
⊢ noncommFold (fun x1 x2 ↦ x1 * x2) (↑l) comm 1 = l.prod
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
ι : Type u_5
s : Set ι
H : ι → Subgroup G
h : ∀ i ∈ s, (H i).Normal
⊢ (⨆ i ∈ s, H i).Normal

Tactic:
rw [← iSup_subtype'']

Goal state after:
G : Type u_2
inst✝ : Group G
ι : Type u_5
s : Set ι
H : ι → Subgroup G
h : ∀ i ∈ s, (H i).Normal
⊢ (⨆ i, H ↑i).Normal
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case head
α : Type u
p : α × Bool
LL₁ c✝ L₁ L₂ : List (α × Bool)
h : ReflTransGen Step c✝ (p :: L₂)
ih : ∀ {L₁ L₂_1 : List (α × Bool)}, p :: L₁ = c✝ → p :: L₂_1 = p :: L₂ → Red L₁ L₂_1
h₁₂ : Step (p :: L₁) c✝
⊢ Red L₁ L₂

Tactic:
obtain ⟨a, b⟩ := p

Goal state after:
case head
α : Type u
LL₁ c✝ L₁ L₂ : List (α × Bool)
a : α
b : Bool
h : ReflTransGen Step c✝ ((a, b) :: L₂)
ih : ∀ {L₁ L₂_1 : List (α × Bool)}, (a, b) :: L₁ = c✝ → (a, b) :: L₂_1 = (a, b) :: L₂ → Red L₁ L₂_1
h₁₂ : Step ((a, b) :: L₁) c✝
⊢ Red L₁ L₂
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case tail.inl
α : Type u
L₁₂ L₁ e : List (α × Bool)
a : α
b : Bool
s' : List (α × Bool)
eq : L₁ ++ (s' ++ e) = L₁ ++ s' ++ e
this : L₁ ++ (s' ++ (a, b) :: (a, !b) :: e) = L₁ ++ s' ++ (a, b) :: (a, !b) :: e
w₁ w₂ : List (α × Bool)
hLL' : ReflTransGen Step (w₁ ++ w₂) (L₁ ++ s' ++ (a, b) :: (a, !b) :: e)
ih :
  ∀ {L₁_1 L₂ : List (α × Bool)},
    L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e → ∃ L₃ L₄, w₁ ++ w₂ = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂
h₁ : Red w₁ L₁
h₂ : Red w₂ (s' ++ (a, b) :: (a, !b) :: e)
⊢ ∃ L₃ L₄, w₁ ++ w₂ = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ (s' ++ e)

Tactic:
exact ⟨w₁, w₂, rfl, h₁, h₂.tail Step.not⟩

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

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
⊢ f a * ∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ insert a s.toFinset, f x ^ count x (a :: s)

pp: case neg
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∉ s.toFinset
⊢ f a * ∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ insert a s.toFinset, f x ^ count x (a :: s)

Tactic:
· rw [insert_eq_of_mem has, ← insert_erase has, prod_insert (notMem_erase _ _),
      prod_insert (notMem_erase _ _), ← mul_assoc, count_cons_self, pow_succ']
    congr 1
    refine prod_congr rfl fun x hx => ?_
    rw [count_cons_of_ne (ne_of_mem_erase hx).symm]

Goal state after:
case neg
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∉ s.toFinset
⊢ f a * ∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ insert a s.toFinset, f x ^ count x (a :: s)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq M
m : Multiset M
s : Finset M
hs : m.toFinset ⊆ s
⊢ m.prod = ∏ i ∈ s, i ^ Multiset.count i m

Tactic:
by
  revert hs
  refine Quot.induction_on m fun l => ?_
  simp only [quot_mk_to_coe'', prod_coe, coe_count]
  apply prod_list_count_of_subset l s

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
inst✝⁵ : Monoid M✝
G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : AddGroup H
ι : Type u_5
inst✝² : Finite ι
M : ι → Type u_6
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : ∀ (i : ι), Monoid.FG (M i)
⊢ ⊤.FG

Tactic:
← Submonoid.pi_top Set.univ

Goal state after:
M✝ : Type u_1
N : Type u_2
inst✝⁵ : Monoid M✝
G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : AddGroup H
ι : Type u_5
inst✝² : Finite ι
M : ι → Type u_6
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : ∀ (i : ι), Monoid.FG (M i)
⊢ (Submonoid.pi Set.univ fun i ↦ ⊤).FG
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
inst✝ : AddCommGroup G
f g : α → G
a : FreeAbelianGroup α
⊢ (lift (f + g)) a = (lift f) a + (lift g) a

Tactic:
by
  induction a using FreeAbelianGroup.induction_on with
  | zero => simp only [(lift _).map_zero, zero_add]
  | of x => simp only [lift_apply_of, Pi.add_apply]
  | neg x => simp only [map_neg, lift_apply_of, Pi.add_apply, neg_add]
  | add x y hx hy => simp only [(lift _).map_add, hx, hy, add_add_add_comm]

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

Goal state before:
pp: case insert
ι : Type u_1
M : Type u_4
α : Type u_5
inst✝ : CommMonoid M
m : Multiset ι
f : ι → α → M
a : α
s : Finset α
ha : a ∉ s
ih : (map (fun i ↦ ∏ a ∈ s, f i a) m).prod = ∏ a ∈ s, (map (fun i ↦ f i a) m).prod
⊢ (map (fun i ↦ ∏ a ∈ insert a s, f i a) m).prod = ∏ a ∈ insert a s, (map (fun i ↦ f i a) m).prod

Tactic:
simp [Finset.prod_insert ha, prod_map_mul, ih]

Goal state after:
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.10
inst✝ : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩
x✝² x✝¹ : X × ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
x✝ : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • (r₂, s₂).fst = v • (r₁, s₁).fst
hs₂ : ↑u * ↑(r₂, s₂).snd = v * ↑(r₁, s₁).snd
⊢ P (r₁, s₁).fst (r₁, s₁).snd = P (r₂, s₂).fst (r₂, s₂).snd

Tactic:
by
    dsimp at *
    have s₁vS : v * s₁ ∈ S := by
      rw [← hs₂, ← S.coe_mul]
      exact SetLike.coe_mem (u * s₂)
    replace hs₂ : u * s₂ = ⟨_, s₁vS⟩ := by ext; simp [hs₂]
    rw [hP r₁ v s₁ s₁vS, hP r₂ u s₂ (by norm_cast; rwa [hs₂]), ← hr₂]
    simp only [← hs₂]; rfl

Goal state after:
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
g₁ g₂ : α ≃*o β
f : β ≃*o γ
hf : Injective ⇑f
h : g₁.trans f = g₂.trans f
a : α
⊢ f (g₁ a) = f (g₂ a)

Tactic:
← trans_apply,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
g₁ g₂ : α ≃*o β
f : β ≃*o γ
hf : Injective ⇑f
h : g₁.trans f = g₂.trans f
a : α
⊢ (g₁.trans f) a = f (g₂ a)
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)
⊢ Surjective ⇑(f.lift hg) ↔ ∀ (v : P), ∃ x, v * g ↑x.2 = g x.1

Tactic:
constructor
  · intro H v
    obtain ⟨z, hz⟩ := H v
    obtain ⟨x, hx⟩ := f.surj z
    use x
    rw [← hz, f.eq_mk'_iff_mul_eq.2 hx, lift_mk', mul_assoc, mul_comm _ (g ↑x.2),
      ← MonoidHom.domRestrict_apply, IsUnit.mul_liftRight_inv (g.domRestrict S) hg, mul_one]
  · intro H v
    obtain ⟨x, hx⟩ := H v
    use f.mk' x.1 x.2
    rw [lift_mk', mul_inv_left hg, mul_comm, ← hx]

Goal state after:
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

Goal state after:
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

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: case top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
⊢ ⊤ * (a + b) = ⊤ * a + ⊤ * b

Tactic:
by_cases ha : a = 0

Goal state after:
case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
ha : a = 0
⊢ ⊤ * (a + b) = ⊤ * a + ⊤ * b

case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
ha : ¬a = 0
⊢ ⊤ * (a + b) = ⊤ * a + ⊤ * b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
⊢ (a + b) * ⊤ = a * ⊤ + b * ⊤

Tactic:
by_cases ha : a = 0

Goal state after:
case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
ha : a = 0
⊢ (a + b) * ⊤ = a * ⊤ + b * ⊤

case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
ha : ¬a = 0
⊢ (a + b) * ⊤ = a * ⊤ + b * ⊤
Module: Mathlib.Order.Iterate

Goal state before:
pp: case hy
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ ∀ (k : ℕ), k < n → f (g^[k] x) ≤ g^[k + 1] x

Tactic:
· simp [h.iterate_right _ _, hg.iterate _ hx]

Goal state after:
Module: Mathlib.Order.Iterate

Goal state before:
pp: case hy
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ ∀ (k : ℕ), k < n → f (g^[k] x) < g^[k + 1] x

Tactic:
· simp [h.iterate_right _ _, hg.iterate _ hx]

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

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

Tactic:
by_cases ha : a = 0

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : a = 0
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b

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

Goal state before:
pp: case coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
x : α
x0 : 0 < ↑x
a✝ : α
h : ⊥ < ↑a✝
⊢ ⊥ * ↑x < ↑a✝ * ↑x

pp: case coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
x : α
x0 : 0 < ↑x
a✝¹ a✝ : α
h : ↑a✝ < ↑a✝¹
⊢ ↑a✝ * ↑x < ↑a✝¹ * ↑x

Tactic:
· simp_rw [bot_mul x0.ne.symm, ← coe_mul, bot_lt_coe]

Goal state after:
case coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
x : α
x0 : 0 < ↑x
a✝¹ a✝ : α
h : ↑a✝ < ↑a✝¹
⊢ ↑a✝ * ↑x < ↑a✝¹ * ↑x
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
x a✝¹ a✝ : α
h : a✝¹ * x ≤ a✝ * x
x0 : 0 < x
⊢ a✝¹ ≤ a✝

Tactic:
exact le_of_mul_le_mul_right h x0

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

Goal state before:
pp: case rfl
α : 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₀ : α
h : ∀ (a : α), ∃ a', f a < f a'
⊢ ∃ a, f a₀ < f a

pp: case succ
α : 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₀ : α
h : ∀ (a : α), ∃ a', f a < f a'
⊢ ∀ (n : β), f a₀ ≤ n → (∃ a, n < f a) → ∃ a, succ n < f a

Tactic:
· exact h a₀

Goal state after:
case succ
α : 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₀ : α
h : ∀ (a : α), ∃ a', f a < f a'
⊢ ∀ (n : β), f a₀ ≤ n → (∃ a, n < f a) → ∃ a, succ n < f a
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case neg.refine_1
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m n : X
hn' : n ≤ m
⊢ n ∈ upperBounds S → n ∈ S → n ∉ S → ∃ x, IsGreatest S x

pp: case neg.refine_2
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m n : X
hn' : n ≤ m
⊢ ∀ (n_1 : X),
    n ≤ n_1 →
      (n_1 ∈ upperBounds S → n ∈ S → n_1 ∉ S → ∃ x, IsGreatest S x) →
        succ n_1 ∈ upperBounds S → n ∈ S → succ n_1 ∉ S → ∃ x, IsGreatest S x

Tactic:
· simp +contextual

Goal state after:
case neg.refine_2
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m n : X
hn' : n ≤ m
⊢ ∀ (n_1 : X),
    n ≤ n_1 →
      (n_1 ∈ upperBounds S → n ∈ S → n_1 ∉ S → ∃ x, IsGreatest S x) →
        succ n_1 ∈ upperBounds S → n ∈ S → succ n_1 ∉ S → ∃ x, IsGreatest S x
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → ((b : α) → b < a → motive b) → motive a
hb : IsSuccLimit b
⊢ limitRecOn b isMin succ isSuccLimit = isSuccLimit b hb fun x x_1 ↦ limitRecOn x isMin succ isSuccLimit

Tactic:
rw [limitRecOn, prelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit, dif_neg hb.not_isMin]

Goal state after:
α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → ((b : α) → b < a → motive b) → motive a
hb : IsSuccLimit b
⊢ (isSuccLimit b ⋯ fun x x_1 ↦
      prelimitRecOn x succ fun a ha IH ↦ if h : IsMin a then isMin a h else isSuccLimit a ⋯ IH) =
    isSuccLimit b hb fun x x_1 ↦ limitRecOn x isMin succ isSuccLimit
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
n : ℕ
hi : ∀ (c : α) (hc : c ∈ s), b ≤ c → pred^[n] c = b → pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[n] (pred c) = b
h : pred ↑⟨c, hc⟩ ∉ s
this : pred ⟨c, hc⟩ = ⟨c, hc⟩
⊢ pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩

Tactic:
Function.iterate_fixed

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
n : ℕ
hi : ∀ (c : α) (hc : c ∈ s), b ≤ c → pred^[n] c = b → pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[n] (pred c) = b
h : pred ↑⟨c, hc⟩ ∉ s
this : pred ⟨c, hc⟩ = ⟨c, hc⟩
⊢ ⟨c, hc⟩ = ⟨b, hb⟩

case neg.h
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
n : ℕ
hi : ∀ (c : α) (hc : c ∈ s), b ≤ c → pred^[n] c = b → pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[n] (pred c) = b
h : pred ↑⟨c, hc⟩ ∉ s
this : pred ⟨c, hc⟩ = ⟨c, hc⟩
⊢ pred ⟨c, hc⟩ = ⟨c, hc⟩
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: m : ℕ∞
n : ℕ
h : m ≤ ↑n
⊢ m.toNat ≤ n

Tactic:
lift m to ℕ using ne_top_of_le_ne_top (natCast_ne_top n) h
  simpa using h

Goal state after:
Module: Mathlib.Algebra.BigOperators.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : CommMonoid M
f : α → M
s : Finset (Option α)
⊢ ∏ x ∈ map Embedding.some (eraseNone s), Option.elim' 1 f x = ∏ x ∈ s.erase none, Option.elim' 1 f x

Tactic:
by rw [map_some_eraseNone]

Goal state after: