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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f g : α ↪o β
h : Set.range ⇑f = Set.range ⇑g
ef : ↑Set.univ ≃o ↑(⇑f '' Set.univ) := StrictMonoOn.orderIso (⇑f) Set.univ ⋯
eg : ↑Set.univ ≃o ↑(⇑g '' Set.univ) := StrictMonoOn.orderIso (⇑g) Set.univ ⋯
⊢ ∀ {a b : ↑(⇑f '' Set.univ)}, (Equiv.setCongr ⋯) a ≤ (Equiv.setCongr ⋯) b ↔ a ≤ b

Tactic:
by rfl

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

Goal state before:
pp: a b : ℕ
⊢ ↑(max a b + 1 - min a b) = ↑((↑b - ↑a).natAbs + 1)

Tactic:
Int.ofNat_sub

Goal state after:
a b : ℕ
⊢ ↑(max a b + 1) - ↑(min a b) = ↑((↑b - ↑a).natAbs + 1)

a b : ℕ
⊢ min a b ≤ max a b + 1
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ k, ⨆ (_ : k < n + 1), u k = u 0 ⊔ ⨆ k, ⨆ (_ : k < n), u (k + 1)

Tactic:
rw [← sup_iSup_nat_succ]
  simp

Goal state after:
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 : α × β
⊢ x ∈ Icc a.1 b.1 ×ˢ Icc a.2 b.2 ↔ a ≤ x ∧ x ≤ b

Tactic:
rw [mem_product, mem_Icc, mem_Icc, and_and_and_comm, le_def, le_def]

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
x y : α
h : x ≤ y
S : Set α := Set.Icc x y
hS : BoundedOrder ↑S := { top := ⟨y, ⋯⟩, le_top := ⋯, bot := ⟨x, ⋯⟩, bot_le := ⋯ }
a : ℕ → ↑S
n : ℕ
e : ∀ i < n, a i ⋖ a (i + 1)
h₁ : ↑(a 0) = ↑⊥
h₂ : ↑(a n) = ↑⊤
⊢ ∃ a, a 0 = x ∧ ∃ n, a n = y ∧ ∀ i < n, a i ⋖ a (i + 1)

Tactic:
exact ⟨Subtype.val ∘ a, h₁, n, h₂, fun i hi ↦ ⟨(e i hi).1, fun c hc h ↦ (e i hi).2
    (c := ⟨c, (a i).2.1.trans hc.le, h.le.trans (a _).2.2⟩) hc h⟩⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : DecidableLE α
inst✝ : LocallyFiniteOrder α
a : { x // x ≤ y }
⊢ y ≤ y

Tactic:
by rfl

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ Icc a (a ⊔ b) = Icc a b

Tactic:
sup_eq_right.2 h

Goal state after:
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ Icc a b = Icc a b
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Subgroup G
⊢ ↑s = ↑⊥ ↔ ↑s = 1

Tactic:
by rfl

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

Goal state before:
pp: case mem
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
x x✝ : G
hx : x✝ ∈ ↑H * ↑N
⊢ x✝ ∈ ↑H * ↑N

Tactic:
exact hx

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

Goal state before:
pp: α : Type u
L₁ L₂ L₃ x✝ b✝ c b : List (α × Bool)
hab hac : Step x✝ b
⊢ ReflGen Step b b

Tactic:
by rfl

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

Goal state before:
pp: α : Type u
L₁ L₂ L₃ x✝ b✝ c b : List (α × Bool)
hab hac : Step x✝ b
⊢ ReflTransGen Step b b

Tactic:
by rfl

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

Goal state before:
pp: α : Type u
L L₁₂ L₁ L₂ : List (α × Bool)
eq : L₁ ++ L₂ = L
⊢ Red L₁ L₁

Tactic:
by rfl

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

Goal state before:
pp: α : Type u
L L₁₂ L₁ L₂ : List (α × Bool)
eq : L₁ ++ L₂ = L
⊢ Red L₂ L₂

Tactic:
by 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 κ
inst✝ : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : κ → M
y : κ
x✝ : y ∈ t
x : ι
hx : x ∈ {i ∈ s | g i = y}
⊢ f y = f (g x)

Tactic:
by rw [(mem_filter.1 hx).2]

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

Goal state before:
pp: α : Type u
x✝ b✝ c b : List (α × Bool)
hab hac : Red.Step x✝ b
⊢ ReflGen Red.Step b b

Tactic:
by rfl

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

Goal state before:
pp: α : Type u
x✝ b✝ c b : List (α × Bool)
hab hac : Red.Step x✝ b
⊢ ReflTransGen Red.Step b b

Tactic:
by rfl

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
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M
⊢ (∏ a ∈ s with p a, if p a then f a else 1) = ∏ a ∈ s, if p a then f a else 1

Tactic:
by
      { refine prod_subset (filter_subset _ s) fun x hs h => ?_
        rw [mem_filter, not_and] at h
        exact if_neg (by simpa using h hs) }

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:
by rintro ⟨L⟩; rfl

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

Goal state before:
pp: ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst✝ : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
| ∏ a ∈ s₂, g a

Tactic:
rw [← sdiff_union_inter s₂ s₁, prod_union_eq_right (by simp_all), inter_comm]

Goal state after:
ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst✝ : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
| ∏ a ∈ s₁ ∩ s₂, g a
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
f : ℕ → M
⊢ ∏ k ∈ range 1, f k = f 0

Tactic:
by
  rw [range_one, prod_singleton]

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
val✝ : Fintype G
⊢ Subgroup.closure ↑Finset.univ = ⊤

Tactic:
rw [Finset.coe_univ]; exact Subgroup.closure_univ

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
⊢ f n = f n

Tactic:
by rfl

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
⊢ (∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅g₁, g₂⁆ ∈ ⊥) ↔ H₁ ≤ centralizer ↑H₂

Tactic:
refine forall_congr' fun p =>
    forall_congr' fun _hp => forall_congr' fun q => forall_congr' fun hq => ?_

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
p : G
_hp : p ∈ H₁
q : G
hq : q ∈ H₂
⊢ ⁅p, q⁆ ∈ ⊥ ↔ q * p = p * q
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : IsMulCommutative ↥H
⊢ IsMulCommutative (G ⧸ N)

Tactic:
let φ : H →ₙ* G ⧸ N := MonoidHom.comp (QuotientGroup.mk' N) (Subgroup.subtype H)

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : IsMulCommutative ↥H
φ : ↥H →ₙ* G ⧸ N := ↑((QuotientGroup.mk' N).comp H.subtype)
⊢ IsMulCommutative (G ⧸ N)
Module: Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommGroup G
a : GrothendieckGroup M
⊢ a⁻¹ * a = 1

Tactic:
by
    cases a using ind
    rw [inv_mk, mk_eq_monoidOf_mk', ← Submonoid.LocalizationMap.mk'_mul]
    convert! Submonoid.LocalizationMap.mk'_self' _ _
    rw [mul_comm, Submonoid.coe_mul]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
s : ι → ↥S
⊢ ∏ i ∈ t, mk (f i) (s i) = mk (∏ i ∈ t, f i) (∏ i ∈ t, s i)

Tactic:
classical
  induction t using Finset.induction_on <;> simp [mk_one, Finset.prod_insert, *, mk_mul]

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 : M →* N
h : ∀ (y : ↥S), IsUnit (f ↑y)
x₁ x₂ : M
y₁ y₂ : ↥S
⊢ f x₁ * ↑((IsUnit.liftRight (f.domRestrict S) h) y₁)⁻¹ = f x₂ * ↑((IsUnit.liftRight (f.domRestrict S) h) y₂)⁻¹ ↔
    f (x₁ * ↑y₂) = f (x₂ * ↑y₁)

Tactic:
by
  rw [mul_inv_right h, mul_assoc, mul_comm _ (f y₂), ← mul_assoc, mul_inv_left h, mul_comm x₂,
    f.map_mul, f.map_mul]

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)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
x y : P
⊢ (f.toMonoidHom.comp k.toMonoidHom) x = (f.toMonoidHom.comp k.toMonoidHom) y → ∃ c, ↑c * x = ↑c * y

Tactic:
rw [MonoidHom.comp_apply, MonoidHom.comp_apply, MulEquiv.toMonoidHom_eq_coe,
        MonoidHom.coe_coe, toMonoidHom_apply, toMonoidHom_apply, f.eq_iff_exists]

Goal state after:
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)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
x y : P
⊢ (∃ c, ↑c * k x = ↑c * k y) → ∃ c, ↑c * x = ↑c * y
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: 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
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ ↑(sc * sa) * r₁ = rc * ↑(sb * s₂)

Tactic:
rw [Submonoid.coe_mul, Submonoid.coe_mul, ← mul_assoc, ← hc, mul_assoc _ ra, ← ha, mul_assoc]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithTop α
hb : b ≠ 0
⊢ ⊤ * b = ⊤

Tactic:
rw [top_mul', if_neg hb]

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

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
⊢ x ^ n = ⊤ ↔ x = ⊤ ∧ n ≠ 0

Tactic:
by
  cases x <;> cases n <;> simp [← coe_pow]

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
hab : succ a = b
⊢ False

Tactic:
subst hab

Goal state after:
case neg
α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
h : ¬IsMax a
hb : IsSuccPrelimit (succ a)
ha : a < succ a
⊢ False
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x : α
inst✝⁴ : PartialOrder α
inst✝³ : AddMonoidWithOne α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : SuccAddOrder α
⊢ 1 ≤ x ↔ 0 < x

Tactic:
by
  rw [← succ_le_iff_of_not_isMax not_isMax_zero, succ_eq_add_one, zero_add]

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

Goal state before:
pp: α : Type u_1
x y : α
inst✝² : PartialOrder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
hx : IsSuccPrelimit x
hy : y < x
n : ℕ
⊢ y + ↑(n + 1) < x

Tactic:
Nat.cast_add_one,

Goal state after:
α : Type u_1
x y : α
inst✝² : PartialOrder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
hx : IsSuccPrelimit x
hy : y < x
n : ℕ
⊢ y + (↑n + 1) < x
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝² : PartialOrder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
hx : IsPredPrelimit x
hy : x < y
n : ℕ
⊢ x < y - ↑(n + 1)

Tactic:
Nat.cast_add_one,

Goal state after:
α : Type u_1
x y : α
inst✝² : PartialOrder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
hx : IsPredPrelimit x
hy : x < y
n : ℕ
⊢ x < y - (↑n + 1)
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case pos
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
b : α
hb : b ∈ s
n : ℕ
hn : pred^[n] b ∈ s → f (pred^[n] b) ≤ f b
ha : pred (pred^[n] b) ∈ s
this : pred^[n] b ∈ s
ha' : IsMin (pred^[n] b)
⊢ f (pred (pred^[n] b)) ≤ f b

Tactic:
pred_eq_iff_isMin.2 ha'

Goal state after:
case pos
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
b : α
hb : b ∈ s
n : ℕ
hn : pred^[n] b ∈ s → f (pred^[n] b) ≤ f b
ha : pred (pred^[n] b) ∈ s
this : pred^[n] b ∈ s
ha' : IsMin (pred^[n] b)
⊢ f (pred^[n] b) ≤ f b
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case pos
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝ : ↑s
x : α
hx : x ∈ s
h' : pred x ∈ s
h : IsMin x
⊢ IsMin ⟨x, hx⟩

Tactic:
rintro ⟨y, _⟩ hy

Goal state after:
case pos
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝ : ↑s
x : α
hx : x ∈ s
h' : pred x ∈ s
h : IsMin x
y : α
property✝ : y ∈ s
hy : ⟨y, property✝⟩ ≤ ⟨x, hx⟩
⊢ ⟨x, hx⟩ ≤ ⟨y, property✝⟩
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case pos
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
hab : ¬IsMin b
n : ℕ
hn : pred^[n + 1] b ∈ s → f (pred^[n + 1] b) < f b
ha : pred (pred^[n + 1] b) ∈ s
this : pred^[n + 1] b ∈ s
ha' : IsMin (pred^[n + 1] b)
⊢ f (pred (pred^[n + 1] b)) < f b

Tactic:
pred_eq_iff_isMin.2 ha'

Goal state after:
case pos
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
hab : ¬IsMin b
n : ℕ
hn : pred^[n + 1] b ∈ s → f (pred^[n + 1] b) < f b
ha : pred (pred^[n + 1] b) ∈ s
this : pred^[n + 1] b ∈ s
ha' : IsMin (pred^[n + 1] b)
⊢ f (pred^[n + 1] b) < f b
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ ↥t
hg' : ∀ i ∈ s, ↑(g' i) = f i
hfat : f a ∈ t
⊢ ∃ g, ∀ i ∈ insert a s, ↑(g i) = f i

Tactic:
use g'.trans (Equiv.swap (⟨f a, hfat⟩ : t) (g' a))

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ ↥t
hg' : ∀ i ∈ s, ↑(g' i) = f i
hfat : f a ∈ t
⊢ ∀ i ∈ insert a s, ↑((g'.trans (Equiv.swap ⟨f a, hfat⟩ (g' a))) i) = f i
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
n✝ n' m : ℕ
s : Sym α✝ n✝
a b : α✝
α : Type u_3
n : ℕ
x✝ : List α
⊢ x✝.length = n ↔ Multiset.card ⟦x✝⟧ = n

Tactic:
by rfl

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
n✝ n' m : ℕ
s : Sym α✝ n✝
a b : α✝
α : Type u_3
n : ℕ
x✝¹ x✝ : { l // l.length = n }
⊢ (Vector.Perm.isSetoid α n) x✝¹ x✝ ↔ (List.isSetoid α) ↑x✝¹ ↑x✝

Tactic:
by rfl

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

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
⊢ ↑(replicate n a) = Multiset.replicate n a

Tactic:
coe_replicate

Goal state after:
α : Type u_1
n : ℕ
a : α
⊢ Multiset.replicate n a = Multiset.replicate n a
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
property✝ : [].length = n
⊢ (tail ⟨[], property✝⟩).toList = (toList ⟨[], property✝⟩).tail

Tactic:
by rfl

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

Goal state before:
pp: α : Type u_1
n : ℕ
head✝ : α
tail✝ : List α
property✝ : (head✝ :: tail✝).length = n
⊢ (tail ⟨head✝ :: tail✝, property✝⟩).toList = (toList ⟨head✝ :: tail✝, property✝⟩).tail

Tactic:
by rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b : α
s : Sym α 1
l l' : { x // x.length = 1 }
⊢ (Subtype.instSetoid_mathlib fun x ↦ x.length = 1) l l' ↔ (List.isSetoid α) ↑l ↑l'

Tactic:
by rfl

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

Goal state before:
pp: α : Type u_1
n : ℕ
m₁ m₂ : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : ↑m₁.snd = ↑m₂.snd
⊢ ↑m₁.fst = ↑m₂.fst

Tactic:
rw [← Nat.sub_sub_self (Nat.le_of_lt_succ m₁.1.is_lt), ← m₁.2.2, val_eq_coe, h,
        ← val_eq_coe, m₂.2.2, Nat.sub_sub_self (Nat.le_of_lt_succ m₂.1.is_lt)]

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

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
⊢ ⟨((↑v).insertIdx j a).eraseIdx ↑(if ⟨i, ⋯⟩ < ⟨j, hj⟩ then ⟨i, ⋯⟩ else ⟨i + 1, ⋯⟩), ⋯⟩ =
    ⟨(↑(match v with
            | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
        (↑(if h : ⟨i, ⋯⟩ < ⟨j, hj⟩ then ⟨j, hj⟩.pred ⋯ else ⟨j, hj⟩.castPred ⋯)) a,
      ⋯⟩

Tactic:
rw [Subtype.mk_eq_mk]

Goal state after:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
⊢ ((↑v).insertIdx j a).eraseIdx ↑(if ⟨i, ⋯⟩ < ⟨j, hj⟩ then ⟨i, ⋯⟩ else ⟨i + 1, ⋯⟩) =
    (↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
      (↑(if h : ⟨i, ⋯⟩ < ⟨j, hj⟩ then ⟨j, hj⟩.pred ⋯ else ⟨j, hj⟩.castPred ⋯)) a
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f g : r ≼i s
a : α
⊢ f a = g a

Tactic:
Subsingleton.elim f g

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f g : r ≼i s
a : α
⊢ g a = g a
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case bot.bot
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
⊢ Sum.Lex (fun x1 x2 ↦ True) (fun x1 x2 ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    ⊥ ≤ ⊥

Tactic:
simp only [elim_inr, lex_inl_inl, bot_le]

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f g : r ≺i s
a : α
⊢ f.toRelEmbedding a = g.toRelEmbedding a

Tactic:
Subsingleton.elim f g

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f g : r ≺i s
a : α
⊢ g.toRelEmbedding a = g.toRelEmbedding a
Module: Mathlib.Data.Part

Goal state before:
pp: case neg
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
a : α
h : ¬o.Dom
⊢ (a ∈ if h : o.Dom then Option.some (o.get h) else Option.none) ↔ a ∈ o

Tactic:
simp only [h, ↓reduceDIte, Option.mem_def, reduceCtorEq, false_iff]

Goal state after:
case neg
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
a : α
h : ¬o.Dom
⊢ ¬a ∈ o
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Inv α
a : Part α
ma : α
ha : ma ∈ a
⊢ ma⁻¹ ∈ a⁻¹

Tactic:
simp [inv_def]; aesop

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

Goal state before:
pp: a : Cardinal.{u}
⊢ a < 2 ^ a

Tactic:
induction a using Cardinal.inductionOn with | _ α

Goal state after:
case mk
α : Type u
⊢ #α < 2 ^ #α
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case mk
α : Type u
⊢ #α < 2 ^ #α

Tactic:
rw [← mk_set]

Goal state after:
case mk
α : Type u
⊢ #α < #(Set α)
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: α : 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, Bijective h ∧ ∀ (a : α), R a (h a)

Tactic:
rcases isEmpty_or_nonempty β with hβ | hβ
  · have : IsEmpty α := Function.isEmpty f
    exact ⟨_, ((Equiv.equivEmpty α).trans (Equiv.equivEmpty β).symm).bijective, by simp⟩
  set F : Set α →o Set α :=
    { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ
      monotone' := fun s t hst => by dsimp at hst ⊢; gcongr }
  set s : Set α := F.lfp
  have hs : (g '' (f '' s)ᶜ)ᶜ = s := F.map_lfp
  have hns : g '' (f '' s)ᶜ = sᶜ := compl_injective (by simp [hs])
  set g' := invFun g
  have g'g : LeftInverse g' g := leftInverse_invFun hg
  have hg'ns : g' '' sᶜ = (f '' s)ᶜ := by rw [← hns, g'g.image_image]
  set h : α → β := s.piecewise f g'
  have : Surjective h := by rw [← range_eq_univ, range_piecewise, hg'ns, union_compl_self]
  have : Injective h := by
    refine (injective_piecewise_iff _).2 ⟨hf.injOn, ?_, ?_⟩
    · intro x hx y hy hxy
      obtain ⟨x', _, rfl⟩ : x ∈ g '' (f '' s)ᶜ := by rwa [hns]
      obtain ⟨y', _, rfl⟩ : y ∈ g '' (f '' s)ᶜ := by rwa [hns]
      rw [g'g _, g'g _] at hxy
      rw [hxy]
    · intro x hx y hy hxy
      obtain ⟨y', hy', rfl⟩ : y ∈ g '' (f '' s)ᶜ := by rwa [hns]
      rw [g'g _] at hxy
      exact hy' ⟨x, hx, hxy⟩
  refine ⟨h, ⟨‹Injective h›, ‹Surjective h›⟩, fun a ↦ ?_⟩
  simp only [h, Set.piecewise, g']
  split
  · exact hp₁ a
  · have : g (invFun g a) = a := by
      have : a ∈ g '' (f '' s)ᶜ := by grind
      obtain ⟨x, _, hx⟩ := mem_image _ _ _ |>.mp this
      exact Function.invFun_eq ⟨x, hx⟩
    grind

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case a.zero
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ (iterateChain (↑f) x h) 0 ≤ ωSup ((iterateChain (↑f) x h).map ↑f)

Tactic:
apply le_trans h

Goal state after:
case a.zero
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ f x ≤ ωSup ((iterateChain (↑f) x h).map ↑f)
Module: Mathlib.Algebra.Group.Hom.CompTypeclasses

Goal state before:
pp: case mp
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
Q : Type u_4
inst✝ : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
h : φ₂₃.comp φ₁ = φ₁₂₃
⊢ φ₁₂.CompTriple φ₃ φ₁₂₃

Tactic:
exact ⟨by simp only [← κ.comp_eq, ← h, ← κ'.comp_eq, MonoidHom.comp_assoc]⟩

Goal state after:
Module: Mathlib.Algebra.Group.Hom.CompTypeclasses

Goal state before:
pp: case mpr
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
Q : Type u_4
inst✝ : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
h : φ₃.comp φ₁₂ = φ₁₂₃
⊢ φ₁.CompTriple φ₂₃ φ₁₂₃

Tactic:
exact ⟨by simp only [← κ.comp_eq, ← h, ← κ'.comp_eq, MonoidHom.comp_assoc]⟩

Goal state after:
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝¹ : Monoid R
inst✝ : MulAction R M
a b : M
ab : (fun x ↦ 1 • x) a = (fun x ↦ 1 • x) b
⊢ a = b

Tactic:
dsimp only [Function.comp_def] at ab
  rw [one_smul, one_smul] at ab
  assumption

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

Goal state before:
pp: α : Type u
h : #α = ℵ₀
f : α ≃ ULift.{u, 0} ℕ
⊢ Nonempty (Denumerable α)

Tactic:
exact ⟨Denumerable.mk' <| f.trans Equiv.ulift⟩

Goal state after: