mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case refine_2
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : F
s : Finset ι
hs : s.Nonempty
g : ι → α
⊢ ∀ (a : ι) (s : Finset ι) (h : a ∉ s) (hs : s.Nonempty),
    f (s.sup' hs g) = s.sup' hs (⇑f ∘ g) → f ((cons a s h).sup' ⋯ g) = (cons a s h).sup' ⋯ (⇑f ∘ g)

Tactic:
intros

Goal state after:
case refine_2
F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : F
s : Finset ι
hs : s.Nonempty
g : ι → α
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
hs✝ : s✝.Nonempty
a✝ : f (s✝.sup' hs✝ g) = s✝.sup' hs✝ (⇑f ∘ g)
⊢ f ((cons a✝¹ s✝ h✝).sup' ⋯ g) = (cons a✝¹ s✝ h✝).sup' ⋯ (⇑f ∘ g)
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
⊢ count b (∅.sup f) = ∅.sup fun a ↦ count b (f a)

pp: case refine_2
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
⊢ ∀ (a : α) (s : Finset α),
    a ∉ s →
      (count b (s.sup f) = s.sup fun a ↦ count b (f a)) →
        count b ((insert a s).sup f) = (insert a s).sup fun a ↦ count b (f a)

Tactic:
· exact count_zero _

Goal state after:
case refine_2
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
⊢ ∀ (a : α) (s : Finset α),
    a ∉ s →
      (count b (s.sup f) = s.sup fun a ↦ count b (f a)) →
        count b ((insert a s).sup f) = (insert a s).sup fun a ↦ count b (f a)
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompletePartialOrderSup α
f : β → α
s : Set β
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (f '' s)
H : BddAbove (f '' s)
Hne : s.Nonempty
⊢ IsLUB (f '' s) (⨆ i, f ↑i)

Tactic:
rw [← sSup_image']
  exact hd.isLUB_csSup (Hne.image _) H

Goal state after:
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : Preorder β
f : β → α
a : β
hf : Monotone f
hd : Directed (fun x1 x2 ↦ x1 ≤ x2) fun x ↦ f ↑x
H : BddAbove (range fun x ↦ f ↑x)
⊢ ⨆ j, f ↑j ≤ f ↑⟨a, ⋯⟩

Tactic:
hd.ciSup_le_iff H

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : Preorder β
f : β → α
a : β
hf : Monotone f
hd : Directed (fun x1 x2 ↦ x1 ≤ x2) fun x ↦ f ↑x
H : BddAbove (range fun x ↦ f ↑x)
⊢ ∀ (i : ↑(Iic a)), f ↑i ≤ f ↑⟨a, ⋯⟩
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inr.refine_1
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup f < sSup ∅
i : ι
hi : ¬p i
this : Nonempty ι
bdd : BddAbove (range f)
j : ι
⊢ ⨆ (h : p j), f ⟨j, h⟩ ≤ sSup ∅

Tactic:
by_cases hj : p j
    · exact ((ciSup_pos hj).trans_le (le_ciSup bdd ⟨j, hj⟩)).trans gt.le
    · exact (ciSup_neg hj).le

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

Goal state before:
pp: α : Type u
β : Type v
f : α ↪ β
s : Finset α
t : Finset β
⊢ map f s ⊆ t ↔ s ⊆ t.preimage ⇑f ⋯

Tactic:
classical rw [map_eq_image, image_subset_iff_subset_preimage]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
wf : WellFoundedLT α
a : α
h : ¬IsMax a
⊢ ∃ a', a ⋖ a'

Tactic:
rw [not_isMax_iff] at h
  exact ⟨_, wellFounded_lt.min_mem (Ioi a) h, fun a' ↦ wf.wf.not_lt_min (Ioi a)⟩

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

Goal state before:
pp: a b c : ℕ
hac : a ≤ c
⊢ image (fun x ↦ c - x) (Ico a b) = Ico (c + 1 - b) (c + 1 - a)

Tactic:
by
  ext x
  simp_rw [mem_image, mem_Ico]
  refine ⟨?_, fun h ↦ ⟨c - x, by lia⟩⟩
  rintro ⟨x, hx, rfl⟩
  lia

Goal state after:
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: case refine_1
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
m : ℕ
hm : m ∈ {m | p m}
⊢ m + n ∈ {m | p (m - n)}

pp: case refine_2
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
m : ℕ
hm : m ∈ {m | p m}
b : ℕ
hb : b ∈ {m | p (m - n)}
hbn : b < n
⊢ b - n ∈ {m | p m}

Tactic:
· dsimp
    rwa [Nat.add_sub_cancel_right]

Goal state after:
case refine_2
n : ℕ
p : ℕ → Prop
h : 0 < sInf {m | p m}
m : ℕ
hm : m ∈ {m | p m}
b : ℕ
hb : b ∈ {m | p (m - n)}
hbn : b < n
⊢ b - n ∈ {m | p m}
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
a b x : α × β
⊢ (a.1 ≤ x.1 ∧ a.2 ≤ x.2) ∧ x.1 ≤ b.1 ∧ x.2 ≤ b.2 ↔ (a.1 ≤ x.1 ∧ a.2 ≤ x.2) ∧ x ≤ b

Tactic:
le_def

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
a b x : α × β
⊢ (a.1 ≤ x.1 ∧ a.2 ≤ x.2) ∧ x.1 ≤ b.1 ∧ x.2 ≤ b.2 ↔ (a.1 ≤ x.1 ∧ a.2 ≤ x.2) ∧ x.1 ≤ b.1 ∧ x.2 ≤ b.2
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : LocallyFiniteOrderTop β
inst✝ : DecidableLE (α × β)
a x : α × β
⊢ a.1 ≤ x.1 ∧ a.2 ≤ x.2 ↔ a ≤ x

Tactic:
le_def

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : LocallyFiniteOrderTop β
inst✝ : DecidableLE (α × β)
a x : α × β
⊢ a.1 ≤ x.1 ∧ a.2 ≤ x.2 ↔ a.1 ≤ x.1 ∧ a.2 ≤ x.2
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
⊢ WellQuasiOrdered r ↔ ∀ (f : ℕ → α), ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

Tactic:
by
  constructor <;> intro h f
  · exact h.exists_monotone_subseq f
  · obtain ⟨g, gmon⟩ := h f
    exact ⟨_, _, g.strictMono Nat.zero_lt_one, gmon _ _ (Nat.zero_le 1)⟩

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: case a
G : Type u_2
inst✝ : Group G
s : Set G
⊢ s⁻¹⁻¹ ⊆ ↑(closure s)

Tactic:
inv_inv

Goal state after:
case a
G : Type u_2
inst✝ : Group G
s : Set G
⊢ s ⊆ ↑(closure s)
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: case comm
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ⋯
⊢ ∀ (a : N), Commute (e x) a

Tactic:
intros

Goal state after:
case comm
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ↑e✝
a✝ : N
⊢ Commute (e x) a✝
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: case left_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ⋯
⊢ ∀ (b c : N), e x * (b * c) = e x * b * c

Tactic:
intros

Goal state after:
case left_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ↑e✝
b✝ c✝ : N
⊢ e x * (b✝ * c✝) = e x * b✝ * c✝
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: case right_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ⋯
⊢ ∀ (a b : N), a * b * e x = a * (b * e x)

Tactic:
intros

Goal state after:
case right_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ↑e✝
a✝ b✝ : N
⊢ a✝ * b✝ * e x = a✝ * (b✝ * e x)
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : DivisionMonoid M
a : M
ha : a ∈ center M
g✝ : M
⊢ g✝⁻¹ * a = g✝⁻¹ * a⁻¹⁻¹

Tactic:
inv_inv

Goal state after:
M : Type u_1
inst✝ : DivisionMonoid M
a : M
ha : a ∈ center M
g✝ : M
⊢ g✝⁻¹ * a = g✝⁻¹ * a
Module: Mathlib.GroupTheory.GroupAction.ConjAct

Goal state before:
pp: G : Type u_3
inst✝ : Group G
g h : G
⊢ g⁻¹ * h * g⁻¹⁻¹ = g⁻¹ * h * g

Tactic:
inv_inv

Goal state after:
G : Type u_3
inst✝ : Group G
g h : G
⊢ g⁻¹ * h * g = g⁻¹ * h * g
Module: Mathlib.GroupTheory.GroupAction.ConjAct

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Group G
⊢ ∀ (x y : ConjAct G) (b : G), (x * y) • b = x • y • b

Tactic:
by simp [smul_def, mul_assoc]

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

Goal state before:
pp: G : Type u_3
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
g : G
h : ↥H
⊢ ofConjAct (toConjAct.toMonoidHom g)⁻¹ * ↑h * g⁻¹⁻¹ = g⁻¹ * ↑h * g

Tactic:
inv_inv

Goal state after:
G : Type u_3
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
g : G
h : ↥H
⊢ ofConjAct (toConjAct.toMonoidHom g)⁻¹ * ↑h * g = g⁻¹ * ↑h * g
Module: Mathlib.GroupTheory.GroupAction.ConjAct

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Monoid M
x : Mˣ
u : (↥(Submonoid.centralizer {↑x}))ˣ
⊢ ConjAct.toConjAct ((Units.map (Submonoid.centralizer {↑x}).subtype) u) ∈ MulAction.stabilizer (ConjAct Mˣ) x

Tactic:
change _ • _ = _

Goal state after:
α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Monoid M
x : Mˣ
u : (↥(Submonoid.centralizer {↑x}))ˣ
⊢ ConjAct.toConjAct ((Units.map (Submonoid.centralizer {↑x}).subtype) u) • x = x
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inr.convert_6
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c ↦ ⟨f c, g (f c) c⟩) c c'
h' : f c = f c'
h'' :
  rπ ((fun c ↦ ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c ↦ ⟨f c, g (f c) c⟩) c).snd) ((fun c ↦ ⟨f c, g (f c) c⟩) c').snd
⊢ Subrel (rπ ↑⟨f c', ⋯⟩ on g ↑⟨f c', ⋯⟩) (fun x ↦ x ∈ f ⁻¹' {↑⟨f c', ⋯⟩}) ⟨c, h'⟩ ⟨c', ⋯⟩

Tactic:
dsimp only [Subtype.coe_mk, Subrel, Order.Preimage] at *

Goal state after:
case inr.convert_6
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c ↦ ⟨f c, g (f c) c⟩) c c'
h' : f c = f c'
h'' : rπ (f c') (h' ▸ g (f c) c) (g (f c') c')
⊢ (rπ (f c') on g (f c')) c c'
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
⊢ ↑(closure s) * s = ↑(closure s)

Tactic:
by
  rw [← Set.iUnion_op_smul_set]
  have h a (ha : a ∈ s) : (closure s : Set G) <• a = closure s :=
    op_smul_coe_set <| subset_closure ha
  simp +contextual [h, hs]

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

Goal state before:
pp: M : Type u_3
inst✝ : Monoid M
s : List M
⊢ ofMul s.prod = (List.map (⇑ofMul) s).sum

Tactic:
simp [ofMul]; rfl

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

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
s : Multiset M
⊢ ofMul s.prod = (Multiset.map (⇑ofMul) s).sum

Tactic:
simp [ofMul]; rfl

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ d c : Con M
⊢ ∀ (x y : M), id (x * y) = id x * id y

Tactic:
intros

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ d c : Con M
x✝ y✝ : M
⊢ id (x✝ * y✝) = id x✝ * id y✝
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
⊢ Red L [(x, !b)]

Tactic:
have h₁ : Red ((x, not b) :: (x, b) :: L) [(x, not b)] := cons_cons h
      have h₂ : Red ((x, not b) :: (x, b) :: L) L := ReflTransGen.single Step.cons_not_rev
      let ⟨L', h₁, h₂⟩ := church_rosser h₁ h₂
      rw [singleton_iff] at h₁
      subst L'
      assumption

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
a b : α
⊢ (leftRel s) a b ↔ a⁻¹ * b ∈ s

Tactic:
by rw [leftRel_apply]

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
f : G →* M
x✝ y✝ : G
⊢ y✝⁻¹ * x✝ ∈ f.ker ↔ f x✝ = f y✝

Tactic:
MonoidHom.eq_iff

Goal state after:
G : Type u_1
M : Type u_4
inst✝¹ : Group G
inst✝ : Monoid M
f : G →* M
x✝ y✝ : G
⊢ y✝⁻¹ * x✝ ∈ f.ker ↔ y✝⁻¹ * x✝ ∈ f.ker
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : MulOneClass I
f : G →* H
inst✝ : f.range.Normal
g : H →* I
h : (mk' f.range).comp g.ker.subtype = 1
x : H
hx : x ∈ g.ker
⊢ ↑x = 1

Tactic:
exact DFunLike.congr_fun h ⟨x, hx⟩

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

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

Tactic:
simp [← ih]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
R : Setoid ι
inst✝ : DecidableRel ⇑R
h : ∀ x ∈ s, ∏ a ∈ s with R a x, f a = 1
⊢ ∏ x ∈ s, f x = 1

Tactic:
prod_partition R,

Goal state after:
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
R : Setoid ι
inst✝ : DecidableRel ⇑R
h : ∀ x ∈ s, ∏ a ∈ s with R a x, f a = 1
⊢ ∏ xbar ∈ image (Quotient.mk R) s, ∏ y ∈ s with ⟦y⟧ = xbar, f y = 1
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x y z₁ z₂ : FreeAbelianGroup α
ih₁ : x * y * z₁ = x * (y * z₁)
ih₂ : x * y * z₂ = x * (y * z₂)
⊢ x * y * (z₁ + z₂) = x * (y * (z₁ + z₂))

Tactic:
| add z₁ z₂ ih₁ ih₂ =>

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MulOneClass γ
inst✝ : MulOneClass δ
f✝ g✝ f g : α →*o β
h : (fun f ↦ (↑f.toMonoidHom).toFun) f = (fun f ↦ (↑f.toMonoidHom).toFun) g
⊢ f = g

Tactic:
obtain ⟨⟨⟨_, _⟩⟩, _⟩ := f
    obtain ⟨⟨⟨_, _⟩⟩, _⟩ := g
    congr

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : Mul γ
inst✝ : Mul δ
f✝ g✝ f g : α ≃*o β
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
⊢ f = g

Tactic:
obtain ⟨⟨⟨_, _⟩⟩, _⟩ := f
    obtain ⟨⟨⟨_, _⟩⟩, _⟩ := g
    congr

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 y : M × ↥S
⊢ (f.lift hg) (f.mk' x.1 x.2) = (f.lift hg) (f.mk' y.1 y.2) ↔ g (x.1 * ↑y.2) = g (y.1 * ↑x.2)

Tactic:
rw [lift_mk', lift_mk', mul_inv hg]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulZeroOneClass α
inst✝² : MulZeroOneClass β
inst✝¹ : MulZeroOneClass γ
inst✝ : MulZeroOneClass δ
f✝ g✝ f g : α →*₀o β
h : (fun f ↦ (↑f.toMonoidWithZeroHom).toFun) f = (fun f ↦ (↑f.toMonoidWithZeroHom).toFun) g
⊢ f = g

Tactic:
obtain ⟨⟨⟨_, _⟩⟩, _⟩ := f
    obtain ⟨⟨⟨_, _⟩⟩, _⟩ := g
    congr

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
f : S.LocalizationMap N
z w : N
⊢ ∃ z' w' d, z * f ↑d = f z' ∧ w * f ↑d = f w'

Tactic:
let ⟨a, ha⟩ := surj f z
  let ⟨b, hb⟩ := surj f w
  refine ⟨a.1 * b.2, a.2 * b.1, a.2 * b.2, ?_, ?_⟩
  · simp_rw [mul_def, map_mul, ← ha]
    exact (mul_assoc z _ _).symm
  · simp_rw [mul_def, map_mul, ← hb]
    exact mul_left_comm w _ _

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

Goal state before:
pp: case c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
z : OreLocalization S X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
⊢ (r₁ /ₒ s₁ * (r₂ /ₒ s₂)) • z = (r₁ /ₒ s₁) • (r₂ /ₒ s₂) • z

Tactic:
cases z with | _ r₃ s₃

Goal state after:
case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
⊢ (r₁ /ₒ s₁ * (r₂ /ₒ s₂)) • (r₃ /ₒ s₃) = (r₁ /ₒ s₁) • (r₂ /ₒ s₂) • (r₃ /ₒ s₃)
Module: Mathlib.Algebra.Order.Sub.WithTop

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Sub α
inst✝² : Bot α
inst✝¹ : Sub β
inst✝ : Bot β
f : α → β
h : ∀ (x y : α), f (x - y) = f x - f y
h₀ : f ⊥ = ⊥
x y : α
⊢ map f (↑x - ↑y) = map f ↑x - map f ↑y

Tactic:
by simp only [← coe_sub, map_coe, h]

Goal state after:
Module: Mathlib.Order.Iterate

Goal state before:
pp: case hx
α : 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^[k + 1] x ≤ f (f^[k] x)

Tactic:
intros

Goal state after:
case hx
α : 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✝ : ℕ
a✝ : k✝ < n
⊢ f^[k✝ + 1] x ≤ f (f^[k✝] x)
Module: Mathlib.Order.Iterate

Goal state before:
pp: case hx
α : 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^[k + 1] x ≤ f (f^[k] x)

Tactic:
intros

Goal state after:
case hx
α : 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✝ : ℕ
a✝ : k✝ < n
⊢ f^[k✝ + 1] x ≤ f (f^[k✝] x)
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
m : α
P : (n : α) → m ≤ n → Prop
rfl : P m ⋯
succ : ∀ (n : α) (hmn : m ≤ n), P n hmn → P (Order.succ n) ⋯
n : α
hmn : m ≤ n
⊢ P n hmn

Tactic:
by
  obtain ⟨n, rfl⟩ := hmn.exists_succ_iterate
  induction n with
  | zero => exact rfl
  | succ n ih =>
    simp_rw [Function.iterate_succ_apply']
    exact succ _ (id_le_iterate_of_id_le le_succ n m) (ih _)

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 ∧ succ a ≠ b

Tactic:
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: α : Type u_1
b : α
motive : α → Sort u_2
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a
hb : ¬IsMax b
h : ¬IsSuccPrelimit (Order.succ b)
H : ¬IsMax (Classical.choose ⋯) ∧ Order.succ (Classical.choose ⋯) = Order.succ b
this :
  ∀ {a c : α} {ha : ¬IsMax a} {hc : ¬IsMax c} {x : (a : α) → motive a} (h : a = c),
    cast ⋯ (succ a ha (x a)) = succ c hc (x c)
⊢ cast ⋯
      (succ (Classical.choose ⋯) ⋯
        ((fun y x ↦
            ⋯.fix
              (fun a IH ↦
                if h : IsSuccPrelimit a then isSuccPrelimit a h IH
                else cast ⋯ (succ (Classical.choose ⋯) ⋯ (IH (Classical.choose ⋯) ⋯)))
              y)
          (Classical.choose ⋯) ⋯)) =
    succ b hb (prelimitRecOn b succ isSuccPrelimit)

Tactic:
exact this <| (succ_eq_succ_iff_of_not_isMax H.1 hb).1 H.2

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

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝ : (j : ι) → Decidable (j ∈ s)
i : ι
p : π i → Prop
hf : p (f i)
hg : p (g i)
⊢ p (s.piecewise f g i)

Tactic:
by
  by_cases hi : i ∈ s <;> simpa [hi]

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor✝¹ : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x *> y = const α id <$> x <*> y
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure✝¹ : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun h ↦ h x) <$> g
seq_assoc✝¹ : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
toLawfulFunctor✝ : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x *> y = const α id <$> x <*> y
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure✝ : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun h ↦ h x) <$> g
seq_assoc✝ : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
⊢ ∀ (α β : Type u) (f : α → β) (x : F α), f <$> x = f <$> x

Tactic:
intros

Goal state after:
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor✝¹ : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x *> y = const α id <$> x <*> y
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure✝¹ : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun h ↦ h x) <$> g
seq_assoc✝¹ : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
toLawfulFunctor✝ : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x *> y = const α id <$> x <*> y
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure✝ : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun h ↦ h x) <$> g
seq_assoc✝ : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
α✝ β✝ : Type u
f✝ : α✝ → β✝
x✝ : F α✝
⊢ f✝ <$> x✝ = f✝ <$> x✝