mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Commute.Hom

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : Mul M
inst✝² : Mul N
a x y : M
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
h : SemiconjBy a x y
f : F
⊢ SemiconjBy (f a) (f x) (f y)

Tactic:
by simpa only [SemiconjBy, map_mul] using congr_arg f h

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

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

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

Tactic:
rintro ⟨y, hy, z, ⟨hzB, hzC⟩, rfl⟩

Goal state after:
case mp
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
y : G
hy : y ∈ ↑A
z : G
hzB : z ∈ ↑B
hzC : z ∈ ↑C
⊢ (∃ x ∈ ↑A, ∃ y_1 ∈ ↑B, x * y_1 = y * z) ∧ y * z ∈ ↑C
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
s : Set (Setoid α)
⊢ sSup s = EqvGen.setoid (sSup (@r α '' s))

Tactic:
by
  rw [sSup_eq_eqvGen, sSup_image]
  congr with (x y)
  simp only [iSup_apply, iSup_Prop_eq, exists_prop]

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

Goal state before:
pp: α : Type u
x✝⁵ x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
H : [] ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵ = [] ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴
⊢ [] ++ x✝⁵ = [] ++ x✝⁴ ∨ ∃ L₅, Step ([] ++ x✝⁵) L₅ ∧ Step ([] ++ x✝⁴) L₅

Tactic:
injections; subst_vars; simp

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

Goal state before:
pp: α : Type u
x✝⁵ : List (α × Bool)
x3 : α
b3 : Bool
x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
H : [] ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵ = [(x3, b3)] ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴
⊢ [] ++ x✝⁵ = [(x3, b3)] ++ x✝⁴ ∨ ∃ L₅, Step ([] ++ x✝⁵) L₅ ∧ Step ([(x3, b3)] ++ x✝⁴) L₅

Tactic:
injections; subst_vars; simp

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

Goal state before:
pp: α : Type u
x3 : α
b3 : Bool
x✝⁵ x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
H : [(x3, b3)] ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵ = [] ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴
⊢ [(x3, b3)] ++ x✝⁵ = [] ++ x✝⁴ ∨ ∃ L₅, Step ([(x3, b3)] ++ x✝⁵) L₅ ∧ Step ([] ++ x✝⁴) L₅

Tactic:
injections; subst_vars; simp

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
c : Con M
d : Con c.Quotient
x y : M
h : c x y
⊢ d ↑x ↑y

Tactic:
rw [c.eq.2 h]

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
d : Con c.Quotient
x y : M
h : c x y
⊢ d ↑y ↑y
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y✝ : M
f✝ : M →* P
f : c.Quotient →* P
x y : M
h : c x y
⊢ f ↑x = f ↑y

Tactic:
rw [c.eq.2 h]

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

Goal state before:
pp: α : Type u
a₁ : α
b₁ : Bool
a₂ : α
b₂ : Bool
L₁ : List (α × Bool)
hL₁ : ∀ (L₂ : List (α × Bool)), ¬Red.Step ((a₁, b₁) :: (a₂, b₂) :: L₁) L₂
⊢ IsReduced ((a₁, b₁) :: (a₂, b₂) :: L₁)

Tactic:
isReduced_cons_cons

Goal state after:
α : Type u
a₁ : α
b₁ : Bool
a₂ : α
b₂ : Bool
L₁ : List (α × Bool)
hL₁ : ∀ (L₂ : List (α × Bool)), ¬Red.Step ((a₁, b₁) :: (a₂, b₂) :: L₁) L₂
⊢ ((a₁, b₁).1 = (a₂, b₂).1 → (a₁, b₁).2 = (a₂, b₂).2) ∧ IsReduced ((a₂, b₂) :: L₁)
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g₁ g₂ : G
⊢ (MulAut.conj g₁) g₂ = ⁅g₁, g₂⁆ * g₂

Tactic:
simp [commutatorElement_def]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case zero
α : Type u
G : Type u_1
β α✝ β✝ : Type u
y : FreeAbelianGroup β✝
⊢ 0 = (fun b a ↦ (a, b)) <$> y <*> 0

Tactic:
seq_zero

Goal state after:
case zero
α : Type u
G : Type u_1
β α✝ β✝ : Type u
y : FreeAbelianGroup β✝
⊢ 0 = 0
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case h
ι : Type u_1
inst✝ : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
h₂ : ∑ x ∈ s.toFinset, k • (count x s / k) • {x} = ∑ x ∈ s.toFinset, count x s • {x}
⊢ s = k • ∑ a ∈ s.toFinset, (count a s / k) • {a}

Tactic:
rw [← Finset.sum_nsmul, h₂, toFinset_sum_count_nsmul_eq]

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

Goal state before:
pp: case a.left.h₁
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') H₁ ≤ H₁.prod K₁

Tactic:
simp [le_prod_iff, map_map, MonoidHom.fst_comp_inl, MonoidHom.snd_comp_inl,
            MonoidHom.fst_comp_inr, MonoidHom.snd_comp_inr]

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

Goal state before:
pp: case h₂
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') H₂ ≤ H₂.prod K₂

Tactic:
simp [le_prod_iff, map_map, MonoidHom.fst_comp_inl, MonoidHom.snd_comp_inl,
            MonoidHom.fst_comp_inr, MonoidHom.snd_comp_inr]

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

Goal state before:
pp: case a.right.h₁
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inr G G') K₁ ≤ H₁.prod K₁

Tactic:
simp [le_prod_iff, map_map, MonoidHom.fst_comp_inl, MonoidHom.snd_comp_inl,
            MonoidHom.fst_comp_inr, MonoidHom.snd_comp_inr]

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

Goal state before:
pp: case h₂
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inr G G') K₂ ≤ H₂.prod K₂

Tactic:
simp [le_prod_iff, map_map, MonoidHom.fst_comp_inl, MonoidHom.snd_comp_inl,
            MonoidHom.fst_comp_inr, MonoidHom.snd_comp_inr]

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

Goal state before:
pp: case h.left
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
v₀ : R := ⋯
u₀ : ↥S := ⋯
h₀ : ↑u₀ * r₁ = v₀ * ↑s₂
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u
this : r₃ * v * ↑s₂ = ↑s₃ * v₀ * ↑s₂
s₄ : ↥S
hs₄ : ↑s₄ * (r₃ * v) = ↑s₄ * (↑s₃ * v₀)
⊢ (↑s₄ * ↑s₃) • v₀ • r₂ = (↑s₄ * r₃) • v • r₂

Tactic:
rw [smul_smul, mul_assoc (c := v₀), ← hs₄]

Goal state after:
case h.left
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : ↑u₀ * r₁ = v₀ * ↑s₂
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u
this : r₃ * v * ↑s₂ = ↑s₃ * v₀ * ↑s₂
s₄ : ↥S
hs₄ : ↑s₄ * (r₃ * v) = ↑s₄ * (↑s₃ * v₀)
⊢ (↑s₄ * (r₃ * v)) • r₂ = (↑s₄ * r₃) • v • r₂
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: case mp
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)
⊢ Injective ⇑(f.lift hg) → ∀ (x y : M), f x = f y ↔ g x = g y

pp: case mpr
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), f x = f y ↔ g x = g y) → Injective ⇑(f.lift hg)

Tactic:
· intro H x y
    constructor
    · exact f.eq_of_eq hg
    · intro h
      rw [← f.lift_eq hg, ← f.lift_eq hg] at h
      exact H h

Goal state after:
case mpr
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), f x = f y ↔ g x = g y) → Injective ⇑(f.lift hg)
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: case mpr
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)
H : ∀ (x y : M), f x = f y ↔ g x = g y
z w : N
h : (f.lift hg) z = (f.lift hg) w
w✝¹ : M × ↥S
h✝¹ : z * f ↑w✝¹.2 = f w✝¹.1
w✝ : M × ↥S
h✝ : w * f ↑w✝.2 = f w✝.1
⊢ f.mk' (f.sec z).1 (f.sec z).2 = f.mk' (f.sec w).1 (f.sec w).2

Tactic:
exact (mul_inv f.map_units).2 ((H _ _).2 <| (mul_inv hg).1 h)

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

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

Tactic:
ha,

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

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

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

Tactic:
· rw [hb, mul_zero, ← coe_zero, untopD_coe, mul_zero]

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

Goal state before:
pp: case refine_1
M : Type u_1
G : Type u_2
F : Type u_3
inst✝³ : CommMonoid M
inst✝² : CommGroup G
S : Submonoid G
inst✝¹ : FunLike F G M
inst✝ : MulHomClass F G M
f : F
h : S.IsLocalizationMap ⇑f
g g' : G
eq : f g = f g'
⊢ g = g'

Tactic:
have ⟨c, eq⟩ := h.exists_of_eq eq

Goal state after:
case refine_1
M : Type u_1
G : Type u_2
F : Type u_3
inst✝³ : CommMonoid M
inst✝² : CommGroup G
S : Submonoid G
inst✝¹ : FunLike F G M
inst✝ : MulHomClass F G M
f : F
h : S.IsLocalizationMap ⇑f
g g' : G
eq✝ : f g = f g'
c : ↥S
eq : ↑c * g = ↑c * g'
⊢ g = g'
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.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)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
⊢ f ra * f r₂ = f (↑sa * r₁) * (↑(fS s₂)⁻¹ * f r₂)

Tactic:
ha,

Goal state after:
case c.c
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)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
⊢ f ra * f r₂ = f (ra * ↑s₂) * (↑(fS s₂)⁻¹ * f r₂)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.inr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
a b c : WithTop α
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
⊢ a * b * c = a * (b * c)

Tactic:
cases a with | top => simp [hb, hc] | coe a => ?_

Goal state after:
case inr.inr.inr.coe
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
b c : WithTop α
hb : b ≠ 0
hc : c ≠ 0
a : α
ha : ↑a ≠ 0
⊢ ↑a * b * c = ↑a * (b * c)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: 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

Tactic:
ha,

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

Goal state before:
pp: 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

pp: 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

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

Goal state after:
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.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a : α
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
⊢ ¬IsSuccPrelimit a ↔ a ∈ range succ

Tactic:
isSuccPrelimit_iff_succ_ne,

Goal state after:
α : Type u_1
a : α
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
⊢ (¬∀ (b : α), succ b ≠ a) ↔ a ∈ range succ
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → motive a
hb : ¬IsMax b
⊢ isSuccPrelimitRecOn (Order.succ b) succ isSuccPrelimit = succ b hb

Tactic:
have hb' := mt IsSuccPrelimit.isMax hb

Goal state after:
α : Type u_1
b : α
motive : α → Sort u_2
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccPrelimit : (a : α) → IsSuccPrelimit a → motive a
hb : ¬IsMax b
hb' : ¬IsSuccPrelimit (Order.succ b)
⊢ isSuccPrelimitRecOn (Order.succ b) succ isSuccPrelimit = succ b hb
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
j : ℕ
hi : Order.succ^[j] ⊥ ≠ ⊥
⊢ P (Order.succ^[j] ⊥)

Tactic:
have hj : 0 < j := by apply Nat.pos_of_ne_zero; contrapose hi; simp [hi]

Goal state after:
α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
j : ℕ
hi : Order.succ^[j] ⊥ ≠ ⊥
hj : 0 < j
⊢ P (Order.succ^[j] ⊥)
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : SuccOrder X
inst✝¹ : IsSuccArchimedean X
inst✝ : SuccOrder Y
f : X ≃o Y
a : Y
n : ℕ
⊢ succ^[n] a = f (succ^[n] (EquivLike.inv f a))

Tactic:
induction n generalizing a with
    | zero => simp
    | succ n IH => simp only [Function.iterate_succ', Function.comp_apply, IH, f.map_succ]

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

Goal state before:
pp: case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
i : α
n : ℕ
hn : ¬IsMax (succ^[n - 1] i) → pred^[n] (succ^[n] i) = i
hin : ¬IsMax (succ^[n] i)
h_not_max : ¬IsMax (succ^[n - 1] i)
⊢ (pred^[n] ∘ pred) ((succ ∘ succ^[n]) i) = i

Tactic:
simp only [Function.comp_apply]

Goal state after:
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
i : α
n : ℕ
hn : ¬IsMax (succ^[n - 1] i) → pred^[n] (succ^[n] i) = i
hin : ¬IsMax (succ^[n] i)
h_not_max : ¬IsMax (succ^[n - 1] i)
⊢ pred^[n] (pred (succ (succ^[n] i))) = i
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 : a < succ^[n + 1] a
⊢ f a < f (succ^[n + 1] a)

Tactic:
apply not_isMax_of_lt at hab

Goal state after:
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)
Module: Mathlib.Logic.Small.Basic

Goal state before:
pp: α : Type v
β : Type w
γ : Type v'
inst✝ : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ a, f a = g b
hβ : Nonempty β
b : β
a : α
ha : f a = g b
⊢ Function.invFun g (f a) = b

Tactic:
ha,

Goal state after:
α : Type v
β : Type w
γ : Type v'
inst✝ : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ a, f a = g b
hβ : Nonempty β
b : β
a : α
ha : f a = g b
⊢ Function.invFun g (g b) = b
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

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

Tactic:
by
  simp only [prod_ite_eq', if_pos h]

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ ↑univ.powerset = ↑univ

Tactic:
simp [-coe_eq_univ]

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

Goal state before:
pp: α : Type u
s : Set α
h : s.Countable
default : α
⊢ range (enumerateCountable h default) ⊆ insert default s

Tactic:
refine range_subset_iff.mpr (fun n ↦ ?_)

Goal state after:
α : Type u
s : Set α
h : s.Countable
default : α
n : ℕ
⊢ enumerateCountable h default n ∈ insert default s
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
s : Set α
a : α
⊢ (insert a s).Countable ↔ s.Countable

Tactic:
by
  simp only [insert_eq, countable_union, countable_singleton, true_and]

Goal state after:
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α ⊕ₗ β
⊢ a ≤ b ∧ ¬b ≤ a → a < b

Tactic:
rintro ⟨⟨hab⟩ | ⟨hab⟩ | ⟨a, b⟩, hba⟩
        · exact Lex.inl (hab.lt_of_not_ge fun h => hba <| Lex.inl h)
        · exact Lex.inr (hab.lt_of_not_ge fun h => hba <| Lex.inr h)
        · exact Lex.sep _ _

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Defs

Goal state before:
pp: case mk.mk
ι : Type u
α : Type v
f : ι → Type v
b : ι
⊢ (Quotient.out #(f b) → ULift α) ≃ Quotient.out #(f b → α)

Tactic:
refine (Equiv.arrowCongr outMkEquiv Equiv.ulift).trans ?_

Goal state after:
case mk.mk
ι : Type u
α : Type v
f : ι → Type v
b : ι
⊢ (f b → α) ≃ Quotient.out #(f b → α)
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inr.inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹⁰ : LE α✝
inst✝⁹ : LE β✝
inst✝⁸ : LE γ
inst✝⁷ : LE α₁
inst✝⁶ : LE α₂
inst✝⁵ : LE β₁
inst✝⁴ : LE β₂
inst✝³ : LE γ₁
inst✝² : LE γ₂
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a : β
b : α
⊢ (Equiv.refl (α ⊕ β)ᵒᵈ) (inr a) ≤ (Equiv.refl (α ⊕ β)ᵒᵈ) (inl b) ↔ inr a ≤ inl b

Tactic:
exact iff_of_false (@not_inr_le_inl (OrderDual α) (OrderDual β) _ _ _ _) not_inl_le_inr

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: case mp
α : Type u_1
o : Part α
⊢ o ≠ none → ∃ x, o = some x

Tactic:
rw [Ne, eq_none_iff', not_not]

Goal state after:
case mp
α : Type u_1
o : Part α
⊢ o.Dom → ∃ x, o = some x
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case inr
α : Type u_2
c : Chain (Part α)
a b : α
i : ℕ
ha : a ∈ c i
j : ℕ
hb : b ∈ c j
hji : j ≤ i
this : b ∈ c.toOrderHom i
⊢ b = a

Tactic:
apply mem_unique this ha

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case mp
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x
b : β
hb : b ∈ ωSup (c.map f)
⊢ ωSup (c.map g) b ≤ x

Tactic:
apply ωSup_le _ _ _

Goal state after:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x
b : β
hb : b ∈ ωSup (c.map f)
⊢ ∀ (i : ℕ), ((c.map g).map (Pi.evalOrderHom b)) i ≤ x
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case refine_1
α β : Type u
a b : Cardinal.{u}
⊢ lift.{v, u} a ≤ lift.{v, u} b ↔ a ≤ b

pp: case refine_2
α β : Type u
a : Cardinal.{u}
b : Cardinal.{max u v}
⊢ b < (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯).ltEmbedding a →
    b ∈ Set.range ⇑(OrderEmbedding.ofMapLEIff lift.{v, u} ⋯).ltEmbedding

Tactic:
· refine inductionOn₂ a b fun _ _ ↦ ?_
    rw [← lift_umax, lift_mk_le.{v, u, u}, le_def]

Goal state after:
case refine_2
α β : Type u
a : Cardinal.{u}
b : Cardinal.{max u v}
⊢ b < (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯).ltEmbedding a →
    b ∈ Set.range ⇑(OrderEmbedding.ofMapLEIff lift.{v, u} ⋯).ltEmbedding
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: case inr.isTrue
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this✝ : Surjective h
this : Injective h
a : α
h✝ : a ∈ s
⊢ R a (f a)

pp: case inr.isFalse
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this✝ : Surjective h
this : Injective h
a : α
h✝ : a ∉ s
⊢ R a (invFun g a)

Tactic:
· exact hp₁ a

Goal state after:
case inr.isFalse
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this✝ : Surjective h
this : Injective h
a : α
h✝ : a ∉ s
⊢ R a (invFun g a)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
n : ℕ
⊢ #α = ↑n ↔ ∃ h, Fintype.card α = n

Tactic:
mk_eq_nat_iff_finset

Goal state after:
α : Type u
n : ℕ
⊢ (∃ t, ↑t = univ ∧ t.card = n) ↔ ∃ h, Fintype.card α = n
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
S T : Set α
H : Disjoint S T
⊢ #↑(S ∪ T) = #↑S + #↑T

Tactic:
by
  classical
  exact Quot.sound ⟨Equiv.Set.union H⟩

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u_1
s : Set α
⊢ #↑s + #↑sᶜ = #α

Tactic:
exact mk_congr (Equiv.Set.sumCompl s)

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u_1
l : List α
h : ↑l.length < #α
⊢ ∃ z, z ∉ l

Tactic:
classical
  contrapose! h
  calc
    #α = #(Set.univ : Set α) := mk_univ.symm
    _ ≤ #l.toFinset := mk_le_mk_of_subset fun x _ => List.mem_toFinset.mpr (h x)
    _ = l.toFinset.card := Cardinal.mk_coe_finset
    _ ≤ l.length := Nat.cast_le.mpr (List.toFinset_card_le l)

Goal state after:
Module: Mathlib.Algebra.Algebra.Defs

Goal state before:
pp: R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
r : R
y : A
⊢ x * ((algebraMap R A) r * y) = x * y * (algebraMap R A) r

Tactic:
commutes,

Goal state after:
R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
r : R
y : A
⊢ x * (y * (algebraMap R A) r) = x * y * (algebraMap R A) r