mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: case mem_mul_mem
R : Type u_1
inst✝ : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
hy : y ∈ I
z : R
hz : z ∈ J
⊢ f (J.toCotangent ⟨y * z, ⋯⟩) = 0

Tactic:
rcases Submodule.mem_map.mp (le (f.mem_range_self (J.toCotangent ⟨z, hz⟩))) with ⟨w, hw, eqz⟩
      have mem_bot := Ideal.mul_mem_mul hy (Submodule.mem_comap.mp hw)
      simp only [← mul_assoc, sq, Submodule.bot_mul, Submodule.mem_bot] at mem_bot
      have eq0 : y • w = 0 := SetCoe.ext mem_bot
      have : ⟨y * z, Ideal.mul_le_right (Submodule.mul_mem_mul hy hz)⟩ = y • (⟨z, hz⟩ : J) := rfl
      rw [this, map_smul, map_smul, ← eqz, ← map_smul, eq0, map_zero]

Goal state after:
Module: Mathlib.RingTheory.WittVector.Compare

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n m : ℕ
hm : n ≤ m
⊢ (zmodEquivTrunc p n).symm.toRingHom.comp (truncate hm) =
    (ZMod.castHom ⋯ (ZMod (p ^ n))).comp (zmodEquivTrunc p m).symm.toRingHom

Tactic:
ext; apply commutes_symm'

Goal state after:
Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing

Goal state before:
pp: p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a b : 𝕎 k
hab : ↑p = a * b
h : a * b = 0
⊢ False

Tactic:
h

Goal state after:
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a b : 𝕎 k
hab : ↑p = 0
h : a * b = 0
⊢ False
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case inr.inr
α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
val✝ : NoTopOrder α
⊢ IsClub (⋂₀ s)

Tactic:
cases one_lt_cof.not_ge hα

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
hf : Monotone f
this : Nonempty α
hα : IsCofinal (range (rangeSplitting f))
⊢ lift.{v, u} (cof α) ≤ lift.{u, v} #β

Tactic:
classical let := hf.isChain_range.linearOrder

Goal state after:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
hf : Monotone f
this✝ : Nonempty α
hα : IsCofinal (range (rangeSplitting f))
this : LinearOrder ↑(range f) := ⋯.linearOrder
⊢ lift.{v, u} (cof α) ≤ lift.{u, v} #β
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
⊢ T = ⊥ → [] ∉ T

Tactic:
rintro rfl; simp

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

Goal state before:
pp: o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih : ∀ y < o₁ + o₂, ∀ {o₁ o₂ : Ordinal.{u_1}}, AddCommute o₁ o₂ → o₁ + o₂ = y → ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := o₂ - o₁
hsub : o₁ + o₃ = o₂
hcomm' : AddCommute o₁ o₃
⊢ o₁ + o₃ < o₁ + o₂

Tactic:
simpa [hsub, hcomm.eq] using h₁.pos

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
⊢ a ≤ b → lfpApprox f x a ≤ lfpApprox f x b

Tactic:
h

Goal state after:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
h : a ≤ b
⊢ lfpApprox f x a ≤ lfpApprox f x b
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
hb : b ≤ 1
ho : o ≠ 0
⊢ CNF b o = [(0, o)]

Tactic:
rcases Order.le_one_iff.1 hb with (rfl | rfl)
  exacts [CNF.zero_left ho, CNF.one_left ho]

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f g : α →o α
⊢ f ≤ g → lfpApprox f ≤ lfpApprox g

Tactic:
h

Goal state after:
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
⊢ lfpApprox f ≤ lfpApprox g
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x₁ x₂ : α
⊢ x₁ ≤ x₂ → lfpApprox f x₁ ≤ lfpApprox f x₂

Tactic:
h

Goal state after:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x₁ x₂ : α
h : x₁ ≤ x₂
⊢ lfpApprox f x₁ ≤ lfpApprox f x₂
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case refine_1.inl
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
h : lfpApprox f x 0 = x
⊢ f x = x ∨ 0 = 0

pp: case refine_1.inr
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u}
h : lfpApprox f x o = x
ho : o ≠ 0
⊢ f x = x ∨ o = 0

Tactic:
· exact Or.inr rfl

Goal state after:
case refine_1.inr
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u}
h : lfpApprox f x o = x
ho : o ≠ 0
⊢ f x = x ∨ o = 0
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b ∧
      a ≠ b
⊢ ∃ a < (succ #α).ord, ∃ b < (succ #α).ord, a ≠ b ∧ lfpApprox f x a = lfpApprox f x b

Tactic:
let ⟨a, b, h_fab, h_nab⟩ := h_ninj

Goal state after:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ ∃ a < (succ #α).ord, ∃ b < (succ #α).ord, a ≠ b ∧ lfpApprox f x a = lfpApprox f x b
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b : Ordinal.{u_1}
⊢ coeff b 0 = 0

Tactic:
by
  ext e
  exact coeff_zero_apply b e

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f g : α →o α
⊢ f ≤ g → gfpApprox f ≤ gfpApprox g

Tactic:
h

Goal state after:
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
⊢ gfpApprox f ≤ gfpApprox g
Module: Mathlib.Topology.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : IsNormal f
b : β
⊢ IsOpen (f ⁻¹' Ioi b)

Tactic:
← isClosed_compl_iff,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : IsNormal f
b : β
⊢ IsClosed (f ⁻¹' Ioi b)ᶜ
Module: Mathlib.Topology.Order.IsNormal

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
h : (f ⁻¹' Iic b).Nonempty
this✝ : Nonempty α
this : Nonempty β
⊢ IsClosed (f ⁻¹' Iic b)

Tactic:
hf.preimage_Iic h (ha ▸ bddAbove_Iio)

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
h : (f ⁻¹' Iic b).Nonempty
this✝ : Nonempty α
this : Nonempty β
⊢ IsClosed (Iic (sSup (f ⁻¹' Iic b)))
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case eq
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₂ = Ordering.eq
h : Ordering.eq.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂

Tactic:
obtain rfl := eq_of_cmp_eq h₁

Goal state after:
case eq
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h : Ordering.eq.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂)) = Ordering.eq
h₁ : e₁.cmp e₁ = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case eq.eq
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
h₁ : e₁.cmp e₁ = Ordering.eq
h₂ : ¬↑n₁ < ↑n₂ ∧ ¬↑n₂ < ↑n₁
h : Ordering.eq.then (Ordering.eq.then (a₁.cmp a₁)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₁.oadd n₂ a₁

Tactic:
not_lt,

Goal state after:
case eq.eq
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
h₁ : e₁.cmp e₁ = Ordering.eq
h₂ : ↑n₂ ≤ ↑n₁ ∧ ¬↑n₂ < ↑n₁
h : Ordering.eq.then (Ordering.eq.then (a₁.cmp a₁)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₁.oadd n₂ a₁
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case eq.eq
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
h₁ : e₁.cmp e₁ = Ordering.eq
h₂ : ↑n₂ ≤ ↑n₁ ∧ ¬↑n₂ < ↑n₁
h : Ordering.eq.then (Ordering.eq.then (a₁.cmp a₁)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₁.oadd n₂ a₁

Tactic:
not_lt,

Goal state after:
case eq.eq
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
h₁ : e₁.cmp e₁ = Ordering.eq
h₂ : ↑n₂ ≤ ↑n₁ ∧ ↑n₁ ≤ ↑n₂
h : Ordering.eq.then (Ordering.eq.then (a₁.cmp a₁)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₁.oadd n₂ a₁
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case single_add.h
b : Ordinal.{u_1}
f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
e₁ x : Ordinal.{u_1}
f₁ : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf₁ : ∀ c ∈ f₁.support, c < e₁
hx : x ≠ 0
IH : (∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁) → eval b (f₁ + f₂) = eval b f₁ + eval b f₂
h : ∀ e₁_1 ∈ (single e₁ x + f₁).support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁_1
⊢ ∀ e' ∈ (f₁ + f₂).support, e' ≤ e₁

Tactic:
intro e₂ he₂

Goal state after:
case single_add.h
b : Ordinal.{u_1}
f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
e₁ x : Ordinal.{u_1}
f₁ : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf₁ : ∀ c ∈ f₁.support, c < e₁
hx : x ≠ 0
IH : (∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁) → eval b (f₁ + f₂) = eval b f₁ + eval b f₂
h : ∀ e₁_1 ∈ (single e₁ x + f₁).support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁_1
e₂ : Ordinal.{u_1}
he₂ : e₂ ∈ (f₁ + f₂).support
⊢ e₂ ≤ e₁
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd'
o : ONote
b : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝² : ONote
eb✝ b✝ : Ordinal.{0}
a✝¹ : e✝.NFBelow eb✝
a✝ : a✝².NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝ : e✝.repr < ω ^ eb✝
IH : a✝².repr < ω ^ e✝.repr
⊢ (e✝.oadd n✝ a✝²).repr < ω ^ b✝

Tactic:
repr

Goal state after:
case oadd'
o : ONote
b : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝² : ONote
eb✝ b✝ : Ordinal.{0}
a✝¹ : e✝.NFBelow eb✝
a✝ : a✝².NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝ : e✝.repr < ω ^ eb✝
IH : a✝².repr < ω ^ e✝.repr
⊢ ω ^ e✝.repr * ↑↑n✝ + a✝².repr < ω ^ b✝
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o : ONote
b : Ordinal.{0}
h : o.NFBelow b
⊢ o.repr < ω ^ b

Tactic:
induction h with

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

Goal state before:
pp: o : ONote
b₁ b₂ : Ordinal.{0}
bb : b₁ ≤ b₂
h : o.NFBelow b₁
⊢ o.NFBelow b₂

Tactic:
induction h with

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

Goal state before:
pp: case h
x✝ y z x : ZFSet.{u}
a : PSet.{u}
f : a.Type → ↥(mk a) := fun i ↦ ⟨mk (a.Func i), ⋯⟩
a✝ : PSet.{u}
i : a.Type
h : a✝.Equiv (a.Func i)
⊢ ∃ a_1, f a_1 = ⟨⟦a✝⟧, ⋯⟩

Tactic:
exact ⟨i, Subtype.coe_injective (Quotient.sound h.symm)⟩

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o₁ o₂ : Ordinal.{u}
⊢ o₁ < o₂ → veblenWith f o₁ a ≤ veblenWith f o₂ a

Tactic:
h

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o₁ o₂ : Ordinal.{u}
h : o₁ < o₂
⊢ veblenWith f o₁ a ≤ veblenWith f o₂ a
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o₁ o₂ : Ordinal.{u}
⊢ o₁ < o₂ → (fun x ↦ veblenWith f x 0) o₁ < (fun x ↦ veblenWith f x 0) o₂

Tactic:
h

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o₁ o₂ : Ordinal.{u}
h : o₁ < o₂
⊢ (fun x ↦ veblenWith f x 0) o₁ < (fun x ↦ veblenWith f x 0) o₂
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case mp
α✝¹ : Type u_1
A✝¹ : α✝¹ → PSet.{u_1}
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
αβ : ∀ (a : α✝¹), ∃ b, (A✝¹ a).Equiv (A✝ b)
βα : ∀ (b : α✝), ∃ a, (A✝¹ a).Equiv (A✝ b)
x✝ : Ordinal.{u_1}
a : α✝¹
⊢ succ (A✝¹ a).rank = x✝ → ∃ y, succ (A✝ y).rank = x✝

Tactic:
h

Goal state after:
case mp
α✝¹ : Type u_1
A✝¹ : α✝¹ → PSet.{u_1}
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
αβ : ∀ (a : α✝¹), ∃ b, (A✝¹ a).Equiv (A✝ b)
βα : ∀ (b : α✝), ∃ a, (A✝¹ a).Equiv (A✝ b)
x✝ : Ordinal.{u_1}
a : α✝¹
h : succ (A✝¹ a).rank = x✝
⊢ ∃ y, succ (A✝ y).rank = x✝
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case mpr
α✝¹ : Type u_1
A✝¹ : α✝¹ → PSet.{u_1}
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
αβ : ∀ (a : α✝¹), ∃ b, (A✝¹ a).Equiv (A✝ b)
βα : ∀ (b : α✝), ∃ a, (A✝¹ a).Equiv (A✝ b)
x✝ : Ordinal.{u_1}
a : α✝
⊢ succ (A✝ a).rank = x✝ → ∃ y, succ (A✝¹ y).rank = x✝

Tactic:
h

Goal state after:
case mpr
α✝¹ : Type u_1
A✝¹ : α✝¹ → PSet.{u_1}
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
αβ : ∀ (a : α✝¹), ∃ b, (A✝¹ a).Equiv (A✝ b)
βα : ∀ (b : α✝), ∃ a, (A✝¹ a).Equiv (A✝ b)
x✝ : Ordinal.{u_1}
a : α✝
h : succ (A✝ a).rank = x✝
⊢ ∃ y, succ (A✝¹ y).rank = x✝
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case a.inr
o a : Ordinal.{u}
h : a < veblen o a
ho : 0 < o
⊢ ω ^ veblen o a ∈ range (veblen o)

Tactic:
rw [← veblen_zero_apply, veblen_veblen_of_lt ho]
      simp

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

Goal state before:
pp: p : ZFSet.{u} → Prop
x y : ZFSet.{u}
IH : ∀ y_1 ∈ y, Hereditarily p y_1 → p ∅
⊢ Hereditarily p y → p ∅

Tactic:
h

Goal state after:
p : ZFSet.{u} → Prop
x y : ZFSet.{u}
IH : ∀ y_1 ∈ y, Hereditarily p y_1 → p ∅
h : Hereditarily p y
⊢ p ∅
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case a.h₁
x y x✝ : ZFSet.{u_1}
⊢ x✝ ∈ x → x✝ ∈ x ∪ y

Tactic:
h

Goal state after:
case a.h₁
x y x✝ : ZFSet.{u_1}
h : x✝ ∈ x
⊢ x✝ ∈ x ∪ y
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case h₂
x y x✝ : ZFSet.{u_1}
⊢ x✝ ∈ y → x✝ ∈ x ∪ y

Tactic:
h

Goal state after:
case h₂
x y x✝ : ZFSet.{u_1}
h : x✝ ∈ y
⊢ x✝ ∈ x ∪ y
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o : Ordinal.{u}
h : o.invVeblen₁ = o
ho : ¬o = 0
| veblen o.invVeblen₁ o.invVeblen₂

Tactic:
h

Goal state after:
o : Ordinal.{u}
h : o.invVeblen₁ = o
ho : ¬o = 0
| veblen o o.invVeblen₂
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case mp
o : Ordinal.{u}
h : o.invVeblen₁ = o
ho : ¬o = 0
⊢ veblen o 0 ≤ o

Tactic:
conv_rhs => rw [← veblen_eq_of_lt_invVeblen₁ (h.trans_ne ho).bot_lt, bot_eq_zero,
      veblen_zero_apply, ← veblen_invVeblen₁_invVeblen₂, h]

Goal state after:
case mp
o : Ordinal.{u}
h : o.invVeblen₁ = o
ho : ¬o = 0
⊢ veblen o 0 ≤ veblen o o.invVeblen₂
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: x y : ZFSet.{u}
h : ↑x = ↑y
z : ZFSet.{u}
⊢ ↑x z ↔ ↑y z

Tactic:
h

Goal state after:
x y : ZFSet.{u}
h : ↑x = ↑y
z : ZFSet.{u}
⊢ ↑y z ↔ ↑y z
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: case mpr
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o
y : ZFSet.{u_1}
hy : y ∈ x
this : y.rank < o
⊢ ∃ a < o, y ⊆ V_ a

Tactic:
exact ⟨_, this, subset_vonNeumann.2 le_rfl⟩

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

Goal state before:
pp: e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
⊢ (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).NFBelow (e₁.repr + b₂)

Tactic:
have IH := oadd_mul_nfBelow h₁ h₂.snd
    by_cases e0 : e₂ = 0 <;> simp only [e0, oadd_mul, ↓reduceIte]
    · apply NFBelow.oadd h₁.fst h₁.snd
      grw [← h₂.lt.pos, add_zero]
    · have := h₁.fst
      have := h₂.fst
      apply NFBelow.oadd
      · infer_instance
      · rwa [repr_add]
      · grw [repr_add, h₂.lt]

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

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a ≤ b → a.toZFSet ⊆ b.toZFSet

Tactic:
h

Goal state after:
a b : Ordinal.{u_1}
h : a ≤ b
⊢ a.toZFSet ⊆ b.toZFSet
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg.e_a.e_a
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * ↑↑n₁ = ω ^ e₁.repr * ↑↑n₁
e0 : ¬e₂ = 0
this✝¹ : e₁.NF
this✝ : e₂.NF
this : ¬e₂.repr = repr 0
⊢ ω ^ e₁.repr * ω ^ e₂.repr = ω ^ e₁.repr * (↑↑n₁ * ω ^ e₂.repr)

Tactic:
mul_omega0_dvd (Nat.cast_pos'.2 n₁.pos) (natCast_lt_omega0 _)

Goal state after:
case neg.e_a.e_a
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * ↑↑n₁ = ω ^ e₁.repr * ↑↑n₁
e0 : ¬e₂ = 0
this✝¹ : e₁.NF
this✝ : e₂.NF
this : ¬e₂.repr = repr 0
⊢ ω ^ e₁.repr * ω ^ e₂.repr = ω ^ e₁.repr * ω ^ e₂.repr

case neg.e_a.e_a
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * ↑↑n₁ = ω ^ e₁.repr * ↑↑n₁
e0 : ¬e₂ = 0
this✝¹ : e₁.NF
this✝ : e₂.NF
this : ¬e₂.repr = repr 0
⊢ ω ∣ ω ^ e₂.repr
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r s t : R
h : r + s = t
⊢ (algebraMap R A) (r + s) = (algebraMap R A) t

Tactic:
h

Goal state after:
R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r s t : R
h : r + s = t
⊢ (algebraMap R A) t = (algebraMap R A) t
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
r t : R
h : -r = t
⊢ (algebraMap R A) (-r) = (algebraMap R A) t

Tactic:
h

Goal state after:
R : Type u_3
A : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
r t : R
h : -r = t
⊢ (algebraMap R A) t = (algebraMap R A) t
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r s : R
b : ℕ
h : r ^ b = s
⊢ (algebraMap R A) (r ^ b) = (algebraMap R A) s

Tactic:
h

Goal state after:
R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r s : R
b : ℕ
h : r ^ b = s
⊢ (algebraMap R A) s = (algebraMap R A) s
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝² : Semifield R
inst✝¹ : Semifield A
inst✝ : Algebra R A
r s : R
h : r⁻¹ = s
⊢ (algebraMap R A) r⁻¹ = (algebraMap R A) s

Tactic:
h

Goal state after:
R : Type u_3
A : Type u_4
inst✝² : Semifield R
inst✝¹ : Semifield A
inst✝ : Algebra R A
r s : R
h : r⁻¹ = s
⊢ (algebraMap R A) s = (algebraMap R A) s
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r : R
h : IsNat r 1
⊢ IsNat ((algebraMap R A) (r + 0)) 1

Tactic:
simp only [h.out, Nat.cast_one, add_zero, map_one]
  exact ⟨by simp⟩

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

Goal state before:
pp: e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this : ω ^ e.repr ≤ (e.oadd n a).repr
⊢ (ω ^ e.repr * ↑↑n + a.repr) ^ ω = (ω ^ e.repr) ^ ω

Tactic:
repr

Goal state after:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
⊢ (ω ^ e.repr * ↑↑n + a.repr) ^ ω = (ω ^ e.repr) ^ ω
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
b : Ordinal.{0}
l : b < ω
this : (e.oadd n a).repr < ω ^ succ e.repr
⊢ (ω ^ e.repr * ↑↑n + a.repr) ^ b ≤ (ω ^ e.repr) ^ ω

Tactic:
repr

Goal state after:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr
⊢ (ω ^ e.repr * ↑↑n + a.repr) ^ b ≤ (ω ^ e.repr) ^ ω
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
b : β
h : F b = none
this :
  match F b with
  | none => ⋯.choose b = nil
  | some (a, c, b') => ⋯.choose b = Seq.cons a (op c (⋯.choose b'))
⊢ gcorec F op b = nil

Tactic:
simpa [h] using! this

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
b : β
a : α
c : γ
b' : β
h : F b = some (a, c, b')
this :
  match F b with
  | none => ⋯.choose b = nil
  | some (a, c, b') => ⋯.choose b = Seq.cons a (op c (⋯.choose b'))
⊢ gcorec F op b = Seq.cons a (op c (gcorec F op b'))

Tactic:
simpa [h] using! this

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
x y : Stream'.Seq α
h : dist (op (Seq.cons hd x)) (op (Seq.cons hd y)) ≤ dist (Seq.cons hd x) (Seq.cons hd y)
⊢ dist (op (Seq.cons hd x)).tail (op (Seq.cons hd y)).tail ≤ dist x y

Tactic:
rwa [dist_cons_cons, dist_eq_half_of_head, mul_le_mul_iff_right₀ (by norm_num)] at h
  grw [dist_le_one x y, mul_one] at h
  obtain (⟨hx, hy⟩ | ⟨_, _, _, hx, hy⟩) := dist_le_half_iff.mp h <;> simp [hx, hy]

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic

Goal state before:
pp: c : ℝ
basis : Basis
h_basis : WellFormedBasis basis
⊢ (const basis c).Approximates

Tactic:
by
  cases basis with
  | nil => simp
  | cons basis_hd basis_tl =>
    simp only [const, Multiseries.const]
    apply (const_approximates h_basis.tail).cons _ (by simp)
    exact Majorized.const <| h_basis.tendsto_atTop (by simp)

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
op : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
motive : (Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl) → Prop
h_base : motive op
h_step :
  ∀ (op : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl),
    motive op →
      ∃ T,
        ∀ (s : Multiseries basis_hd basis_tl),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (exp, coef, opf, op') => (exp, coef, ↑op' (↑opf s.tail)))
              (T s.head)
⊢ FriendlyOperation op

Tactic:
refine Seq.FriendlyOperation.coind_comp_friend_right motive h_base (fun op h_op ↦ ?_)

Goal state after:
basis_hd : ℝ → ℝ
basis_tl : Basis
op✝ : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
motive : (Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl) → Prop
h_base : motive op✝
h_step :
  ∀ (op : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl),
    motive op →
      ∃ T,
        ∀ (s : Multiseries basis_hd basis_tl),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (exp, coef, opf, op') => (exp, coef, ↑op' (↑opf s.tail)))
              (T s.head)
op : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl) → Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h_op : motive op
⊢ ∃ T,
    ∀ (s : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)),
      (op s).destruct =
        Option.map
          (fun x ↦
            match x with
            | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
          (T s.head)