mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inr.convert_4
ι : 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
⊢ { x // x ∈ f ⁻¹' {↑⟨f c', ⋯⟩} }

pp: case e'_5
ι : 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
⊢ ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩ = ⟨⟨f c', ⋯⟩, ?inr.convert_4⟩

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', ⋯⟩}) ?inr.convert_4 ⟨c', ⋯⟩

Tactic:
· exact ⟨c, h'⟩

Goal state after:
case e'_5
ι : 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
⊢ ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩ = ⟨⟨f c', ⋯⟩, ⟨c, h'⟩⟩

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', ⋯⟩
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

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

Tactic:
subgroupClosure_mul hs,

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
n : ℕ
⊢ ↑(closure s) * s ^ n = ↑(closure s)
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case mul_left
G : Type u_2
inst✝ : Group G
s : Set G
p : (x : G) → x ∈ closure s → Prop
one : p 1 ⋯
x✝ : G
mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Submonoid.closure (s ∪ s⁻¹)), p y ⋯ → p (x * y) ⋯
inv_mul_cancel : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Submonoid.closure (s ∪ s⁻¹)), p y ⋯ → p (x⁻¹ * y) ⋯
x : G
hx : x ∈ s ∪ s⁻¹
y : G
hy : y ∈ Submonoid.closure (s ∪ s⁻¹)
ih : p y ⋯
⊢ p (x * y) ⋯

Tactic:
cases hx with
    | inl hx => exact mul_left _ hx _ hy ih
    | inr hx => simpa only [inv_inv] using inv_mul_cancel _ hx _ hy ih

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
m : β
h : ∀ x ∈ s, f x = m
⊢ m ^ (Multiset.map f s.val).card = m ^ #s

Tactic:
simp only [Finset.card_def, Multiset.card_map]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
s : Finset α
a : α
h : a ∈ s
f : α → β
comm : (↑s).Pairwise (Commute on f)
comm' : ∀ x ∈ ↑(s.erase a), ∀ x_1 ∈ ↑(s.erase a), x ≠ x_1 → (Commute on f) x x_1
⊢ f a * (s.erase a).noncommProd f comm' = s.noncommProd f comm

Tactic:
by
  classical
  simpa only [← Multiset.map_erase_of_mem _ _ h] using!
    Multiset.mul_noncommProd_erase (s.1.map f) (Multiset.mem_map_of_mem f h) _

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 : Con M
c : Con P
g : N → P
f : M → N
hg : ∀ (x y : N), g (x * y) = g x * g y
hf : ∀ (x y : M), f (x * y) = f x * f y
⊢ ∀ (x y : M), (g ∘ f) (x * y) = (g ∘ f) x * (g ∘ f) y

Tactic:
by grind

Goal state after:
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
f : F
w✝ x✝ y✝ z✝ : M
h1 : (Setoid.ker ⇑f) w✝ x✝
h2 : (Setoid.ker ⇑f) y✝ z✝
⊢ (Setoid.ker ⇑f) (w✝ * y✝) (x✝ * z✝)

Tactic:
by
    dsimp +instances [Setoid.ker, onFun] at *
    rw [map_mul, h1, h2, map_mul]

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
s : Finset ι
t : Finset κ
inst✝ : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : ι → M
⊢ ∏ j ∈ t, ∏ i ∈ s with g i = j, f i = ∏ i ∈ s, f i

Tactic:
rw [← prod_disjiUnion, disjiUnion_filter_eq_of_maps_to h]

Goal state after:
case h
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
s : Finset ι
t : Finset κ
inst✝ : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : ι → M
⊢ (↑t).PairwiseDisjoint fun j ↦ {i ∈ s | g i = j}
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 ι
s : Finset ι
f : ι → M
a : ι
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
h : a ∈ s
⊢ ∏ x ∈ s, f x = if a ∈ s then f a else 1

Tactic:
simp [Finset.prod_eq_single_of_mem a h h₀, h]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
have := Classical.decEq ι; by_cases h₁ : a ∈ s <;> by_cases h₂ : b ∈ s
  · exact prod_eq_mul_of_mem a b h₁ h₂ hn h₀
  · rw [hb h₂, mul_one]
    apply prod_eq_single_of_mem a h₁
    exact fun c hc hca => h₀ c hc ⟨hca, ne_of_mem_of_not_mem hc h₂⟩
  · rw [ha h₁, one_mul]
    apply prod_eq_single_of_mem b h₂
    exact fun c hc hcb => h₀ c hc ⟨ne_of_mem_of_not_mem hc h₁, hcb⟩
  · rw [ha h₁, hb h₂, mul_one]
    exact
      _root_.trans
        (prod_congr rfl fun c hc =>
          h₀ c hc ⟨ne_of_mem_of_not_mem hc h₁, ne_of_mem_of_not_mem hc h₂⟩)
        prod_const_one

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

Goal state before:
pp: case calc_3
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
b : κ
hb : b ∈ {x ∈ t | g x ≠ 1}
h₁ : b ∈ t
h₂ : g b ≠ 1
a : ι
ha₁ : a ∈ s
ha₂ : f a ≠ 1
eq : i a ha₁ ha₂ = b
⊢ ∃ a, ∃ (ha : a ∈ {x ∈ s | f x ≠ 1}), i a ⋯ ⋯ = b

Tactic:
exact ⟨a, mem_filter.mpr ⟨ha₁, ha₂⟩, eq⟩

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : Finite M
⊢ FG M

Tactic:
cases nonempty_fintype M
  exact ⟨⟨Finset.univ, by rw [Finset.coe_univ]; exact Submonoid.closure_univ⟩⟩

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

Goal state before:
pp: case H.inl
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝ : CommMonoid M
f : ι → M
ih :
  ∀ t ⊂ ∅,
    ∀ (g : (a : ι) → a ∈ t → ι),
      (∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1) →
        (∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) →
          ∀ (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t), (∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a) → ∏ x ∈ t, f x = 1
g : (a : ι) → a ∈ ∅ → ι
hg₁ : ∀ (a : ι) (ha : a ∈ ∅), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ ∅), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ ∅), g a ha ∈ ∅
hg₄ : ∀ (a : ι) (ha : a ∈ ∅), g (g a ha) ⋯ = a
⊢ ∏ x ∈ ∅, f x = 1

pp: case H.inr
ι : Type u_1
M : Type u_4
s✝ : Finset ι
inst✝ : CommMonoid M
f : ι → M
s : Finset ι
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : ι) → a ∈ t → ι),
      (∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1) →
        (∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) →
          ∀ (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t), (∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a) → ∏ x ∈ t, f x = 1
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
x : ι
hx : x ∈ s
⊢ ∏ x ∈ s, f x = 1

Tactic:
· simp

Goal state after:
case H.inr
ι : Type u_1
M : Type u_4
s✝ : Finset ι
inst✝ : CommMonoid M
f : ι → M
s : Finset ι
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : ι) → a ∈ t → ι),
      (∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1) →
        (∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) →
          ∀ (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t), (∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a) → ∏ x ∈ t, f x = 1
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
x : ι
hx : x ∈ s
⊢ ∏ x ∈ s, f x = 1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s).Pairwise fun i j ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : κ → Finset ι := fun k ↦ {i ∈ t k | f i ≠ 1}
this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}
i : κ
hi : i ∈ ↑s
j : κ
hj : j ∈ ↑s
hij : i ≠ j
a : Finset ι
hai : a ⊆ t' i
haj : a ⊆ t' j
k : ι
hk : k ∈ a
hki : k ∈ t i ∧ ¬f k = 1
hkj : k ∈ t j ∧ ¬f k = 1
⊢ k ∈ t i ∩ t j

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : κ → ι
g : ι → M
n : κ
I : Finset κ
hn : n ∈ I
hf : (↑I).Pairwise fun i j ↦ f i = f j → g (f i) = 1
h : ∀ j ∈ {i ∈ I | f i = f n}.erase n, g (f j) = 1
⊢ ∏ j ∈ I with f j = f n, g (f j) = g (f n)

Tactic:
← mul_one (g (f n)),

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : κ → ι
g : ι → M
n : κ
I : Finset κ
hn : n ∈ I
hf : (↑I).Pairwise fun i j ↦ f i = f j → g (f i) = 1
h : ∀ j ∈ {i ∈ I | f i = f n}.erase n, g (f j) = 1
⊢ ∏ j ∈ I with f j = f n, g (f j) = g (f n) * 1
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x ↦ f x >>= g
⊢ -pure x >>= f >>= g = -pure x >>= fun x ↦ f x >>= g

Tactic:
rw [neg_bind] <;> try rw [ih]

Goal state after:
α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x ↦ f x >>= g
⊢ -(pure x >>= f) >>= g = -pure x >>= fun x ↦ f x >>= g
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x ↦ f x >>= g
⊢ -(pure x >>= f) >>= g = -pure x >>= fun x ↦ f x >>= g

Tactic:
rw [neg_bind] <;> try rw [ih]

Goal state after:
α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x ↦ f x >>= g
⊢ -(pure x >>= fun x ↦ f x >>= g) = -pure x >>= fun x ↦ f x >>= g
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x ↦ f x >>= g
⊢ -(pure x >>= fun x ↦ f x >>= g) = -pure x >>= fun x ↦ f x >>= g

Tactic:
rw [neg_bind] <;> try rw [ih]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : DecidableEq M
s✝ : Finset ι
t : ι → Finset M
this : DecidableEq ι
a : ι
s : Finset ι
has : a ∉ s
ih : #(s.biUnion t) ≤ ∑ a ∈ s, #(t a)
⊢ #(t a) + #(s.biUnion t) ≤ ∑ a ∈ insert a s, #(t a)

Tactic:
by grind

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ map f (commutator G) = ⁅f.range, f.range⁆

Tactic:
by
  rw [_root_.commutator_def, Subgroup.map_commutator]
  apply congr_arg₂ <;>
  · rw [Subgroup.map_eq_range_iff]
    rw [codisjoint_iff, top_sup_eq]

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

Goal state before:
pp: case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommGroup α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedAddMonoid α
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
h : StrictMono ⇑f
a : α
⊢ 0 < a → 0 < f a

pp: case refine_2
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommGroup α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedAddMonoid α
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
h : ∀ (a : α), 0 < a → 0 < f a
a b : α
hl : a < b
⊢ f a < f b

Tactic:
· rw [← map_zero f]
    apply h

Goal state after:
case refine_2
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommGroup α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedAddMonoid α
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
h : ∀ (a : α), 0 < a → 0 < f a
a b : α
hl : a < b
⊢ f a < f b
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case refine_2
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f ↑a.2 = f a.1
b : M × ↥S
hb : w * f ↑b.2 = f b.1
⊢ w * f ↑(a.2 * b.2) = f (↑a.2 * b.1)

Tactic:
simp_rw [mul_def, map_mul, ← hb]

Goal state after:
case refine_2
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f ↑a.2 = f a.1
b : M × ↥S
hb : w * f ↑b.2 = f b.1
⊢ w * (f ↑a.2 * f ↑b.2) = f ↑a.2 * (w * f ↑b.2)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * ↑s ∈ S
x : X
s₂ : ↥S
⊢ smul' r₁ s x s₂ = smul' (r₂ * r₁) ⟨r₂ * ↑s, hs⟩ x s₂

Tactic:
rcases oreCondition r₁ s₂ with ⟨r₁', s₁', h₁⟩

Goal state after:
case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * ↑s ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r₁ = r₁' * ↑s₂
⊢ smul' r₁ s x s₂ = smul' (r₂ * r₁) ⟨r₂ * ↑s, hs⟩ x 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
x₁ x₂ : M
y₁ y₂ : ↥S
H : f (↑y₂ * x₁) = f (↑y₁ * x₂)
⊢ f x₁ = f x₂ * (↑((IsUnit.liftRight (f.toMonoidHom.domRestrict S) ⋯) y₂)⁻¹ * f ↑y₁)

Tactic:
mul_comm _ (f y₁),

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x₁ x₂ : M
y₁ y₂ : ↥S
H : f (↑y₂ * x₁) = f (↑y₁ * x₂)
⊢ f x₁ = f x₂ * (f ↑y₁ * ↑((IsUnit.liftRight (f.toMonoidHom.domRestrict S) ⋯) y₂)⁻¹)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case mk.mk
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
inst✝ : IsMulTorsionFree M
n : ℕ
hn : n ≠ 0
a₁✝ : Localization S
a : M × ↥S
a₂✝ : Localization S
b : M × ↥S
hab : ∃ a_1 ∈ S, a_1 * (↑b.2 ^ n * a.1 ^ n) = a_1 * (↑a.2 ^ n * b.1 ^ n)
⊢ ∃ a_1 ∈ S, a_1 * (↑b.2 * a.1) = a_1 * (↑a.2 * b.1)

Tactic:
obtain ⟨c, hc, hab⟩ := hab

Goal state after:
case mk.mk
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
inst✝ : IsMulTorsionFree M
n : ℕ
hn : n ≠ 0
a₁✝ : Localization S
a : M × ↥S
a₂✝ : Localization S
b : M × ↥S
c : M
hc : c ∈ S
hab : c * (↑b.2 ^ n * a.1 ^ n) = c * (↑a.2 ^ n * b.1 ^ n)
⊢ ∃ a_1 ∈ S, a_1 * (↑b.2 * a.1) = a_1 * (↑a.2 * b.1)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case mk.mk.zero
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
inst✝ : IsMulTorsionFree M
a₁✝ : Localization S
a : M × ↥S
a₂✝ : Localization S
b : M × ↥S
c : M
hc : c ∈ S
hn : 0 ≠ 0
hab : c * (↑b.2 ^ 0 * a.1 ^ 0) = c * (↑a.2 ^ 0 * b.1 ^ 0)
⊢ (fun a ↦ a ^ 0) (c * (↑b.2 * a.1)) = (fun a ↦ a ^ 0) (c * (↑a.2 * b.1))

pp: case mk.mk.succ
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
inst✝ : IsMulTorsionFree M
a₁✝ : Localization S
a : M × ↥S
a₂✝ : Localization S
b : M × ↥S
c : M
hc : c ∈ S
n : ℕ
hn : n + 1 ≠ 0
hab : c * (↑b.2 ^ (n + 1) * a.1 ^ (n + 1)) = c * (↑a.2 ^ (n + 1) * b.1 ^ (n + 1))
⊢ (fun a ↦ a ^ (n + 1)) (c * (↑b.2 * a.1)) = (fun a ↦ a ^ (n + 1)) (c * (↑a.2 * b.1))

Tactic:
· simp

Goal state after:
case mk.mk.succ
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
inst✝ : IsMulTorsionFree M
a₁✝ : Localization S
a : M × ↥S
a₂✝ : Localization S
b : M × ↥S
c : M
hc : c ∈ S
n : ℕ
hn : n + 1 ≠ 0
hab : c * (↑b.2 ^ (n + 1) * a.1 ^ (n + 1)) = c * (↑a.2 ^ (n + 1) * b.1 ^ (n + 1))
⊢ (fun a ↦ a ^ (n + 1)) (c * (↑b.2 * a.1)) = (fun a ↦ a ^ (n + 1)) (c * (↑a.2 * b.1))
Module: Mathlib.Algebra.Order.Sub.WithTop

Goal state before:
pp: case coe.top
α : Type u_1
β : Type u_2
inst✝⁴ : Add α
inst✝³ : LE α
inst✝² : OrderBot α
inst✝¹ : Sub α
inst✝ : OrderedSub α
z : WithTop α
a✝ : α
⊢ ⊤ - ↑a✝ ≤ z ↔ ⊤ ≤ z + ↑a✝

pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝⁴ : Add α
inst✝³ : LE α
inst✝² : OrderBot α
inst✝¹ : Sub α
inst✝ : OrderedSub α
z : WithTop α
a✝¹ a✝ : α
⊢ ↑a✝ - ↑a✝¹ ≤ z ↔ ↑a✝ ≤ z + ↑a✝¹

Tactic:
· simp

Goal state after:
case coe.coe
α : Type u_1
β : Type u_2
inst✝⁴ : Add α
inst✝³ : LE α
inst✝² : OrderBot α
inst✝¹ : Sub α
inst✝ : OrderedSub α
z : WithTop α
a✝¹ a✝ : α
⊢ ↑a✝ - ↑a✝¹ ≤ z ↔ ↑a✝ ≤ z + ↑a✝¹
Module: Mathlib.Algebra.Order.Sub.WithTop

Goal state before:
pp: case coe.coe.top
α : Type u_1
β : Type u_2
inst✝⁴ : Add α
inst✝³ : LE α
inst✝² : OrderBot α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝¹ a✝ : α
⊢ ↑a✝ - ↑a✝¹ ≤ ⊤ ↔ ↑a✝ ≤ ⊤ + ↑a✝¹

pp: case coe.coe.coe
α : Type u_1
β : Type u_2
inst✝⁴ : Add α
inst✝³ : LE α
inst✝² : OrderBot α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝² a✝¹ a✝ : α
⊢ ↑a✝¹ - ↑a✝² ≤ ↑a✝ ↔ ↑a✝¹ ≤ ↑a✝ + ↑a✝²

Tactic:
· simp

Goal state after:
case coe.coe.coe
α : Type u_1
β : Type u_2
inst✝⁴ : Add α
inst✝³ : LE α
inst✝² : OrderBot α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝² a✝¹ a✝ : α
⊢ ↑a✝¹ - ↑a✝² ≤ ↑a✝ ↔ ↑a✝¹ ≤ ↑a✝ + ↑a✝²
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inl
α : Type u_1
inst✝⁶ : DecidableEq α
R : Type u_2
S : Type u_3
inst✝⁵ : MulZeroOneClass R
inst✝⁴ : DecidableEq R
inst✝³ : Nontrivial R
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : R →*₀ S
hf : Function.Injective ⇑f
y : WithTop R
this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0
⊢ map (⇑f) (0 * y) = map (⇑f) 0 * map (⇑f) y

pp: case inr
α : Type u_1
inst✝⁶ : DecidableEq α
R : Type u_2
S : Type u_3
inst✝⁵ : MulZeroOneClass R
inst✝⁴ : DecidableEq R
inst✝³ : Nontrivial R
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : R →*₀ S
hf : Function.Injective ⇑f
x y : WithTop R
this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0
hx : x ≠ 0
⊢ map (⇑f) (x * y) = map (⇑f) x * map (⇑f) y

Tactic:
· simp

Goal state after:
case inr
α : Type u_1
inst✝⁶ : DecidableEq α
R : Type u_2
S : Type u_3
inst✝⁵ : MulZeroOneClass R
inst✝⁴ : DecidableEq R
inst✝³ : Nontrivial R
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : R →*₀ S
hf : Function.Injective ⇑f
x y : WithTop R
this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0
hx : x ≠ 0
⊢ map (⇑f) (x * y) = map (⇑f) x * map (⇑f) y
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝⁶ : DecidableEq α
R : Type u_2
S : Type u_3
inst✝⁵ : MulZeroOneClass R
inst✝⁴ : DecidableEq R
inst✝³ : Nontrivial R
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : R →*₀ S
hf : Function.Injective ⇑f
x : WithTop R
this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0
hx : x ≠ 0
⊢ map (⇑f) (x * 0) = map (⇑f) x * map (⇑f) 0

pp: case inr.inr
α : Type u_1
inst✝⁶ : DecidableEq α
R : Type u_2
S : Type u_3
inst✝⁵ : MulZeroOneClass R
inst✝⁴ : DecidableEq R
inst✝³ : Nontrivial R
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : R →*₀ S
hf : Function.Injective ⇑f
x y : WithTop R
this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0
hx : x ≠ 0
hy : y ≠ 0
⊢ map (⇑f) (x * y) = map (⇑f) x * map (⇑f) y

Tactic:
· simp

Goal state after:
case inr.inr
α : Type u_1
inst✝⁶ : DecidableEq α
R : Type u_2
S : Type u_3
inst✝⁵ : MulZeroOneClass R
inst✝⁴ : DecidableEq R
inst✝³ : Nontrivial R
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : R →*₀ S
hf : Function.Injective ⇑f
x y : WithTop R
this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0
hx : x ≠ 0
hy : y ≠ 0
⊢ map (⇑f) (x * y) = map (⇑f) x * map (⇑f) y
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
eq : (fun x ↦ f m * x) n₁ = (fun x ↦ f m * x) n₂
ms₁ : M × ↥S
eq₁ : n₁ * f ↑ms₁.2 = f ms₁.1
ms₂ : M × ↥S
eq₂ : n₂ * f ↑ms₂.2 = f ms₂.1
⊢ n₁ * f (↑ms₁.2 * ↑ms₂.2) = n₂ * f (↑ms₁.2 * ↑ms₂.2)

Tactic:
replace eq := congr($eq * f (ms₁.2 * ms₂.2))

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
ms₁ : M × ↥S
eq₁ : n₁ * f ↑ms₁.2 = f ms₁.1
ms₂ : M × ↥S
eq₂ : n₂ * f ↑ms₂.2 = f ms₂.1
eq : (fun x ↦ f m * x) n₁ * f (↑ms₁.2 * ↑ms₂.2) = (fun x ↦ f m * x) n₂ * f (↑ms₁.2 * ↑ms₂.2)
⊢ n₁ * f (↑ms₁.2 * ↑ms₂.2) = n₂ * f (↑ms₁.2 * ↑ms₂.2)
Module: Mathlib.Order.Iterate

Goal state before:
pp: case succ.succ
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn :
  0 < n + 1 →
    (∀ (k : ℕ), k < n + 1 → x (k + 1) < f (x k)) → (∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)) → x (n + 1) < y (n + 1)
hn : 0 < n + 1 + 1
hx : ∀ (k : ℕ), k < n + 1 + 1 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n + 1 + 1 → f (y k) ≤ y (k + 1)
⊢ x (n + 1) ≤ y (n + 1)

Tactic:
| succ n =>

Goal state after: