mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.QuotientGroup.Finite

Goal state before:
pp: G : Type u_2
inst✝² : Group G
H : Subgroup G
inst✝¹ : Finite ↥H
inst✝ : Finite (G ⧸ H)
⊢ Finite ↥?m.11 ∧ Finite (G ⧸ ?m.11)

pp: G : Type u_2
inst✝² : Group G
H : Subgroup G
inst✝¹ : Finite ↥H
inst✝ : Finite (G ⧸ H)
⊢ Subgroup G

Tactic:
constructor <;> assumption

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

Goal state before:
pp: case inl
α : Type u_1
s t : Set α
h : (s ∪ t).Finite
⊢ (s ∪ t).encard ≤ s.encard + ↑t.ncard

Tactic:
(h.subset subset_union_right).cast_ncard_eq

Goal state after:
case inl
α : Type u_1
s t : Set α
h : (s ∪ t).Finite
⊢ (s ∪ t).encard ≤ s.encard + t.encard
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set (α ⧸ s)
x✝ : ↥s × ↑t
a : α
ha : a ∈ s
x : α ⧸ s
hx : x ∈ t
⊢ (fun a ↦ (⟨(Quotient.out ↑↑a)⁻¹ * ↑a, ⋯⟩, ⟨↑↑a, ⋯⟩)) ((fun a ↦ ⟨Quotient.out ↑a.2 * ↑a.1, ⋯⟩) (⟨a, ha⟩, ⟨x, hx⟩)) =
    (⟨a, ha⟩, ⟨x, hx⟩)

Tactic:
by ext <;> simp [ha]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
⊢ ∀ (r : R) (x : A × B), ((algebraMap R A).prod (algebraMap R B)) r * x = x * ((algebraMap R A).prod (algebraMap R B)) r

Tactic:
rintro r ⟨a, b⟩

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
r : R
a : A
b : B
⊢ ((algebraMap R A).prod (algebraMap R B)) r * (a, b) = (a, b) * ((algebraMap R A).prod (algebraMap R B)) r
Module: Mathlib.Algebra.Algebra.Prod

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
⊢ ∀ (r : R) (x : A × B), r • x = ((algebraMap R A).prod (algebraMap R B)) r * x

Tactic:
rintro r ⟨a, b⟩

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
r : R
a : A
b : B
⊢ r • (a, b) = ((algebraMap R A).prod (algebraMap R B)) r * (a, b)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
ht : t.Infinite
hst : s ⊆ t
hs : s.Finite
k : ℕ
hsk : s.ncard ≤ k
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ t ∧ s'.ncard = k

Tactic:
obtain ⟨s₁, hs₁, hs₁fin, hs₁card⟩ := (ht.sdiff hs).exists_subset_ncard_eq (k - s.ncard)
  refine ⟨s ∪ s₁, subset_union_left, union_subset hst (hs₁.trans sdiff_subset), ?_⟩
  rwa [ncard_union_eq (disjoint_of_subset_right hs₁ disjoint_sdiff_right) hs hs₁fin, hs₁card,
    add_tsub_cancel_of_le]

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

Goal state before:
pp: α : Type u_1
s t : Set α
n : ℕ
hu : (s ∪ t).Finite
hst : 2 * n < hu.toFinset.card
⊢ ∃ r, n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)

Tactic:
Finite.toFinset_union (hu.subset subset_union_left)
      (hu.subset subset_union_right)

Goal state after:
α : Type u_1
s t : Set α
n : ℕ
hu : (s ∪ t).Finite
hst : 2 * n < (⋯.toFinset ∪ ⋯.toFinset).card
⊢ ∃ r, n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
hs : s.Finite
⊢ (∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n) → s.ncard = n + 1

Tactic:
rintro ⟨a, t, hat, h, rfl⟩

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
a : α
t : Set α
hat : a ∉ t
h : insert a t = s
⊢ s.ncard = t.ncard + 1
Module: Mathlib.LinearAlgebra.Quotient.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
h : p = p'
a b : M
⊢ p.quotientRel a b ↔ p'.quotientRel ((Equiv.refl M) a) ((Equiv.refl M) b)

Tactic:
subst h
      rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Quotient.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
h : p = p'
⊢ ∀ (x y : M ⧸ p),
    (Quotient.congr (Equiv.refl M) ⋯).toFun (x + y) =
      (Quotient.congr (Equiv.refl M) ⋯).toFun x + (Quotient.congr (Equiv.refl M) ⋯).toFun y

Tactic:
rintro ⟨x⟩ ⟨y⟩
      rfl

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

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✝ f : M →* P
x y : (ker f).Quotient
h : (kerLift f).mrangeRestrict x = (kerLift f).mrangeRestrict y
⊢ (kerLift f) x = (kerLift f) y

Tactic:
by rcases x with ⟨⟩; rcases y with ⟨⟩; injections

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Monoid

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a d x✝ : M
h : x✝ ∈ Ioi (a + d)
⊢ x✝ ∈ (fun x ↦ x + d) '' Ioi a

Tactic:
obtain ⟨c, rfl⟩ := exists_add_of_le (mem_Ioi.mp h).le

Goal state after:
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : ExistsAddOfLE M
a d c : M
h : a + d + c ∈ Ioi (a + d)
⊢ a + d + c ∈ (fun x ↦ x + d) '' Ioi a
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
h_mem : ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j
f : ℕ → ↥(Finset.Icc i j) := fun n ↦ ⟨succ^[n] i, ⋯⟩
n m : ℕ
hnm_ne : n ≠ m
hfnm : f n = f m
⊢ ∃ n m, n < m ∧ succ^[n] i = succ^[m] i

Tactic:
have hnm_eq : succ^[n] i = succ^[m] i := by simpa only [f, Subtype.mk_eq_mk] using hfnm

Goal state after:
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
h_mem : ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j
f : ℕ → ↥(Finset.Icc i j) := fun n ↦ ⟨succ^[n] i, ⋯⟩
n m : ℕ
hnm_ne : n ≠ m
hfnm : f n = f m
hnm_eq : succ^[n] i = succ^[m] i
⊢ ∃ n m, n < m ∧ succ^[n] i = succ^[m] i
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
⊢ StrictMono (toZ i0)

Tactic:
intro j i h_le

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 j i : ι
h_le : j < i
⊢ toZ i0 j < toZ i0 i
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommGroup M
n : ℕ
a b : Fin n
hab : a ≤ b
f : Fin (n + 1) → M
⊢ (∏ i ∈ Icc ↑a ↑b, if h : i < n then f ⟨i, h⟩.succ / f ⟨i, h⟩.castSucc else 1) = f b.succ / f a.castSucc

Tactic:
convert! Finset.prod_Icc_div (Fin.le_def.1 hab) (fun i ↦ if hi : i < n + 1 then f ⟨i, hi⟩ else 1)

Goal state after:
case e'_2.a
M : Type u_3
inst✝ : CommGroup M
n : ℕ
a b : Fin n
hab : a ≤ b
f : Fin (n + 1) → M
x✝ : ℕ
a✝ : x✝ ∈ Icc ↑a ↑b
⊢ (if h : x✝ < n then f ⟨x✝, h⟩.succ / f ⟨x✝, h⟩.castSucc else 1) =
    (if hi : x✝ + 1 < n + 1 then f ⟨x✝ + 1, hi⟩ else 1) / if hi : x✝ < n + 1 then f ⟨x✝, hi⟩ else 1

case e'_3.e'_5
M : Type u_3
inst✝ : CommGroup M
n : ℕ
a b : Fin n
hab : a ≤ b
f : Fin (n + 1) → M
⊢ f b.succ = if hi : ↑b + 1 < n + 1 then f ⟨↑b + 1, hi⟩ else 1

case e'_3.e'_6
M : Type u_3
inst✝ : CommGroup M
n : ℕ
a b : Fin n
hab : a ≤ b
f : Fin (n + 1) → M
⊢ f a.castSucc = if hi : ↑a < n + 1 then f ⟨↑a, hi⟩ else 1
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Ring α
x y : α
⊢ span {x, -y} = span {x, y}

Tactic:
by
  rw [span_pair_comm, span_insert_neg, span_pair_comm]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝² : Ring R
I J : Ideal R
a b : R
S : Type v
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
h : I = J
⊢ ∀ (x y : R ⧸ I),
    (↑(Submodule.quotEquivOfEq I J h)).toFun (x * y) =
      (↑(Submodule.quotEquivOfEq I J h)).toFun x * (↑(Submodule.quotEquivOfEq I J h)).toFun y

Tactic:
rintro ⟨x⟩ ⟨y⟩
      rfl

Goal state after:
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case zero.inl
α : Type u_2
inst✝ : CommSemiring α
hs : span ∅ = ⊤
⊢ 1 ∈ span ((fun x ↦ x ^ 0) '' ∅)

Tactic:
rw [Set.image_empty, hs]

Goal state after:
case zero.inl
α : Type u_2
inst✝ : CommSemiring α
hs : span ∅ = ⊤
⊢ 1 ∈ ⊤
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: R : Type u_3
inst✝² : Ring R
I : Ideal R
inst✝¹ : Finite ↥I
inst✝ : Finite (R ⧸ I)
⊢ Finite ↥?m.9 ∧ Finite (R ⧸ ?m.9)

pp: R : Type u_3
inst✝² : Ring R
I : Ideal R
inst✝¹ : Finite ↥I
inst✝ : Finite (R ⧸ I)
⊢ Ideal R

Tactic:
constructor <;> assumption

Goal state after:
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hmax : ⊥.IsMaximal
⊢ IsField R

Tactic:
by_contra hf

Goal state after:
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hmax : ⊥.IsMaximal
hf : ¬IsField R
⊢ False
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case inr
R : Type u_5
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ ¬IsField R ↔ ¬IsSimpleOrder (Ideal R)

Tactic:
Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top

Goal state after:
case inr
R : Type u_5
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ (∃ I, ⊥ < I ∧ I < ⊤) ↔ ¬IsSimpleOrder (Ideal R)
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter β
m : α → β
⊢ (comap m f).NeBot ↔ ∀ t ∈ f, ∃ a, m a ∈ t

Tactic:
by
  simp only [← forall_mem_nonempty_iff_neBot, mem_comap, forall_exists_index, and_imp]
  exact ⟨fun h t t_in => h (m ⁻¹' t) t t_in Subset.rfl, fun h s t ht hst => (h t ht).imp hst⟩

Goal state after:
Module: Mathlib.Order.Filter.Tendsto

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
a : Filter α
b : Filter β
c : Filter γ
hfg : Tendsto (g ∘ f) a c
hg : comap g c ≤ b
⊢ Tendsto f a b

Tactic:
tendsto_iff_comap

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
a : Filter α
b : Filter β
c : Filter γ
hfg : a ≤ comap (g ∘ f) c
hg : comap g c ≤ b
⊢ a ≤ comap f b
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
f : Filter α
s : Set α
h : ∀ U ∈ f, (U ∩ sᶜ).Nonempty
hs : s ∈ f
⊢ False

Tactic:
simpa [Set.not_nonempty_empty] using h s hs

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

Goal state before:
pp: α : Type u
f : Filter α
s : Set α
h : f ⊓ 𝓟 sᶜ = ⊥
⊢ s ∈ f

Tactic:
by
  rwa [inf_principal_eq_bot, compl_compl] at h

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
s : β → Set α
S : Set β
h : DirectedOn (s ⁻¹'o fun x1 x2 ↦ x1 ⊇ x2) S
ne : S.Nonempty
t : Set α
⊢ t ∈ ⨅ i ∈ S, 𝓟 (s i) ↔ ∃ i ∈ S, s i ⊆ t

Tactic:
refine mem_biInf_of_directed ?_ ne

Goal state after:
α : Type u_1
β : Type u_2
s : β → Set α
S : Set β
h : DirectedOn (s ⁻¹'o fun x1 x2 ↦ x1 ⊇ x2) S
ne : S.Nonempty
t : Set α
⊢ DirectedOn ((fun i ↦ 𝓟 (s i)) ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) S
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
p : α → Prop
q : Prop
⊢ (∃ᶠ (x : α) in f, p x ∧ q) ↔ (∃ᶠ (x : α) in f, p x) ∧ q

Tactic:
simp only [@and_comm _ q, frequently_and_distrib_left]

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

Goal state before:
pp: α : Type u
p : α → Prop
⊢ (∃ᶠ (x : α) in ⊤, p x) ↔ ∃ x, p x

Tactic:
by simp [Filter.Frequently]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
e : α ≃ β
inst✝¹ : Mul β
inst✝ : IsRightCancelMul β
⊢ IsRightCancelMul α

Tactic:
let := e.mul; exact e.injective.isRightCancelMul _ fun _ _ ↦ e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
hgi : ∀ (c : β), b ≤ c → ∃ x, f x = c ∧ ∀ (a : α), f a ≤ c ↔ a ≤ x
⊢ map f atTop = atTop

Tactic:
have : Nonempty α := (hgi b le_rfl).nonempty

Goal state after:
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
hgi : ∀ (c : β), b ≤ c → ∃ x, f x = c ∧ ∀ (a : α), f a ≤ c ↔ a ≤ x
this : Nonempty α
⊢ map f atTop = atTop
Module: Mathlib.RingTheory.Noetherian.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := ⋯
H : WellFoundedGT { N // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ : ∀ x ∈ {N' | ↑N' ≤ N}, ¬⟨N₀, h₁⟩ < x
h₃ : ¬N ≤ N₀
x : M
hx₁ : x ∈ N
hx₂ : x ∉ N₀
⊢ x ∈ N₀

Tactic:
rw [eq_of_le_of_not_lt (le_sup_right : N₀ ≤ _) (h₂
      ⟨_, Submodule.FG.sup ⟨{x}, by rw [Finset.coe_singleton]⟩ h₁⟩ <|
      sup_le ((Submodule.span_singleton_le_iff_mem _ _).mpr hx₁) e)]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ : ∀ x ∈ {N' | ↑N' ≤ N}, ¬⟨N₀, h₁⟩ < x
h₃ : ¬N ≤ N₀
x : M
hx₁ : x ∈ N
hx₂ : x ∉ N₀
⊢ x ∈ R ∙ x ⊔ N₀
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ ≤ a₂ → a₁ • b ≤ a₂ • b
b : β
hb : 0 ≤ b
a₁ a₂ : α
h : a₁ ≤ a₂
⊢ a₁ • b ≤ a₂ • b

Tactic:
obtain hb | hb := hb.eq_or_lt
    · simp [← hb]
    · exact h₀ _ hb _ _ h

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case h
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ r x ((enum r) ⟨succ ((typein r).toRelEmbedding x), ⋯⟩)

Tactic:
convert! enum_lt_enum.mpr _

Goal state after:
case e'_1
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ x = (enum r) ?h.convert_4

case h.convert_4
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ ↑(Iio (type r))

case h.convert_6
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ ?h.convert_4 < ⟨succ ((typein r).toRelEmbedding x), ⋯⟩
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case refine_1
c : Cardinal.{v}
a : Ordinal.{v}
left✝ : a < c.ord
ha : Ordinal.lift.{u, v} a < Ordinal.lift.{u, v} c.ord
⊢ a.card < c

Tactic:
← lt_ord,

Goal state after:
case refine_1
c : Cardinal.{v}
a : Ordinal.{v}
left✝ : a < c.ord
ha : Ordinal.lift.{u, v} a < Ordinal.lift.{u, v} c.ord
⊢ a < c.ord
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
x : α
h : (#α).ord = type r
⊢ ((typein r).toRelEmbedding x).card < #α

Tactic:
← lt_ord,

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
x : α
h : (#α).ord = type r
⊢ (typein r).toRelEmbedding x < (#α).ord
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℵ₀ ≤ o.card ↔ ω ≤ o

Tactic:
rw [← ord_le, ord_aleph0]

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

Goal state before:
pp: a : Cardinal.{u}
b : Ordinal.{max u v}
h : b < (succ (Cardinal.lift.{v, u} a)).ord
⊢ b ∈ range lift.{v, u}

Tactic:
← lift_succ,

Goal state after:
a : Cardinal.{u}
b : Ordinal.{max u v}
h : b < (Cardinal.lift.{v, u} (succ a)).ord
⊢ b ∈ range lift.{v, u}
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case cons.cons
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
b : α
bs : List α
hm : (b :: bs).SortedGT
hmltl : Lex (fun x1 x2 ↦ x1 < x2) (b :: bs) (a :: as)
i : α
hi : i ∈ b :: bs
⊢ i ≤ a

Tactic:
cases hi with
      | head as => exact List.head_le_of_lt hmltl
      | tail b hi => exact le_of_lt (lt_of_lt_of_le (List.rel_of_pairwise_cons hm.pairwise hi)
          (List.head_le_of_lt hmltl))

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: x y z : Ordinal.{u_4}
⊢ (x * y + z) % x = z % x

Tactic:
by
  rcases eq_or_ne x 0 with rfl | hx
  · simp
  · rwa [mod_def, mul_add_div, mul_add, ← sub_sub, add_sub_cancel, mod_def]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
b c : Ordinal.{u_4}
hb₀ : b ≠ 0
q : Ordinal.{u_4}
hq : q < c
r : Ordinal.{u_4}
hr : r < b
⊢ b * (q + 1) ≤ b * c

Tactic:
add_one_le_iff.2 hq

Goal state after:
case inr
b c : Ordinal.{u_4}
hb₀ : b ≠ 0
q : Ordinal.{u_4}
hq : q < c
r : Ordinal.{u_4}
hr : r < b
⊢ b * c ≤ b * c
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inl
o : Ordinal.{u_4}
ho : o < ω
⊢ (∃ n, o = ↑n) ∨ ω ≤ o

Tactic:
exact Or.inl <| lt_omega0.1 ho

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
hx : x ≠ 0
⊢ x < b ^ succ (log b x)

Tactic:
· rw [lt_opow_iff_log_lt hb hx, lt_succ_iff]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case a
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ o / 2 ^ log 2 o ≤ 1

pp: case a
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ 1 ≤ o / 2 ^ log 2 o

Tactic:
· simpa [← one_add_one_eq_two] using div_opow_log_lt o one_lt_two

Goal state after:
case a
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ 1 ≤ o / 2 ^ log 2 o
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case zero
⊢ preOmega ↑0 = ↑0

Tactic:
exact preOmega_zero

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

Goal state before:
pp: x : Ordinal.{u_1}
⊢ x ∈ range ⇑preOmega ↔ x.IsInitial

Tactic:
rw [range_preOmega, mem_ofPred]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a : Ordinal.{u_1}
ha : IsPrincipal (fun x1 x2 ↦ x1 + x2) a
b : Ordinal.{u_1}
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (a ^ b)

Tactic:
rcases isPrincipal_add_iff_zero_or_omega0_opow.1 ha with (rfl | ⟨c, rfl⟩)

Goal state after:
case inl
b : Ordinal.{u_1}
ha : IsPrincipal (fun x1 x2 ↦ x1 + x2) 0
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (0 ^ b)

case inr
b c : Ordinal.{u_1}
ha : IsPrincipal (fun x1 x2 ↦ x1 + x2) ((fun x ↦ ω ^ x) c)
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) ((fun x ↦ ω ^ x) c ^ b)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : ℵ₀ ≤ b
⊢ b ≤ a * b

Tactic:
by simpa only [one_mul] using mul_le_mul_left (one_le_aleph0.trans ha) b

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

Goal state before:
pp: case inl
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b
ha : a ≠ 0
hb : b ≠ 0
ha' : ℵ₀ ≤ a
⊢ a * b = max a b

pp: case inr
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b
ha : a ≠ 0
hb : b ≠ 0
hb' : ℵ₀ ≤ b
⊢ a * b = max a b

Tactic:
· exact mul_eq_max_of_aleph0_le_left ha' hb

Goal state after:
case inr
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b
ha : a ≠ 0
hb : b ≠ 0
hb' : ℵ₀ ≤ b
⊢ a * b = max a b
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.cof = 0 ↔ o = 0

Tactic:
rw [← cof_toType, cof_eq_zero_iff, isEmpty_toType_iff]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inl
a b : Ordinal.{u}
hb : b < ω
c0 : 0 < 0
ha : a < ω ^ 0
⊢ a * b < ω ^ 0

Tactic:
exact (lt_irrefl _).elim c0

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

Goal state before:
pp: case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
⊢ lift.{v, u} (2 ^ #ι) ≤ prod fun i ↦ lift.{u, v} (c i)

Tactic:
· rw [← prod_const', lift_prod]
    refine prod_le_prod _ _ fun i => ?_
    rw [lift_two, ← lift_two.{u, v}, lift_le]
    exact h₁ i

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

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c ^< ℵ₀ ≤ max c ℵ₀

Tactic:
rcases le_or_gt ℵ₀ c with h | h

Goal state after:
case inl
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ^< ℵ₀ ≤ max c ℵ₀

case inr
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ c ^< ℵ₀ ≤ max c ℵ₀
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inr
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
⊢ #{ s // #↑s < (#α).ord.cof } = #α

Tactic:
rcases exists_ord_eq α with ⟨r, wo, hr⟩

Goal state after:
case inr
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
⊢ #{ s // #↑s < (#α).ord.cof } = #α
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (ℵ_ o).IsSingular ↔ IsSuccLimit o ∧ o.cof < ℵ_ o

Tactic:
obtain rfl | ⟨a, rfl⟩ | ho := zero_or_succ_or_isSuccLimit o

Goal state after:
case inl
⊢ (ℵ_ 0).IsSingular ↔ IsSuccLimit 0 ∧ Ordinal.cof 0 < ℵ_ 0

case inr.inl
a : Ordinal.{u_1}
⊢ (ℵ_ (succ a)).IsSingular ↔ IsSuccLimit (succ a) ∧ (succ a).cof < ℵ_ (succ a)

case inr.inr
o : Ordinal.{u_1}
ho : IsSuccLimit o
⊢ (ℵ_ o).IsSingular ↔ IsSuccLimit o ∧ o.cof < ℵ_ o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
val✝ : Fintype α
⊢ ∃ g, ∀ (x : ↑s), g ↑x = f x

pp: case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
val✝ : Infinite α
⊢ ∃ g, ∀ (x : ↑s), g ↑x = f x

Tactic:
· exact extend_function_finite f h

Goal state after:
case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
val✝ : Infinite α
⊢ ∃ g, ∀ (x : ↑s), g ↑x = f x
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
x : Π₀ (i : ι), β₁ i
s : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
i : ι
h : x i = 0
⊢ f i (x i) = 0

Tactic:
by
      rw [← hf i, ← h]

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case h.cons.inl
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)
i : ι
s : Multiset ι
ih : ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0), p { toFun := f, support' := Trunc.mk ⟨s, H⟩ }
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 : p (erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })
H3 :
  single i ({ toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } i) +
      erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } =
    { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ }
h : f i = 0
⊢ p (erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })

Tactic:
exact H2

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
i : ι
φ : β i →+ γ
⊢ ↑(sumAddHom (Pi.single i φ)) = ↑(φ.comp (evalAddMonoidHom i))

Tactic:
by
    convert! sumZeroHom_piSingle i φ.toZeroHom using 1
    rw [DFinsupp.sumAddHom_toZeroHom]
    conv_lhs =>
      enter [1, i]
      rw [Pi.apply_single (fun i (x : β i →+ γ) => x.toZeroHom) (fun _ => rfl)]

Goal state after: