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

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidablePred fun x ↦ x ≤ a
hab : a < b
⊢ filter (fun x ↦ x ≤ a) (Ico a b) = {a}

Tactic:
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_left hab]

Goal state after:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidablePred fun x ↦ x ≤ a
hab : a < b
⊢ {a}.val = {a}
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✝ : LocallyFiniteOrderBot α
⊢ Finite { x // x ≤ y }

Tactic:
by
  simpa only [coe_Iic] using! (Finset.Iic y).finite_toSet

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

Goal state before:
pp: case h
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)
nx : ℕ
hx : r ^ nx • x ∈ closure (r • s)
ny : ℕ
hy : r ^ ny • y ∈ closure (r • s)
⊢ r ^ (ny + nx) • (x * y) ∈ closure (r • s)

Tactic:
pow_add,

Goal state after:
case h
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)
nx : ℕ
hx : r ^ nx • x ∈ closure (r • s)
ny : ℕ
hy : r ^ ny • y ∈ closure (r • s)
⊢ (r ^ ny * r ^ nx) • (x * y) ∈ closure (r • s)
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
c : α
h : ⟦a⟧ = ⟦b⟧
hb : b ∈ MulAction.orbit ↥H ⟦a⟧.out
⊢ ↑b ∈ MulAction.orbit ↥H ↑a

Tactic:
orbitRel.Quotient.mem_subgroup_orbit_iff

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
c : α
h : ⟦a⟧ = ⟦b⟧
hb : b ∈ MulAction.orbit ↥H ⟦a⟧.out
⊢ b ∈ MulAction.orbit (↥H) a
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: M✝ : Type u_1
inst✝² : MulOneClass M✝
M : Type u_2
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
c : ↥(center M)
r : M
v : α
⊢ c • r • v = r • c • v

Tactic:
have := Semigroup.mem_center_iff.1 c.2
    simp_rw [Submonoid.smul_def, smul_smul, this]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun x ↦ (ofLex x).2
h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x ↦ (ofLex x).1) ⁻¹' {a})
b c : Lex (α × β)
hbc : b ≤ c
hb : (ofLex b).1 = a
hc : (ofLex c).1 = a
this : (ofLex b).1 < (ofLex c).1 ∨ (ofLex b).1 = (ofLex c).1 ∧ f b ≤ f c
⊢ f b ≤ f c

Tactic:
simp_all only [lt_self_iff_false, true_and, false_or]

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)
y : β
h : ∀ x ∈ s, Commute y (f x)
x : α
hx : x ∈ s.val
⊢ Commute y (f x)

Tactic:
exact h x hx

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)
y : β
h : ∀ x ∈ s, Commute y (f x)
⊢ Commute y (s.noncommProd f comm)

Tactic:
by
  apply Multiset.noncommProd_commute
  intro y
  rw [Multiset.mem_map]
  rintro ⟨x, ⟨hx, rfl⟩⟩
  exact h x hx

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
comm : (↑t).Pairwise (Function.onFun Commute f)
h : ∀ c ∈ t, f c ∈ S
x : ι
hx : x ∈ t.val
⊢ f x ∈ S

Tactic:
exact h x hx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : Setoid α
s : Setoid β
q : Quotient (r.prod s)
x y : α × β
hxy : (r.prod s) x y
⊢ (Quotient.mk'' x.1, Quotient.mk'' x.2).2 = (Quotient.mk'' y.1, Quotient.mk'' y.2).2

Tactic:
by simpa [Quotient.eq] using hxy.2

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

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

Tactic:
have h₁ : Red ((x, not b) :: (x, b) :: L) [(x, not b)] := cons_cons h

Goal state after:
α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
⊢ Red L [(x, !b)]
Module: Mathlib.GroupTheory.Coset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
s : Subgroup α
inst✝ : DecidablePred fun x ↦ x ∈ s
x y : α
⊢ Decidable ((leftRel s) x y)

Tactic:
by
  rw [leftRel_eq]
  exact ‹DecidablePred (· ∈ s)› _

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
n✝ n : ℕ
⊢ mk L * mk L ^ n = mk (List.replicate (n + 1) L).flatten

Tactic:
pow_mk,

Goal state after:
α : Type u
L : List (α × Bool)
n✝ n : ℕ
⊢ mk L * mk (List.replicate n L).flatten = mk (List.replicate (n + 1) L).flatten
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ FreeGroup Unit → FreeGroup ℤ

Tactic:
exact ↑(map fun _ => (1 : ℤ))

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
h : ∀ (x x_1 : G), x_1⁻¹ * x ∈ N
⊢ N = ⊤

Tactic:
ext; simpa using h _ 1

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
h : ∀ (x x_1 : G), x * x_1⁻¹ ∈ N
⊢ N = ⊤

Tactic:
ext; simpa using h _ 1

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s✝ : Finset ι
inst✝ : CommMonoid M
f : ι → M
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
this : {x, g x hx} ⊆ s
h : ∏ x ∈ s \ {x, g x hx}, f x = 1
x✝ : g x hx = x ∨ g x hx ≠ x
⊢ ∏ x ∈ {x, g x hx}, f x = 1

Tactic:
cases eq_or_ne (g x hx) x with

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

Goal state before:
pp: case a
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅H₁.prod K₁, H₂.prod K₂⁆ ≤ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆

Tactic:
rw [commutator_le]
    rintro ⟨p₁, p₂⟩ ⟨hp₁, hp₂⟩ ⟨q₁, q₂⟩ ⟨hq₁, hq₂⟩
    exact ⟨commutator_mem_commutator hp₁ hq₁, commutator_mem_commutator hp₂ hq₂⟩

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • r' = v • r
hsu : ↑u * ↑s' = v * ↑s
⊢ ∃ u v, u • r = v • r' ∧ ↑u * ↑s = v * ↑s'

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

Goal state after:
case refine_1
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • r' = v • r
hsu : ↑u * ↑s' = v * ↑s
r₂ : R
s₂ : ↥S
h₁ : ↑s₂ * ↑s = r₂ * ↑s'
⊢ ∃ u v, u • r = v • r' ∧ ↑u * ↑s = v * ↑s'
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case e_s
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₂
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * (r₂ * r₁) = r₂' * ↑s₂
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * (↑s₂' * r₂) = r₃' * ↑s₁'
this✝ : ↑s₃' * r₂' * ↑s₂ = r₃' * r₁' * ↑s₂
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₂') = ↑s₄' * (r₃' * r₁')
this : ↑s₄' * r₃' * (↑s₁' * ↑s) ∈ S
⊢ ↑s₄' * r₃' * ↑s₁' * ↑s = ↑s₄' * ↑s₃' * ↑s₂' * r₂ * ↑s

Tactic:
rw [mul_assoc _ r₃', ← h₃, ← mul_assoc, ← mul_assoc]

Goal state after:
Module: Mathlib.Algebra.Ring.Equiv

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
R✝ : Type u_4
S✝ : Type u_5
S'✝ : Type u_6
inst✝⁶ : NonUnitalNonAssocSemiring R✝
inst✝⁵ : NonUnitalNonAssocSemiring S✝
f✝ : R✝ ≃+* S✝
x : R✝
inst✝⁴ : FunLike F R✝ S✝
R : Type u_7
R' : Type u_8
S : Type u_9
S' : Type u_10
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : NonUnitalNonAssocSemiring R'
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring S'
f : R ≃+* R'
g : S ≃+* S'
x✝¹ x✝ : R × S
⊢ ((↑f).prodCongr ↑g).toFun (x✝¹ + x✝) = ((↑f).prodCongr ↑g).toFun x✝¹ + ((↑f).prodCongr ↑g).toFun x✝

Tactic:
by
    simp only [Equiv.toFun_as_coe, Equiv.prodCongr_apply, EquivLike.coe_coe,
      Prod.map, map_add, Prod.mk_add_mk]

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : MulZeroClass α
inst✝ : LT α
a b : WithTop α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ a * b ≠ ⊤

Tactic:
exact mul_ne_top ha hb

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

Goal state before:
pp: M : Type u_3
X : Type u_4
inst✝² : Monoid M
S : Submonoid M
inst✝¹ : OreSet S
inst✝ : MulAction M X
r : M
x : OreLocalization S X
⊢ (r /ₒ 1) • x = r • x

Tactic:
by
  cases x
  rw [smul_oreDiv, oreDiv_smul_oreDiv, mul_one, smul_eq_mul, mul_one]

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
b₂ : WithTop α
this : MulPosStrictMono α
a₁ b₁ : α
hb : ↑b₁ < b₂
ha : ↑a₁ < ⊤
⊢ b₂ ≠ 0

Tactic:
by simpa [bot_eq_zero] using hb.bot_lt.ne'

Goal state after:
Module: Mathlib.Order.Iterate

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
f : α → α
h : id ≤ f
n : ℕ
x : α
⊢ f^[n] x ≤ f^[n + 1] x

Tactic:
rw [iterate_succ_apply']
    exact h _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Icc (succ a) b = Ioc a b

Tactic:
← Ici_inter_Iic,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Ici (succ a) ∩ Iic b = Ioc a b
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a : α
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
h : IsSuccPrelimit a
b : α
hb : b ≤ a
⊢ a ≤ b

Tactic:
by
  revert h
  refine Succ.rec (fun _ => le_rfl) (fun c _ H hc => ?_) hb
  have := hc.isMax.succ_eq
  rw [this] at hc ⊢
  exact H hc

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

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
⊢ a ≤ b ∧ b ≤ succ a ↔ b = a ∨ b = succ a

Tactic:
refine ⟨fun h ↦ or_iff_not_imp_left.2 fun hba : b ≠ a ↦
    h.2.antisymm (succ_le_of_lt <| h.1.lt_of_ne <| hba.symm), ?_⟩

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
⊢ b = a ∨ b = succ a → a ≤ b ∧ b ≤ succ a
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ a ≤ succ b ↔ a = succ b ∨ a ≤ b

Tactic:
· rw [← lt_succ_iff_of_not_isMax hb, le_iff_eq_or_lt]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ succ b
⊢ Icc a (succ b) = insert (succ b) (Icc a b)

Tactic:
← Ici_inter_Iic,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ succ b
⊢ Ici a ∩ Iic (succ b) = insert (succ b) (Ici a ∩ Iic b)
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
⊢ succ a = sInf (Ioi a)

Tactic:
apply (le_csInf nonempty_Ioi fun b => succ_le_of_lt).antisymm
  exact csInf_le ⟨a, fun b => le_of_lt⟩ <| lt_succ a

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

Goal state before:
pp: a b c d m n : ℕ∞
x : ℕ∞ˣ
x_top : ↑x ≠ ⊤
x_inv_top : x.inv ≠ ⊤
y z : ℕ
this : y = 1 ∧ z = 1
x_z : ↑z = x.inv
x_y : ↑x = 1
⊢ x = default

Tactic:
Units.val_eq_one

Goal state after:
a b c d m n : ℕ∞
x : ℕ∞ˣ
x_top : ↑x ≠ ⊤
x_inv_top : x.inv ≠ ⊤
y z : ℕ
this : y = 1 ∧ z = 1
x_z : ↑z = x.inv
x_y : x = 1
⊢ x = default
Module: Mathlib.Data.Finset.Piecewise

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

Tactic:
ext
  congr

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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
r : Finset (α × γ)
s : Finset γ
t : γ → Finset α
h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2
f : α × γ → β
⊢ ∏ p ∈ r, f p = ∏ c ∈ s, ∏ a ∈ t c, f (a, c)

Tactic:
by
  refine Eq.trans ?_ (prod_sigma s t fun p => f (p.2, p.1))
  apply prod_equiv ((Equiv.prodComm _ _).trans (Equiv.sigmaEquivProd _ _).symm) <;> simp [h]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
⊢ (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, f x = ∏ x ∈ s, f x

Tactic:
by
  convert! (s.prod_piecewise t f f).symm
  simp +unfoldPartialApp [Finset.piecewise]

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 : α
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ (filter (fun x ↦ a ≠ x) ↑m).card + ↑⟨count a ↑m, ⋯⟩ = (↑m).card

Tactic:
← countP_eq_card_filter,

Goal state after:
α : Type u_1
β : Type u_2
n n' m✝ : ℕ
s : Sym α n
a✝ b : α
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ countP (fun x ↦ a ≠ x) ↑m + ↑⟨count a ↑m, ⋯⟩ = (↑m).card
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
⊢ ∏ j, Function.update (fun j ↦ #(s j)) i 1 j = ∏ j ∈ univ.erase i, #(s j)

Tactic:
by simp [prod_update_of_mem, erase_eq]

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

Goal state before:

Tactic:
_ ≤ (Finset.univ.image List.ofFn).card := by
          apply Finset.card_le_card
          intro a ha
          let hlen := Finset.mem_filter.mp ha
          exact Finset.mem_image.mpr ⟨
              (fun j : Fin s => a.get ⟨j.val, by simp [hlen]⟩),
              by simp,
              List.ext_get (by simp [hlen]) (by simp)⟩
    _ = Fintype.card α ^ s := by
          simp [card_image_of_injective univ List.ofFn_injective]

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

Goal state before:
pp: α : Type u
s : Set (Set α)
hs : s.Countable
⊢ (⋃₀ s).Countable ↔ ∀ a ∈ s, a.Countable

Tactic:
by rw [sUnion_eq_biUnion, hs.biUnion_iff]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl r
inst✝ : Std.Irrefl s
a✝ : α
h : r a✝ a✝
⊢ False

Tactic:
exact irrefl _ h

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl r
inst✝ : Std.Irrefl s
b✝ : β
h : s b✝ b✝
⊢ False

Tactic:
exact irrefl _ h

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl r
inst✝ : Std.Irrefl s
a₁✝ : α
h : r a₁✝ a₁✝
⊢ False

Tactic:
exact irrefl _ h

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl r
inst✝ : Std.Irrefl s
b₁✝ : β
h : s b₁✝ b₁✝
⊢ False

Tactic:
exact irrefl _ h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LE α
inst✝¹ : OrderBot α
inst✝ : LE β
⊢ ∀ (a : α ⊕ₗ β), inl ⊥ ≤ a

Tactic:
by
    rintro (a | b)
    · exact Lex.inl bot_le
    · exact Lex.sep _ _

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

Goal state before:
pp: ι : Type u_1
f : ι → Cardinal.{u_2}
⊢ prod f ≠ 0 ↔ ∀ (i : ι), f i ≠ 0

Tactic:
simp [prod_eq_zero]

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
⊢ (fun x ↦ (f x, g x)) a ∈ {x | ∀ ⦃a : β × γ⦄, a ∈ (fun x ↦ (f x, g x)) '' d → a ≤ x}

Tactic:
simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_ofPred_eq,
      Prod.mk_le_mk]
    intro b hb
    exact ⟨hf.monotone D hD (hda.1 hb), hg.monotone D hD (hda.1 hb)⟩

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

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

Tactic:
have : Surjective h := by rw [← range_eq_univ, range_piecewise, hg'ns, union_compl_self]

Goal state after:
case inr
α : 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
⊢ ∃ h, Bijective h ∧ ∀ (a : α), R a (h a)
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β : 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
this : a ∈ g '' (f '' s)ᶜ
⊢ g (invFun g a) = a

Tactic:
obtain ⟨x, _, hx⟩ := mem_image _ _ _ |>.mp this

Goal state after:
α : 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
this : a ∈ g '' (f '' s)ᶜ
x : β
left✝ : x ∈ (f '' s)ᶜ
hx : g x = a
⊢ g (invFun g a) = a
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case a.succ
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
n : ℕ
this : (iterateChain (↑f) x h) n.succ = ((iterateChain (↑f) x h).map ↑f) n
⊢ (iterateChain (↑f) x h) (n + 1) ≤ ωSup ((iterateChain (↑f) x h).map ↑f)

Tactic:
rw [this]

Goal state after:
case a.succ
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
n : ℕ
this : (iterateChain (↑f) x h) n.succ = ((iterateChain (↑f) x h).map ↑f) n
⊢ ((iterateChain (↑f) x h).map ↑f) n ≤ ωSup ((iterateChain (↑f) x h).map ↑f)
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case succ
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : f a ≤ a
h_x_le_a : x ≤ a
n : ℕ
h_ind : (iterateChain (↑f) x h) n ≤ a
this : (iterateChain (↑f) x h) n.succ = f ((iterateChain (↑f) x h) n)
⊢ (iterateChain (↑f) x h) (n + 1) ≤ a

Tactic:
rw [this]

Goal state after:
case succ
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : f a ≤ a
h_x_le_a : x ≤ a
n : ℕ
h_ind : (iterateChain (↑f) x h) n ≤ a
this : (iterateChain (↑f) x h) n.succ = f ((iterateChain (↑f) x h) n)
⊢ f ((iterateChain (↑f) x h) n) ≤ a
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: c : Cardinal.{u}
⊢ lift.{v, u} c < ℵ₀ ↔ c < ℵ₀

Tactic:
by
  simpa using lift_lt (b := ℵ₀)

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

Goal state before:
pp: x : Cardinal.{v}
m : ℕ∞
⊢ lift.{u, v} x < ↑m ↔ x < ↑m

Tactic:
by
  rw [← lift_ofENat.{u, v}, lift_lt]

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

Goal state before:
pp: x : Cardinal.{v}
m : ℕ∞
⊢ ↑m < lift.{u, v} x ↔ ↑m < x

Tactic:
by
  rw [← lift_ofENat.{u, v}, lift_lt]

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
hf : BddAbove (range f)
g : Cardinal.{v} → Cardinal.{max v w}
⊢ BddAbove (g '' range f)

Tactic:
exact bddAbove_image g hf

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
i : ι
⊢ lift.{u, v} (f i) ≤ ⨆ i, lift.{u, v} (f i)

Tactic:
exact le_ciSup bddAbove_of_small i

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

Goal state before:
pp: case mp
α : Type u_1
s : Set α
n : ℕ
h : #↑s = ↑n
⊢ ∃ t, ↑t = s ∧ t.card = n

Tactic:
lift s to Finset α using lt_aleph0_iff_set_finite.1 (h.symm ▸ natCast_lt_aleph0)

Goal state after:
case mp
α : Type u_1
n : ℕ
s : Finset α
h : #↑↑s = ↑n
⊢ ∃ t, ↑t = ↑s ∧ t.card = n
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
A B : Set α
hfin : B.Finite
hlt : A ⊂ B
this✝ : Fintype ↑A
this : Fintype ↑B
⊢ #↑A < #↑B

Tactic:
simpa using Finset.card_lt_card <| Set.toFinset_ssubset_toFinset.mpr hlt

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic

Goal state before:
pp: M : Type u_1
β : Type u_2
α : Type u_3
N : Type u_4
inst✝² : SMul M α
inst✝¹ : FaithfulSMul M α
inst✝ : Nontrivial β
c₁ c₂ : Mᵈᵐᵃ
h : ∀ (a : α → β), c₁ • a = c₂ • a
a : α
⊢ mk.symm c₁ • a = mk.symm c₂ • a

Tactic:
rcases exists_pair_ne β with ⟨x, y, hne⟩
    contrapose! hne
    have := Classical.decEq α
    replace h := congr_fun (h (update (const α x) (mk.symm c₂ • a) y)) a
    simpa [smul_apply, hne] using h

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Pi

Goal state before:
pp: I : Type u
f : I → Type v
g : I → Type u_1
n : (i : I) → Zero (g i)
inst✝ : (i : I) → SMulZeroClass (f i) (g i)
a✝ : (i : I) → f i
x : I
⊢ (a✝ • 0) x = 0 x

Tactic:
exact smul_zero _

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Pi

Goal state before:
pp: I : Type u
f : I → Type v
g : I → Type u_1
n : (i : I) → AddZeroClass (g i)
inst✝ : (i : I) → DistribSMul (f i) (g i)
a✝ : (i : I) → f i
x : I
⊢ (a✝ • 0) x = 0 x

Tactic:
exact smul_zero _

Goal state after: