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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
u : Set β
hu : u.Finite
hsu : u ⊆ f '' s
this : Finite ↑u
⊢ ∃ t ⊆ s, ∃ (_ : t.Finite), f '' t = u

Tactic:
choose g hg hg' using hsu

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set α
u : Set β
hu : u.Finite
this : Finite ↑u
g : ⦃a : β⦄ → a ∈ u → α
hg : ∀ ⦃a : β⦄ (a_1 : a ∈ u), g a_1 ∈ s
hg' : ∀ ⦃a : β⦄ (a_1 : a ∈ u), f (g a_1) = a
⊢ ∃ t ⊆ s, ∃ (_ : t.Finite), f '' t = u
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case cons.inl
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s✝ : Finset ι
H : s✝.Nonempty
f : ι → α
c : ι
s : Finset ι
hcs : c ∉ s
hs : s.Nonempty
b : ι
hb : b ∈ s
h' : s.sup' hs f = f b
h : f b ≤ f c
⊢ ∃ i ∈ cons c s hcs, max (f c) (f b) = f i

Tactic:
| inl h =>

Goal state after:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
inst✝¹ : LinearOrder ι'
inst✝ : Nonempty ι'
α : ι → Type u_3
I : Set ι
s : (i : ι) → ι' → Set (α i)
hI : I.Finite
hs : ∀ i ∈ I, Monotone (s i)
this : Finite ↑I
i : ↑I
j₁ j₂ : ι'
h : j₁ ≤ j₂
⊢ eval ↑i ⁻¹' s (↑i) j₁ ⊆ eval ↑i ⁻¹' s (↑i) j₂

Tactic:
exact preimage_mono <| hs i i.2 h

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
p q : Prop
f : p ∨ q → α
⊢ ⨆ (h : p ∨ q), f h = max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯)

Tactic:
by_cases hp : p <;>
  by_cases hq : q <;>
  simp [hp, hq]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case refine_2.inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ : α
b₁ b₂ : β
h : b₁ ⩿ b₂
⊢ (a₁, b₁) ⩿ (a₁, b₂)

Tactic:
· exact mk_wcovBy_mk_iff_right.2 h

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

Goal state before:
pp: case inl
s : Set ℕ
h : s = ∅
⊢ sInf s = 0 ↔ 0 ∈ s ∨ s = ∅

Tactic:
| inl h =>

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

Goal state before:
pp: case inl
s : Set ℕ
m : ℕ
hm : m < sInf s
h : s = ∅
⊢ m ∉ s

Tactic:
| inl h =>

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

Goal state before:
pp: case zero
a k l : ℕ
hkl : k = l % a
hk : k < a
hl : l < a
⊢ k = l

Tactic:
mod_eq_of_lt hl

Goal state after:
case zero
a k l : ℕ
hkl : k = l
hk : k < a
hl : l < a
⊢ k = l
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ x ∈ (Ioo (f a) (f b)).preimage ⇑f ⋯ ↔ a < x ∧ x < b

Tactic:
rw [mem_preimage, mem_Ioo, f.lt_iff_lt, f.lt_iff_lt]

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : WellFoundedGT α
a : ℕ →o α
m : ℕ
hm : monotonicSequenceLimitIndex a < m
⊢ a m ≤ monotonicSequenceLimit a

Tactic:
obtain h := WellFoundedGT.monotone_chain_condition a
    exact (Nat.sInf_mem (s := {n | ∀ m, n ≤ m → a n = a m}) h m hm.le).ge

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
⊢ ∃ a, IsMin (a 0) ∧ ∃ n, IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)

Tactic:
have hα := Set.nonempty_iff_univ_nonempty.mp ‹_›

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, IsMin (a 0) ∧ ∃ n, IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun x1 x2 ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ s
ht : ∀ (f : (fun x1 x2 ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ t
⊢ ∀ (f : (fun x1 x2 ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ s ∪ t

Tactic:
rintro f hf

Goal state after:
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun x1 x2 ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ s
ht : ∀ (f : (fun x1 x2 ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ t
f : (fun x1 x2 ↦ x1 > x2) ↪r r
hf : ∀ (n : ℕ), f n ∈ s ∪ t
⊢ False
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: case mul
M : Type u_3
inst✝³ : Monoid M
N : Type u_7
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x✝ x y : N
hx✝ : x ∈ closure s
hy✝ : y ∈ closure s
hx : ∃ n, r ^ n • x ∈ closure (r • s)
hy : ∃ n, r ^ n • y ∈ closure (r • s)
⊢ ∃ n, r ^ n • (x * y) ∈ closure (r • s)

Tactic:
obtain ⟨⟨nx, hx⟩, ⟨ny, hy⟩⟩ := And.intro hx hy
    use ny + nx
    rw [pow_add, mul_smul, ← smul_mul_assoc, mul_comm, ← smul_mul_assoc]
    exact mul_mem hy hx

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
hs : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
this : BddAbove (f ⁻¹' s)
⊢ ∃ k, ∀ (m : ℕ), k < m → f m ∉ s

Tactic:
contrapose! this

Goal state after:
α : Type u_2
r : α → α → Prop
s : Set α
hs : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
this : ∀ (k : ℕ), ∃ m, k < m ∧ f m ∈ s
⊢ ¬BddAbove (f ⁻¹' s)
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MulAction G β
inst✝¹ : SMul α β
inst✝ : IsScalarTower G α β
a : α
b : β
⊢ stabilizer G a ≤ stabilizer G (a • b)

Tactic:
by
  simp_rw [SetLike.le_def, mem_stabilizer_iff, ← smul_assoc]; rintro a h; rw [h]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_2
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t ↦
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn ↦ ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m
n : ℕ
g : ℕ → α
hg1 : ∀ m < n, (fun n ↦ ↑(fs n) n) m = g m
hg2 : rk (g n) < rk ((fun n ↦ ↑(fs n) n) n)
⊢ ¬IsBadSeq r s g

Tactic:
· refine (fs n).2.2 g (fun m mn => ?_) hg2
    rw [← h m n mn.le, ← hg1 m mn]

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

Goal state before:
pp: case refine_1
G : Type u_2
inst✝ : Group G
g : G
hg : g ∈ ↑(Subgroup.center G)
⊢ ConjClasses.mk g ∈ (noncenter G)ᶜ

pp: case refine_2
G : Type u_2
inst✝ : Group G
x : G
hx : x ∈ ↑(Subgroup.center G)
y : G
x✝ : y ∈ ↑(Subgroup.center G)
H : ConjClasses.mk x = ConjClasses.mk y
⊢ x = y

pp: case refine_3
G : Type u_2
inst✝ : Group G
⊢ Set.SurjOn ConjClasses.mk (↑(Subgroup.center G)) (noncenter G)ᶜ

Tactic:
· simp only [mem_noncenter, Set.compl_def, Set.mem_ofPred, Set.not_nontrivial_iff]
    intro x hx y hy
    simp only [mem_carrier_iff_mk_eq, mk_eq_mk_iff_isConj] at hx hy
    rw [hx.eq_of_right_mem_center hg, hy.eq_of_right_mem_center hg]

Goal state after:
case refine_2
G : Type u_2
inst✝ : Group G
x : G
hx : x ∈ ↑(Subgroup.center G)
y : G
x✝ : y ∈ ↑(Subgroup.center G)
H : ConjClasses.mk x = ConjClasses.mk y
⊢ x = y

case refine_3
G : Type u_2
inst✝ : Group G
⊢ Set.SurjOn ConjClasses.mk (↑(Subgroup.center G)) (noncenter G)ᶜ
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
z₁ z₂ : M
hz₁ : z₁ ∈ center M
hz₂ : z₂ ∈ center M
⊢ z₁ * z₂ ∈ center M

Tactic:
simp only [commute_iff_eq, mem_center_iff, isMulCentral_iff] at *
  grind

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : Mˣ
ha : ↑a ∈ center M
⊢ ↑a⁻¹ ∈ center M

Tactic:
by
  rw [Semigroup.mem_center_iff] at *
  exact (Commute.units_inv_right <| ha ·)

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

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝ : Group G
H : Subgroup G
hH : H.Normal
K : Subgroup ↥H
h : K.Characteristic
a : G
ha : a ∈ map H.subtype K
b : G
⊢ b * a * b⁻¹ ∈ map H.subtype K

Tactic:
by
    obtain ⟨a, ha, rfl⟩ := ha
    exact K.apply_coe_mem_map H.subtype
      ⟨_, (SetLike.ext_iff.mp (h.fixed (MulAut.conjNormal b)) a).mpr ha⟩

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H K : Subgroup G
⊢ normalizer ↑H ⊓ normalizer ↑K ≤ normalizer ↑(H ⊔ K)

Tactic:
intro g

Goal state after:
G : Type u_2
inst✝ : Group G
H K : Subgroup G
g : G
⊢ g ∈ normalizer ↑H ⊓ normalizer ↑K → g ∈ normalizer ↑(H ⊔ K)
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
ι : Sort u_5
H : ι → Subgroup G
⊢ ⨅ i, normalizer ↑(H i) ≤ normalizer ↑(⨆ i, H i)

Tactic:
intro g

Goal state after:
G : Type u_2
inst✝ : Group G
ι : Sort u_5
H : ι → Subgroup G
g : G
⊢ g ∈ ⨅ i, normalizer ↑(H i) → g ∈ normalizer ↑(⨆ i, H i)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

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

Tactic:
by
  simp [toMul, 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 (Additive M)
⊢ toMul s.sum = (Multiset.map (⇑toMul) s).prod

Tactic:
by
  simp [toMul, ofMul]; rfl

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 κ
f : ι → M
g : κ → M
e : ι → κ
he : Set.InjOn e ↑s
hest : Set.MapsTo e ↑s ↑t
h' : ∀ i ∈ t, i ∉ e '' ↑s → g i = 1
h : ∀ i ∈ s, f i = g (e i)
⊢ ∏ i ∈ s, f i = ∏ j ∈ t, g j

Tactic:
by
  classical
  exact (prod_nbij e (fun a ↦ mem_image_of_mem e) he (by simp [Set.surjOn_image]) h).trans <|
    prod_subset (image_subset_iff.2 hest) <| by simpa using h'

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ ∀ ⦃a b : List (α × Bool)⦄, Red.Step a b → Red.Step (invRev a) (invRev b)

Tactic:
intro a b h
        cases h
        simp [invRev]

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ ∀ (a : FreeGroup α), 1 * a = a

Tactic:
rintro ⟨L⟩

Goal state after:
case mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
a✝ : FreeGroup α
L : List (α × Bool)
⊢ 1 * Quot.mk Red.Step L = Quot.mk Red.Step L
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ ∀ (a : FreeGroup α), a * 1 = a

Tactic:
rintro ⟨L⟩

Goal state after:
case mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
a✝ : FreeGroup α
L : List (α × Bool)
⊢ Quot.mk Red.Step L * 1 = Quot.mk Red.Step L
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ ∀ (a : FreeGroup α), a⁻¹ * a = 1

Tactic:
rintro ⟨L⟩

Goal state after:
case mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
a✝ : FreeGroup α
L : List (α × Bool)
⊢ (Quot.mk Red.Step L)⁻¹ * Quot.mk Red.Step L = 1
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u_1
⊢ Subgroup.closure (Set.range of) = ⊤

Tactic:
← range_lift_eq_closure,

Goal state after:
α : Type u_1
⊢ (lift of).range = ⊤
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : FreeGroup α →* FreeGroup β
hg : ∀ (x : α), g (FreeGroup.of x) = FreeGroup.of (f x)
⊢ ∀ {x : FreeGroup α}, g x = (map f) x

Tactic:
rintro ⟨L⟩

Goal state after:
case mk
α : Type u
β : Type v
f : α → β
g : FreeGroup α →* FreeGroup β
hg : ∀ (x : α), g (FreeGroup.of x) = FreeGroup.of (f x)
x✝ : FreeGroup α
L : List (α × Bool)
⊢ g (Quot.mk Red.Step L) = (map f) (Quot.mk Red.Step L)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
hf : Function.Injective f
⊢ Function.Injective ⇑(map f)

Tactic:
by_cases! h : IsEmpty α
  · exact Function.injective_of_subsingleton _
  · rw [Function.injective_iff_hasLeftInverse]
    use map (Function.invFun f)
    simp [Function.LeftInverse, map.comp, Function.invFun_comp hf]

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ Function.LeftInverse (fun x ↦ of () ^ x) fun x ↦ ((map fun x ↦ 1) x).sum

Tactic:
rintro ⟨L⟩

Goal state after:
case mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
x✝ : FreeGroup Unit
L : List (Unit × Bool)
⊢ (fun x ↦ of () ^ x) ((fun x ↦ ((map fun x ↦ 1) x).sum) (Quot.mk Red.Step L)) = Quot.mk Red.Step L
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
⊢ Nontrivial (G ⧸ N) ↔ N ≠ ⊤

Tactic:
simp [← not_subsingleton_iff_nontrivial]

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
inst✝ : Finite G
⊢ FG G

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

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
s : Finset G
⊢ Subgroup.closure (Subtype.val ⁻¹' ↑s) = ⊤

Tactic:
← Subgroup.coe_subtype,

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
s : Finset G
⊢ Subgroup.closure (⇑(Subgroup.closure ↑s).subtype ⁻¹' ↑s) = ⊤
Module: Mathlib.GroupTheory.Abelianization.Defs

Goal state before:
pp: G : Type u
inst✝¹ : Group G
A : Type v
inst✝ : CommGroup A
f : G →* A
p q : G
⊢ ⁅p, q⁆ ∈ ↑f.ker

Tactic:
simp [MonoidHom.mem_ker, mul_right_comm (f p) (f q), commutatorElement_def]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

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

Tactic:
simp only [(lift _).map_zero, zero_add]

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

Goal state before:
pp: case H
M : Type u_1
G : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommGroup G
y✝ : M × ↥⊤
⊢ (monoidOf ⊤).mk' (↑y✝.2 * y✝.1) (⟨y✝.1, ⋯⟩ * y✝.2) = 1

Tactic:
convert! Submonoid.LocalizationMap.mk'_self' _ _

Goal state after:
case e'_2.e'_7
M : Type u_1
G : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommGroup G
y✝ : M × ↥⊤
⊢ ↑y✝.2 * y✝.1 = ↑(⟨y✝.1, ⋯⟩ * y✝.2)
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 y : M
x✝ : ∃ c, ↑c * x = ↑c * y
c : ↥S
h : f (↑c * x) = f (↑c * y)
⊢ f x = f y

Tactic:
rw [map_mul, map_mul] at h

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 y : M
x✝ : ∃ c, ↑c * x = ↑c * y
c : ↥S
h : f ↑c * f x = f ↑c * f y
⊢ f x = f y
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 y : M
c : ↥S
h : f (↑c * x) = f (↑c * y)
⊢ f x = f y

Tactic:
rw [map_mul, map_mul] at h

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 y : M
c : ↥S
h : f ↑c * f x = f ↑c * f y
⊢ f x = f y
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
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
x : OreLocalization S R
r t : R
s : ↥S
ht : t * ↑s ∈ S
⊢ ↑(fS s)⁻¹ * f r = ↑(fS ⟨t * ↑s, ht⟩)⁻¹ * f (t • r)

Tactic:
by
      simp only [smul_eq_mul]
      have : (fS ⟨t * s, ht⟩ : T) = f t * fS s := by
        simp only [← hf, map_mul]
      conv_rhs =>
        rw [map_mul, ← one_mul (f r), ← Units.val_one, ← mul_inv_cancel (fS s)]
        rw [Units.val_mul, mul_assoc, ← mul_assoc _ (fS s : T), ← this, ← mul_assoc]
      simp only [one_mul, Units.inv_mul]

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

Goal state before:
pp: case inl
S : AddSubmonoid ℕ
hS : S ≠ ⊥
z : ℕ
⊢ ∃ x, ∃ y ∈ S, ↑z = ↑x - ↑y

pp: case inr
S : AddSubmonoid ℕ
hS : S ≠ ⊥
z : ℕ
⊢ ∃ x, ∃ y ∈ S, -↑z = ↑x - ↑y

Tactic:
· exact ⟨z, 0, zero_mem _, by lia⟩

Goal state after:
case inr
S : AddSubmonoid ℕ
hS : S ≠ ⊥
z : ℕ
⊢ ∃ x, ∃ y ∈ S, -↑z = ↑x - ↑y
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹⁷ : Monoid M
S : Submonoid M
inst✝¹⁶ : OreSet S
inst✝¹⁵ : MulAction M X
inst✝¹⁴ : SMul R X
inst✝¹³ : SMul R M
inst✝¹² : IsScalarTower R M M
inst✝¹¹ : IsScalarTower R M X
inst✝¹⁰ : SMul R' X
inst✝⁹ : SMul R' M
inst✝⁸ : IsScalarTower R' M M
inst✝⁷ : IsScalarTower R' M X
inst✝⁶ : SMul R R'
inst✝⁵ : IsScalarTower R R' M
inst✝⁴ : SMul Rᵐᵒᵖ M
inst✝³ : SMul Rᵐᵒᵖ X
inst✝² : IsScalarTower Rᵐᵒᵖ M M
inst✝¹ : IsScalarTower Rᵐᵒᵖ M X
inst✝ : IsCentralScalar R M
r : R
x : OreLocalization S X
⊢ (MulOpposite.op r • 1 /ₒ 1) • x = (r • 1 /ₒ 1) • x

Tactic:
op_smul_eq_smul

Goal state after:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹⁷ : Monoid M
S : Submonoid M
inst✝¹⁶ : OreSet S
inst✝¹⁵ : MulAction M X
inst✝¹⁴ : SMul R X
inst✝¹³ : SMul R M
inst✝¹² : IsScalarTower R M M
inst✝¹¹ : IsScalarTower R M X
inst✝¹⁰ : SMul R' X
inst✝⁹ : SMul R' M
inst✝⁸ : IsScalarTower R' M M
inst✝⁷ : IsScalarTower R' M X
inst✝⁶ : SMul R R'
inst✝⁵ : IsScalarTower R R' M
inst✝⁴ : SMul Rᵐᵒᵖ M
inst✝³ : SMul Rᵐᵒᵖ X
inst✝² : IsScalarTower Rᵐᵒᵖ M M
inst✝¹ : IsScalarTower Rᵐᵒᵖ M X
inst✝ : IsCentralScalar R M
r : R
x : OreLocalization S X
⊢ (r • 1 /ₒ 1) • x = (r • 1 /ₒ 1) • x
Module: Mathlib.Order.Iterate

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
f : α → α
β : Type u_2
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
⊢ (h ∘ g^[n]) x ≤ (f^[n] ∘ h) x

Tactic:
apply hf.seq_le_seq n

Goal state after:
case h₀
α : Type u_1
inst✝ : Preorder α
f : α → α
β : Type u_2
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
⊢ (h ∘ g^[0]) x ≤ (f^[0] ∘ h) x

case hx
α : Type u_1
inst✝ : Preorder α
f : α → α
β : Type u_2
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
⊢ ∀ (k : ℕ), k < n → (h ∘ g^[k + 1]) x ≤ f ((h ∘ g^[k]) x)

case hy
α : Type u_1
inst✝ : Preorder α
f : α → α
β : Type u_2
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
⊢ ∀ (k : ℕ), k < n → f ((f^[k] ∘ h) x) ≤ (f^[k + 1] ∘ h) x
Module: Mathlib.Order.Iterate

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ f^[n] x ≤ g^[n] x

Tactic:
apply hf.seq_le_seq n

Goal state after:
case h₀
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ f^[0] x ≤ g^[0] x

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)

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
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
  by_cases ha : a = 0; · rw [ha, zero_mul, ← coe_zero, unbotD_coe, zero_mul]
  by_cases hb : b = 0; · rw [hb, mul_zero, ← coe_zero, unbotD_coe, mul_zero]
  cases a; · rw [bot_mul hb, unbotD_bot, zero_mul]
  cases b; · rw [mul_bot ha, unbotD_bot, mul_zero]
  rw [← coe_mul, unbotD_coe, unbotD_coe, unbotD_coe]

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

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

Tactic:
by
  cases a
  · simp [bot_eq_zero]
  · rename_i a
    simp only [WithBot.succ_coe, WithBot.coe_ne_bot, iff_false, succ_eq_add_one]
    by_contra h
    simpa [h] using max_of_succ_le (a := a)

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

Goal state before:
pp: α : Type u_1
x : α
inst✝⁵ : LinearOrder α
inst✝⁴ : AddMonoidWithOne α
inst✝³ : SuccAddOrder α
inst✝² : IsBotZeroClass α
inst✝¹ : NeZero 1
inst✝ : NoMaxOrder α
⊢ x ≤ 2 ↔ x = 0 ∨ x = 1 ∨ x = 2

Tactic:
by
  rw [le_iff_lt_or_eq, lt_two_iff, le_one_iff, or_assoc]

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

Goal state before:
pp: case succ
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
n : ℕ
hb : succ^[n + 1] a ∈ s
hab : ¬IsMax a
⊢ f a < f (succ^[n + 1] a)

Tactic:
induction n with
  | zero => simpa using hf _ hab ha hb
  | succ n hn =>
    rw [Function.iterate_succ_apply'] at hb ⊢
    have : succ^[n + 1] a ∈ s := hs.1 ha hb ⟨le_succ_iterate .., le_succ _⟩
    by_cases hb' : IsMax (succ^[n + 1] a)
    · rw [succ_eq_iff_isMax.2 hb']
      exact hn this
    · exact (hn this).trans (hf _ hb' this hb)

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

Goal state before:
pp: m : ℕ
n : WithTop ℕ∞
h : ↑m < ↑⊤
⊢ ↑(m + 1) ≤ ↑⊤

Tactic:
exact WithTop.coe_le_coe.2 (OrderTop.le_top _)

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
f : (x : ι) → p x → M
g : (x : ι) → ¬p x → M
⊢ (∏ x ∈ s, if hx : p x then f x hx else g x hx) = (∏ x, f ↑x ⋯) * ∏ x, g ↑x ⋯

Tactic:
by
  simp [prod_apply_dite _ _ fun x => x]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Nonempty β
h : Countable (α × β)
⊢ Countable α

Tactic:
by
  contrapose! h
  infer_instance

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Nonempty α
h : Countable (α × β)
⊢ Countable β

Tactic:
by
  contrapose! h
  infer_instance

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

Goal state before:
pp: α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 1
⊢ scanl f b v = b ::ᵥ f b v.head ::ᵥ nil

Tactic:
rw [← cons_head_tail v]
  simp only [scanl_cons, scanl_nil, head_cons, singleton_tail]

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

Goal state before:
pp: case succ.succ.refine_2
α : Type u_1
β : Type u_6
f : β → α → β
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (n + 1)) (i : Fin (n + 1)),
    (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
b : β
v : Vector α (n + 1 + 1)
i : Fin (n + 1 + 1)
⊢ ∀ (i : Fin (n + 1)),
    (scanl f (f b v.head) v.tail).get i.succ =
      f ((b ::ᵥ scanl f (f b v.head) v.tail).get i.succ.castSucc) ((v.head ::ᵥ v.tail).get i.succ)

Tactic:
intro i'
      simp only [hn, Fin.castSucc_succ, get_cons_succ]

Goal state after:
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
ha : a ∈ s i
⊢ #({f ∈ piFinset s | f i = a}) = ∏ j, #(Function.update s i {a} j)

Tactic:
by
      rw [← piFinset_update_singleton_eq_filter_piFinset_eq _ _ ha, Fintype.card_piFinset]

Goal state after:
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : Set α
t : Set β
hs : s.Countable
ht : t.Countable
f : α → β → γ
⊢ (Set.image2 f s t).Countable

Tactic:
by
  rw [← image_prod]
  exact (hs.prod ht).image _

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
p : Prop
f : p → Part α
h : p
⊢ assert p f = f h

Tactic:
by
  ext
  simp_all

Goal state after: