mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
⊢ ∀ (x : M ⧸ p), x ∈ p.mkQ.range

Tactic:
rintro ⟨x⟩

Goal state after:
case mk
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
x✝ : M ⧸ p
x : M
⊢ Quot.mk (⇑p.quotientRel) x ∈ p.mkQ.range
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R✝ : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι✝ : Type x
ι' : Type x'
inst✝¹⁴ : Semiring R✝
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R✝ M₂
inst✝¹¹ : AddCommMonoid M₃
inst✝¹⁰ : Module R✝ M₃
φ : ι✝ → Type i
inst✝⁹ : (i : ι✝) → AddCommMonoid (φ i)
inst✝⁸ : (i : ι✝) → Module R✝ (φ i)
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : SMul R M
inst✝³ : SMul R N
inst✝² : Module S M
inst✝¹ : Module S N
inst✝ : CompatibleSMul M N R S
f : M →ₗ[S] ι → N
r : R
m : M
i : ι
⊢ f (r • m) i = (r • f m) i

Tactic:
apply ((LinearMap.proj i).comp f).map_smul_of_tower

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M × M₂ →ₗ[R] M₃
⊢ (f ∘ₗ inl R M M₂).coprod (f ∘ₗ inr R M M₂) = f

Tactic:
rw [← comp_coprod, coprod_inl_inr, comp_id]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
H : p ≤ p'
⊢ factor H ∘ₗ p.mkQ = p'.mkQ

Tactic:
ext x
  rw [LinearMap.comp_apply, factor_mk]

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R✝ : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹⁶ : Semiring R✝
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst✝¹⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝¹⁴ : (i : ι) → Module R✝ (φ i)
inst✝¹³ : (i : ι) → AddCommMonoid (ψ i)
inst✝¹² : (i : ι) → Module R✝ (ψ i)
inst✝¹¹ : (i : ι) → AddCommMonoid (χ i)
inst✝¹⁰ : (i : ι) → Module R✝ (χ i)
S : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : Module S M✝
inst✝³ : SMulCommClass R✝ S M✝
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ∀ (x y : α ⊕ β → M),
    (Equiv.sumArrowEquivProdArrow α β M).toFun (x + y) =
      (Equiv.sumArrowEquivProdArrow α β M).toFun x + (Equiv.sumArrowEquivProdArrow α β M).toFun y

Tactic:
by
      intro f g
      ext <;> rfl

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 b c : M
⊢ (fun x ↦ a + x) '' Ioo b c = Ioo (a + b) (a + c)

Tactic:
simp only [add_comm a, image_add_const_Ioo]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
hab : a < b
f : ℕ → M
⊢ ∏ k ∈ Ico a b, f k = f a * ∏ k ∈ Ico (a + 1) b, f k

Tactic:
by
  have ha : a ∉ Ico (a + 1) b := by simp
  rw [← prod_insert ha, Finset.insert_Ico_add_one_left_eq_Ico hab]

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

Goal state before:
pp: case succ
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
h_eq : pred^[m] i0 = pred^[n.succ] i0
⊢ toZ i0 (pred^[n + 1] i0) = -↑(n + 1)

Tactic:
by_cases hmn : m = n + 1

Goal state after:
case pos
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
h_eq : pred^[m] i0 = pred^[n.succ] i0
hmn : m = n + 1
⊢ toZ i0 (pred^[n + 1] i0) = -↑(n + 1)

case neg
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
hn : ¬IsMin (pred^[n + 1] i0)
this : pred^[n.succ] i0 < i0
m : ℕ := (-toZ i0 (pred^[n.succ] i0)).toNat
h_eq : pred^[m] i0 = pred^[n.succ] i0
hmn : ¬m = n + 1
⊢ toZ i0 (pred^[n + 1] i0) = -↑(n + 1)
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case succ
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
n✝ : ℕ
⊢ ∏ x ∈ Ico 0 (n✝ + 1), f (n✝ - x) = ∏ x ∈ Ico 0 (n✝ + 1), f x

Tactic:
rw [prod_Ico_reflect _ _ le_rfl]

Goal state after:
case succ
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
n✝ : ℕ
⊢ ∏ j ∈ Ico (n✝ + 1 - (n✝ + 1)) (n✝ + 1 - 0), f j = ∏ x ∈ Ico 0 (n✝ + 1), f x
Module: Mathlib.Data.List.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ (0, n + 1) :: (Nat.succ 0, n) :: map ((fun i ↦ (i, n + 1 - i)) ∘ Nat.succ ∘ Nat.succ) (range n) =
    (0, n + 1) :: (Nat.succ 0, n) :: map (Prod.map Nat.succ id ∘ (fun i ↦ (i, n - i)) ∘ Nat.succ) (range n)

Tactic:
apply congr rfl (congr rfl _)

Goal state after:
n : ℕ
⊢ map ((fun i ↦ (i, n + 1 - i)) ∘ Nat.succ ∘ Nat.succ) (range n) =
    map (Prod.map Nat.succ id ∘ (fun i ↦ (i, n - i)) ∘ Nat.succ) (range n)
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝ : Fintype ι
f : ι → α
hι : Nonempty ι
R : ι ≃ Fin (card ι) := equivFin ι
⊢ ∃ g ≤ f, univ.sup g = univ.sup f ∧ Pairwise (Disjoint on g)

Tactic:
let f' : Fin _ → α := f ∘ R.symm

Goal state after:
case inr
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝ : Fintype ι
f : ι → α
hι : Nonempty ι
R : ι ≃ Fin (card ι) := equivFin ι
f' : Fin (card ι) → α := f ∘ ⇑R.symm
⊢ ∃ g ≤ f, univ.sup g = univ.sup f ∧ Pairwise (Disjoint on g)
Module: Mathlib.RingTheory.Ideal.Defs

Goal state before:
pp: α : Type u
a : α
inst✝ : CommSemiring α
I : Ideal α
ha : a ∈ I
c : α
⊢ a * c ∈ I

Tactic:
exact I.mul_mem_right _ ha

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝ : Ring R
I J : Ideal R
a b x y : R
⊢ ∀ (a : R ⧸ ⊤), a = default

Tactic:
rintro ⟨x⟩

Goal state after:
case mk
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝ : Ring R
I J : Ideal R
a b x✝ y : R
a✝ : R ⧸ ⊤
x : R
⊢ Quot.mk (⇑(Submodule.quotientRel ⊤)) x = default
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case h
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : c ≤ n
this : (s.card + 1) * n + 1 - c = s.card * n + 1 + (n - c)
⊢ a ^ c * s.sum ^ ((s.card + 1) * n + 1 - c) * ↑(((s.card + 1) * n + 1).choose c) ∈
    span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset

Tactic:
rw [this, pow_add]

Goal state after:
case h
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : c ≤ n
this : (s.card + 1) * n + 1 - c = s.card * n + 1 + (n - c)
⊢ a ^ c * (s.sum ^ (s.card * n + 1) * s.sum ^ (n - c)) * ↑(((s.card + 1) * n + 1).choose c) ∈
    span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
Module: Mathlib.Algebra.Module.Submodule.IterateMapComap

Goal state before:
pp: R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
h : map f K ≤ map i K
n : ℕ
ih : map f (f.iterateMapComap i n K) ≤ map i (f.iterateMapComap i n K)
⊢ map i (comap f (map f (f.iterateMapComap i n K))) ≤ map i (comap f (map i ((fun K ↦ comap f (map i K))^[n] K)))

Tactic:
gcongr; exact ih

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.IterateMapComap

Goal state before:
pp: case zero.succ
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
hf : Surjective ⇑f
hi : Injective ⇑i
heq : f.iterateMapComap i 0 K ≠ f.iterateMapComap i (0 + 1) K
m : ℕ
ih : f.iterateMapComap i m K ≠ f.iterateMapComap i (m + 1) K
⊢ ((fun K ↦ comap f (map i K)) ∘ (fun K ↦ comap f (map i K))^[m]) K ≠
    ((fun K ↦ comap f (map i K)) ∘ (fun K ↦ comap f (map i K))^[m + 1]) K

Tactic:
exact fun H ↦ ih (map_injective_of_injective hi (comap_injective_of_surjective hf H))

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a b : R
inst✝ : I.IsTwoSided
⊢ Function.LeftInverse (fun x ↦ (Quotient.mk (pi fun x ↦ I)) fun x_1 ↦ Quotient.out (x x_1)) fun x ↦
    Quotient.liftOn' x (fun f i ↦ (Quotient.mk I) (f i)) ⋯

Tactic:
rintro ⟨x⟩

Goal state after:
case mk
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a b : R
inst✝ : I.IsTwoSided
x✝ : (ι → R) ⧸ pi fun x ↦ I
x : ι → R
⊢ (fun x ↦ (Quotient.mk (pi fun x ↦ I)) fun x_1 ↦ Quotient.out (x x_1))
      ((fun x ↦ Quotient.liftOn' x (fun f i ↦ (Quotient.mk I) (f i)) ⋯)
        (Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) x)) =
    Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) x
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_5
p : α → Submodule R M
x : α →₀ M
hx : x ∈ submodule p
⊢ x ∈ ⨆ i, map (lsingle i) (p i)

Tactic:
← Finsupp.sum_single x

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_5
p : α → Submodule R M
x : α →₀ M
hx : x ∈ submodule p
⊢ x.sum single ∈ ⨆ i, map (lsingle i) (p i)
Module: Mathlib.Order.Filter.AtTopBot.Defs

Goal state before:
pp: case a
α : Type u_3
inst✝ : Preorder α
s : Set α
hs : ∀ (x : α), ∃ y ∈ s, x ≤ y
y : α
⊢ Ici y ∈ (generate (range Ici)).sets

Tactic:
exact mem_generate_of_mem ⟨y, rfl⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : α → β
s : Set α
⊢ kernMap m (𝓟 s) = 𝓟 (kernImage m s)

Tactic:
refine eq_of_forall_le_iff (fun g ↦ ?_)

Goal state after:
α : Type u_1
β : Type u_2
m : α → β
s : Set α
g : Filter β
⊢ g ≤ kernMap m (𝓟 s) ↔ g ≤ 𝓟 (kernImage m s)
Module: Mathlib.Order.Filter.Tendsto

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
φ : α → β
ψ : β → α
eq : ψ ∘ φ = id
hφ : Tendsto φ f g
hψ : Tendsto ψ g f
⊢ comap φ (comap ψ f) ≤ f

Tactic:
rw [comap_comap, eq, comap_id]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
f : β → α
hl : l.HasBasis p s
t : Set β
⊢ (∃ i, p i ∧ s i ⊆ {y | ∀ ⦃x : β⦄, f x = y → x ∈ t}) ↔ ∃ i, p i ∧ f ⁻¹' s i ⊆ t

Tactic:
refine exists_congr (fun i => Iff.rfl.and ?_)

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
f : β → α
hl : l.HasBasis p s
t : Set β
i : ι
⊢ s i ⊆ {y | ∀ ⦃x : β⦄, f x = y → x ∈ t} ↔ f ⁻¹' s i ⊆ t
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Semigroup β
⊢ Semigroup α

Tactic:
by
  let mul := e.mul
  apply e.injective.semigroup _; intros; exact e.apply_symm_apply _

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

Goal state before:
pp: R : Type u_1
M : Type u_2
G : Type u_3
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : IsRegular r
m₁ m₂ : M
hm : r • m₁ - r • m₂ = 0
⊢ m₁ = m₂

Tactic:
← smul_sub

Goal state after:
R : Type u_1
M : Type u_2
G : Type u_3
inst✝⁴ : Semiring R
inst✝³ : IsDomain R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
r : R
hr : IsRegular r
m₁ m₂ : M
hm : r • (m₁ - m₂) = 0
⊢ m₁ = m₂
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : PosSMulMono α β
inst✝ : SMulPosMono α β
hab : 0 < a • b
ha : 0 < a
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
refine Or.inl ⟨ha, lt_imp_lt_of_le_imp_le (fun hb ↦ ?_) hab⟩

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : PosSMulMono α β
inst✝ : SMulPosMono α β
hab : 0 < a • b
ha : 0 < a
hb : b ≤ 0
⊢ a • b ≤ 0
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
ha : a ∉ s
ha' : IsSuccLimit a
c : α
hc : c < a
d : α
hd : d ∈ s
hcd : c < d
hda : d ≤ a
hb : ∀ ⦃x : α⦄, x ∈ s → f x ≤ b
⊢ f c ≤ b

Tactic:
exact (hf.strictMono hcd).le.trans (hb hd)

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case convert_2
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ Nonempty ↑(Iio a)

pp: case convert_4
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ BddAbove (range Subtype.val)

Tactic:
· exact ⟨⊥, ha.bot_lt⟩

Goal state after:
case convert_4
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ BddAbove (range Subtype.val)
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case convert_4
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ BddAbove (range Subtype.val)

Tactic:
use a
    rintro _ ⟨⟨x, hx⟩, rfl⟩
    exact hx.le

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case isSuccLimit
α : Type u_1
β : Type u_2
f : α → β
inst✝³ : LinearOrder α
inst✝² : WellFoundedLT α
inst✝¹ : SuccOrder α
inst✝ : LinearOrder β
hs : ∀ (a : α), f a < f (succ a)
hl : ∀ {a : α}, IsSuccLimit a → IsLUB (f '' Iio a) (f a)
a b : α
hb : IsSuccLimit b
IH : ∀ b_1 < b, a < b_1 → f a < f b_1
⊢ a < b → f a < f b

Tactic:
| isSuccLimit b hb IH =>

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

Goal state before:
pp: case mp
α : Type u
β : Type v
e : Nonempty (α ≃ β)
⊢ ∃ c', lift.{v + 1, u} #α = lift.{max u (v + 1), v} c'

Tactic:
exact ⟨#β, lift_mk_eq.{u, _, v + 1}.2 e⟩

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

Goal state before:
pp: α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ ∃ y, r x y

Tactic:
use enum r ⟨succ (typein r x), h _ (typein_lt_type r x)⟩

Goal state after:
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), ⋯⟩)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
⊢ a - b ≤ c ↔ a ≤ b + c

Tactic:
refine ⟨fun h ↦ (le_add_sub a b).trans (by gcongr), fun h ↦ ?_⟩

Goal state after:
a b c : Ordinal.{u_4}
h : a ≤ b + c
⊢ a - b ≤ c
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{u}
inst✝ : Small.{u, u_3} ι
h : iSup f = 0
i : ι
⊢ f i ≤ iSup f

Tactic:
exact Ordinal.le_iSup f i

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

Goal state before:
pp: case mpr
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
h : #α ≤ (type s).card
⊢ (#α).ord ≤ type s

Tactic:
obtain ⟨f⟩ := h
    have g := RelEmbedding.preimage f s
    have := RelEmbedding.isWellOrder g
    exact (ord_le_type _).trans g.ordinal_type_le

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

Goal state before:
pp: a : Ordinal.{u_1}
⊢ a ^ 1 = a

Tactic:
simpa using opow_add_one a 0

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

Goal state before:
pp: a b : Ordinal.{u_4}
h : a < b
⊢ a % b = a

Tactic:
simp [mod_def, div_eq_zero_of_lt h]

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

Goal state before:
pp: case neg
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
bdd : ¬BddAbove s
⊢ ¬BddAbove ((fun x ↦ o * x) '' s)

Tactic:
exact fun ⟨u, hu⟩ ↦ bdd ⟨u, fun x hx ↦ (x.le_mul_right ho).trans (hu ⟨x, hx, rfl⟩)⟩

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

Goal state before:
pp: case inl
b c : Ordinal.{u_1}
⊢ 0 ^ (b + c) = 0 ^ b * 0 ^ c

pp: case inr
a b c : Ordinal.{u_1}
ha : 0 < a
⊢ a ^ (b + c) = a ^ b * a ^ c

Tactic:
· obtain rfl | hc := eq_zero_or_pos c; · simp
    have : b + c ≠ 0 := (hc.trans_le le_add_self).ne'
    rw [zero_opow hc.ne', zero_opow, mul_zero]
    exact (hc.trans_le le_add_self).ne'

Goal state after:
case inr
a b c : Ordinal.{u_1}
ha : 0 < a
⊢ a ^ (b + c) = a ^ b * a ^ c
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
b x : Ordinal.{u_1}
hx : x ≠ 0
hb : b ≤ 1
⊢ b ^ log b x ≤ x

Tactic:
rw [← one_le_iff_ne_zero] at hx

Goal state after:
case inl
b x : Ordinal.{u_1}
hx : 1 ≤ x
hb : b ≤ 1
⊢ b ^ log b x ≤ x
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case refine_2
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
h : IsSuccLimit o
⊢ IsLUB (derivFamily f '' Set.Iio o) (⨆ b, derivFamily f ↑b)

Tactic:
Set.image_eq_range

Goal state after:
case refine_2
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
h : IsSuccLimit o
⊢ IsLUB (Set.range fun x ↦ derivFamily f ↑x) (⨆ b, derivFamily f ↑b)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑n
| a - ω ^ log ω a

Tactic:
left

Goal state after:
a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑n
| a
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
ho : ω ^ 2 ≤ o
⊢ preOmega o = ω_ o

Tactic:
rw [← opow_natCast] at ho

Goal state after:
o : Ordinal.{u_1}
ho : ω ^ ↑2 ≤ o
⊢ preOmega o = ω_ o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case refine_1.inl
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0

Tactic:
left

Goal state after:
case refine_1.inl
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case neg
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
hb : b ≠ 0
⊢ b = 1 ∨ a = 0

Tactic:
left

Goal state after:
case neg
a b : Cardinal.{u_1}
h : a * b = a
ha : a < ℵ₀
h2a : ¬a = 0
hb : b ≠ 0
⊢ b = 1
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case neg.inl
b : Cardinal.{u_1}
hb : b ≠ 0
h : 0 * b = 0
h2a : ¬0 = 0
⊢ b = 1

pp: case neg.inr.inl
a : Cardinal.{u_1}
h2a : ¬a = 0
h : a * 0 = a
hb : 0 ≠ 0
⊢ 0 = 1

pp: case neg.inr.inr
n : ℕ
h2a : ¬↑n = 0
m : ℕ
hb : ↑m ≠ 0
h : ↑n * ↑m = ↑n
⊢ ↑m = 1

Tactic:
· contradiction

Goal state after:
case neg.inr.inl
a : Cardinal.{u_1}
h2a : ¬a = 0
h : a * 0 = a
hb : 0 ≠ 0
⊢ 0 = 1

case neg.inr.inr
n : ℕ
h2a : ¬↑n = 0
m : ℕ
hb : ↑m ≠ 0
h : ↑n * ↑m = ↑n
⊢ ↑m = 1
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case neg.inr.inl
a : Cardinal.{u_1}
h2a : ¬a = 0
h : a * 0 = a
hb : 0 ≠ 0
⊢ 0 = 1

pp: case neg.inr.inr
n : ℕ
h2a : ¬↑n = 0
m : ℕ
hb : ↑m ≠ 0
h : ↑n * ↑m = ↑n
⊢ ↑m = 1

Tactic:
· contradiction

Goal state after:
case neg.inr.inr
n : ℕ
h2a : ¬↑n = 0
m : ℕ
hb : ↑m ≠ 0
h : ↑n * ↑m = ↑n
⊢ ↑m = 1
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
h2b✝ : 1 < m
| n < n * m

Tactic:
left

Goal state after:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
h2b✝ : 1 < m
| n
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case refine_2
a b : Cardinal.{u_1}
⊢ (ℵ₀ ≤ a ∧ b ≤ a) ∧ b ≠ 0 ∨ b = 1 ∨ a = 0 → a * b = a

Tactic:
rintro (⟨⟨ha, hab⟩, hb⟩ | rfl | rfl)
    · rw [mul_eq_max_of_aleph0_le_left ha hb, max_eq_left hab]
    all_goals simp

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

Goal state before:
pp: o : Ordinal.{u_1}
ho : ω ^ 2 ≤ o
⊢ preBeth o = ℶ_ o

Tactic:
rw [← opow_natCast] at ho

Goal state after:
o : Ordinal.{u_1}
ho : ω ^ ↑2 ≤ o
⊢ preBeth o = ℶ_ o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case refine_1.inl
a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
⊢ ℵ₀ ≤ a ∧ b ≤ a ∨ b = 0

Tactic:
left

Goal state after:
case refine_1.inl
a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
⊢ ℵ₀ ≤ a ∧ b ≤ a
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
⊢ (⨆ i, f i) + c = ⨆ i, c + f i

Tactic:
Cardinal.ciSup_add f hf

Goal state after:
ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
⊢ ⨆ i, f i + c = ⨆ i, c + f i
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inl
a : Ordinal.{u_1}
hb : 0 ≠ 0
⊢ (a + 0).cof = cof 0

pp: case inr.inl
a c : Ordinal.{u_1}
hb : succ c ≠ 0
⊢ (a + succ c).cof = (succ c).cof

pp: case inr.inr
a b : Ordinal.{u_1}
hb✝ : b ≠ 0
hb : IsSuccLimit b
⊢ (a + b).cof = b.cof

Tactic:
· contradiction

Goal state after:
case inr.inl
a c : Ordinal.{u_1}
hb : succ c ≠ 0
⊢ (a + succ c).cof = (succ c).cof

case inr.inr
a b : Ordinal.{u_1}
hb✝ : b ≠ 0
hb : IsSuccLimit b
⊢ (a + b).cof = b.cof
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
inst✝ : Infinite α
⊢ #(Finset α) = #α

Tactic:
exact Eq.symm <|
    le_antisymm (mk_le_of_injective fun _ _ => Finset.singleton_inj.1) <|
      calc
        #(Finset α) ≤ #(List α) := mk_le_of_surjective List.toFinset_surjective
        _ = #α := mk_list_eq_mk α

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

Goal state before:
pp: case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ⇑(single i xi) = ⇑(single j xj)
hci : (single i xi) i = (single j xj) i
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0

Tactic:
have hcj := congr_fun h_coe j

Goal state after:
case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ⇑(single i xi) = ⇑(single j xj)
hci : (single i xi) i = (single j xj) i
hcj : (single i xi) j = (single j xj) j
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0