mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, x ^ n ∈ f.range
hker : RingHom.ker f ≤ nilradical R
⊢ IsHomeomorph (comap f)

Tactic:
have h1 : Function.Injective (comap f) := by
    intro q q' hqq'
    ext x
    obtain ⟨n, hn, y, hy⟩ := H x
    rw [← q.2.pow_mem_iff_mem _ hn, ← q'.2.pow_mem_iff_mem _ hn, ← hy]
    rw [PrimeSpectrum.ext_iff, SetLike.ext_iff] at hqq'
    apply hqq'
  have hint : f.kerLift.IsIntegral := fun x ↦
    have ⟨n, hn, y, hy⟩ := H x
    let _ := f.kerLift.toAlgebra
    IsIntegral.of_pow hn (hy ▸ f.kerLift.isIntegralElem_map (x := ⟦y⟧))
  have hbij : Function.Bijective (comap f) :=
    ⟨h1, (comap_quotientMk_bijective_of_le_nilradical hker).2.comp <|
      hint.comap_surjective f.kerLift_injective⟩
  refine ⟨continuous_comap f, ?_, h1, hbij.2⟩
  rw [isTopologicalBasis_basic_opens.isOpenMap_iff]
  rintro - ⟨s, rfl⟩
  obtain ⟨n, hn, r, hr⟩ := H s
  have : (comap f) '' (basicOpen s) = basicOpen r :=
    (Set.eq_preimage_iff_image_eq hbij).mp <| by rw [← basicOpen_pow _ n hn, ← hr]; rfl
  exact this ▸ isOpen_basicOpen

Goal state after:
Module: Mathlib.RingTheory.Valuation.Quotient

Goal state before:
pp: case a
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
⊢ v.supp ≤ Ideal.comap (Ideal.Quotient.mk J) (v.onQuot hJ).supp

Tactic:
intro x

Goal state after:
case a
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
x : R
⊢ x ∈ v.supp → x ∈ Ideal.comap (Ideal.Quotient.mk J) (v.onQuot hJ).supp
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: 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))
this : ∀ {x : R} (h : x ∈ I * J), f (J.toCotangent ⟨x, ⋯⟩) = 0
⊢ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J)) ≤ f.ker

Tactic:
intro x

Goal state after:
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))
this : ∀ {x : R} (h : x ∈ I * J), f (J.toCotangent ⟨x, ⋯⟩) = 0
x : J.Cotangent
⊢ x ∈ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J)) → x ∈ f.ker
Module: Mathlib.RingTheory.Valuation.Extension

Goal state before:
pp: A : Type u_2
inst✝⁴ : Ring A
K : Type u_5
inst✝³ : Field K
inst✝² : Algebra K A
ΓA : Type u_7
ΓK : Type u_8
inst✝¹ : LinearOrderedCommGroupWithZero ΓK
inst✝ : LinearOrderedCommGroupWithZero ΓA
vK : Valuation K ΓK
vA : Valuation A ΓA
h : Subring.comap (algebraMap K A) vA.integer = vK.integer
⊢ ∀ {x : K}, vK x ≤ 1 ↔ (comap (algebraMap K A) vA) x ≤ 1

Tactic:
intro x

Goal state after:
A : Type u_2
inst✝⁴ : Ring A
K : Type u_5
inst✝³ : Field K
inst✝² : Algebra K A
ΓA : Type u_7
ΓK : Type u_8
inst✝¹ : LinearOrderedCommGroupWithZero ΓK
inst✝ : LinearOrderedCommGroupWithZero ΓA
vK : Valuation K ΓK
vA : Valuation A ΓA
h : Subring.comap (algebraMap K A) vA.integer = vK.integer
x : K
⊢ vK x ≤ 1 ↔ (comap (algebraMap K A) vA) x ≤ 1
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ x ∈ range n, (↑p ^ x * wittMul p x ^ p ^ (n - x)).vars ⊆ univ ×ˢ range n

Tactic:
intro x

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
⊢ x ∈ range n → (↑p ^ x * wittMul p x ^ p ^ (n - x)).vars ⊆ univ ×ˢ range n
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ x ∈ range (n + 1),
    ((rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))).vars ⊆ univ ×ˢ range (n + 1)

Tactic:
intro x

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
⊢ x ∈ range (n + 1) →
    ((rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))).vars ⊆ univ ×ˢ range (n + 1)
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ x ∈ range (n + 1),
    ((rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))).vars ⊆ univ ×ˢ range (n + 1)

Tactic:
intro x

Goal state after:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
⊢ x ∈ range (n + 1) →
    ((rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))).vars ⊆ univ ×ˢ range (n + 1)
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
    ↑p ^ (n + 1) * X (0, n + 1) *
      ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))

Tactic:
2,

Goal state after:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| ↑p ^ (n + 1) * X (0, n + 1) *
    ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
      ↑p ^ (n + 1) * X (0, n + 1) *
        (∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
          ↑p ^ (n + 1) * X (1, n + 1)) +
    ↑p ^ (n + 1) * X (1, n + 1) *
      ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))

Tactic:
2,

Goal state after:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| ↑p ^ (n + 1) * X (1, n + 1) *
    ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑↑(univ ×ˢ range (n + 1)) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
⊢ TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k

Tactic:
intro x

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑↑(univ ×ˢ range (n + 1)) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
x : TruncatedWittVector p (n + 1) k
⊢ TruncatedWittVector p (n + 1) k → k
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑↑(univ ×ˢ range (n + 1)) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k := ⋯
⊢ ∀ (x y : 𝕎 k),
    f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
      peval (polyOfInterest p n) ![fun i ↦ x.coeff i, fun i ↦ y.coeff i]

Tactic:
intro x

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑↑(univ ×ˢ range (n + 1)) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k :=
  fun x y ↦
    f₀ fun a ↦
      Subtype.casesOn a fun a ha ↦
        Function.uncurry ![x, y]
          (let S := {a | a.2 = n ∨ a.2 < n};
          have ha' := ⋯;
          (a.1, ⟨a.2, ⋯⟩))
x : 𝕎 k
⊢ ∀ (y : 𝕎 k),
    f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
      peval (polyOfInterest p n) ![fun i ↦ x.coeff i, fun i ↦ y.coeff i]
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k
hf :
  ∀ (x y : 𝕎 k),
    f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
      (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)
⊢ ∀ (x y : 𝕎 k),
    (x * y).coeff (n + 1) =
      x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) + y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) +
        f (truncateFun (n + 1) x) (truncateFun (n + 1) y)

Tactic:
intro x

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k
hf :
  ∀ (x y : 𝕎 k),
    f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
      (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)
x : 𝕎 k
⊢ ∀ (y : 𝕎 k),
    (x * y).coeff (n + 1) =
      x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) + y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) +
        f (truncateFun (n + 1) x) (truncateFun (n + 1) y)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
ι : Type u
f : ι → Set α
hα : cof α ≠ ℵ₀
hι : lift.{v, u} #ι < lift.{u, v} (cof α)
hf : ∀ (i : ι), IsClub (f i)
⊢ #↑(range f) < cof α

Tactic:
rw [← Cardinal.lift_lt]

Goal state after:
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
ι : Type u
f : ι → Set α
hα : cof α ≠ ℵ₀
hι : lift.{v, u} #ι < lift.{u, v} (cof α)
hf : ∀ (i : ι), IsClub (f i)
⊢ lift.{?u.38, v} #↑(range f) < lift.{?u.38, v} (cof α)
Module: Mathlib.SetTheory.Cardinal.NatCount

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ ↑(count p n) ≤ {k | p k}.encard

Tactic:
by
  simp only [Set.encard, ENat.card, Set.coe_ofPred, Cardinal.natCast_le_toENat]
  exact Nat.count_le_cardinal n

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
ι : Type u
f : ι → Set α
hα : cof α ≠ ℵ₀
hι : lift.{v, u} #ι < lift.{u, v} (cof α)
⊢ #↑(range f) < cof α

Tactic:
rw [← Cardinal.lift_lt]

Goal state after:
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
ι : Type u
f : ι → Set α
hα : cof α ≠ ℵ₀
hι : lift.{v, u} #ι < lift.{u, v} (cof α)
⊢ lift.{?u.37, v} #↑(range f) < lift.{?u.37, v} (cof α)
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
a : α
l : Lists α
h : atom a ~ l
⊢ atom a = l

Tactic:
by cases h; rfl

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
b : Bool
l : Lists' α b
⊢ 0 < sizeOf l

Tactic:
cases l

Goal state after:
case atom
α : Type u_1
a✝ : α
⊢ 0 < sizeOf (Lists'.atom a✝)

case nil
α : Type u_1
⊢ 0 < sizeOf Lists'.nil

case cons'
α : Type u_1
b✝ : Bool
a✝¹ : Lists' α b✝
a✝ : Lists' α true
⊢ 0 < sizeOf (a✝¹.cons' a✝)
Module: Mathlib.SetTheory.ZFC.Cardinal

Goal state before:
pp: x : ZFSet.{u}
⊢ x.powerset.card = 2 ^ x.card

Tactic:
by
  rw [← lift_inj.{u, u + 1}]
  simpa [← cardinalMk_coe_sort] using mk_congr (powersetEquiv x)

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

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

Tactic:
revert h'

Goal state after:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
⊢ (a + o).NFBelow b → (e.addAux n (a + o)).NFBelow b
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
i : α
⊢ f i ⊆ ⋃ (i : α), f i

Tactic:
intro x

Goal state after:
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
i : α
x : ZFSet.{u}
⊢ x ∈ f i → x ∈ ⋃ (i : α), f i
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: ⊢ Function.Injective2 pair

Tactic:
intro x

Goal state after:
x : ZFSet.{u_1}
⊢ ∀ ⦃a₂ b₁ b₂ : ZFSet.{u_1}⦄, x.pair b₁ = a₂.pair b₂ → x = a₂ ∧ b₁ = b₂
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case a
x : PSet.{u_1}
⊢ x.powerset.rank ≤ succ x.rank

Tactic:
simp_rw [rank_le_iff, mem_powerset, lt_succ_iff]
    intro
    exact rank_mono

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

Goal state before:
pp: case mp
x y : ZFSet.{u}
⊢ ∀ (a₁ b₁ : ZFSet.{u}),
    (∀ (a₂ b₂ : ZFSet.{u}),
        Sym2.GameAdd (fun x1 x2 ↦ x1 ∈ x2) s(a₂, b₂) s(a₁, b₁) →
          a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂) →
      a₁.IsOrdinal → b₁.IsOrdinal → a₁ ⊆ b₁ → a₁ = b₁ ∨ a₁ ∈ b₁

Tactic:
intro x

Goal state after:
case mp
x✝ y x : ZFSet.{u}
⊢ ∀ (b₁ : ZFSet.{u}),
    (∀ (a₂ b₂ : ZFSet.{u}),
        Sym2.GameAdd (fun x1 x2 ↦ x1 ∈ x2) s(a₂, b₂) s(x, b₁) →
          a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂) →
      x.IsOrdinal → b₁.IsOrdinal → x ⊆ b₁ → x = b₁ ∨ x ∈ b₁
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
mn : ↑n₁ - ↑n₂ = 0
en : ¬n₁ = n₂
⊢ (if n₁ = n₂ then a₁.sub a₂ else 0).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr

Tactic:
simp only [en, ite_false]
          exact
            (Ordinal.sub_eq_zero_iff_le.2 <|
                le_of_lt <|
                  oadd_lt_oadd_2 h₁ <|
                    lt_of_le_of_ne (tsub_eq_zero_iff_le.1 mn) (mt PNat.eq en)).symm

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

Goal state before:
pp: case inl
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : Std.Trichotomous (Subrel (fun x1 x2 ↦ x1 ∈ x2) fun x_1 ↦ x_1 ∈ x)
y z w : ↥x
hyz : Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) y z
hzw : Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) z w
hyw : Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) y w
⊢ Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) y w

pp: case inr.inl
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : Std.Trichotomous (Subrel (fun x1 x2 ↦ x1 ∈ x2) fun x_1 ↦ x_1 ∈ x)
y z : ↥x
hyz : Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) y z
hzw : Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) z y
⊢ Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) y y

pp: case inr.inr
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : Std.Trichotomous (Subrel (fun x1 x2 ↦ x1 ∈ x2) fun x_1 ↦ x_1 ∈ x)
y z w : ↥x
hyz : Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) y z
hzw : Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) z w
hwy : Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) w y
⊢ Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) y w

Tactic:
· exact hyw

Goal state after:
case inr.inl
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : Std.Trichotomous (Subrel (fun x1 x2 ↦ x1 ∈ x2) fun x_1 ↦ x_1 ∈ x)
y z : ↥x
hyz : Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) y z
hzw : Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) z y
⊢ Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) y y

case inr.inr
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : Std.Trichotomous (Subrel (fun x1 x2 ↦ x1 ∈ x2) fun x_1 ↦ x_1 ∈ x)
y z w : ↥x
hyz : Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) y z
hzw : Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) z w
hwy : Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) w y
⊢ Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) y w
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case refine_2
x : ZFSet.{u}
⊢ x ∈ Set.range toZFSet → x.IsOrdinal

Tactic:
rintro ⟨a, rfl⟩
    exact isOrdinal_toZFSet a

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

Goal state before:
pp: n : ℕ
o : ONote
⊢ o.mulNat n = o * ↑n

Tactic:
cases o <;> cases n <;> rfl

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

Goal state before:
pp: e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
m : ℕ
⊢ (e.opowAux a0 a 0 m).repr = ω ^ e.repr * (opowAux 0 a0 a 0 m).repr

Tactic:
by cases m <;> simp [opowAux]

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

Goal state before:
pp: α : Type u_1
hd : α
⊢ ∀ (s t : Stream'.Seq α), 2⁻¹ * dist s t ≤ dist s t

Tactic:
intro x

Goal state after:
α : Type u_1
hd : α
x : Stream'.Seq α
⊢ ∀ (t : Stream'.Seq α), 2⁻¹ * dist x t ≤ dist x t
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
h : ∀ (s t : Stream'.Seq α), dist (op s) (op t) ≤ dist s t
⊢ ∀ (s t : Stream'.Seq α), dist (op (Seq.cons hd s)).tail (op (Seq.cons hd t)).tail ≤ dist s t

Tactic:
intro x

Goal state after:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
h : ∀ (s t : Stream'.Seq α), dist (op s) (op t) ≤ dist s t
x : Stream'.Seq α
⊢ ∀ (t : Stream'.Seq α), dist (op (Seq.cons hd x)).tail (op (Seq.cons hd t)).tail ≤ dist x t
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s : Stream'.Seq α
⊢ (op s).destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, op') => (hd, ↑op' s.tail))
      (match s.head with
      | none =>
        match (op nil).destruct with
        | none => none
        | some (t_hd, t_tl) => some (t_hd, ⟨fun x ↦ t_tl, ⋯⟩)
      | some s_hd =>
        match (op (Seq.cons s_hd nil)).destruct with
        | none => none
        | some (t_hd, snd) => some (t_hd, ⟨fun s_tl ↦ (op (Seq.cons s_hd s_tl)).tail, ⋯⟩))

Tactic:
cases s with
  | nil =>
    generalize op nil = t
    cases t <;> simp
  | cons s_hd s_tl =>
    simp only [Seq.tail_cons, Seq.head_cons]
    generalize ht0 : op (.cons s_hd nil) = t0 at *
    generalize ht : op (.cons s_hd s_tl) = t at *
    have : t0.head = t.head := by
      rw [← ht0, ← ht, FriendlyOperation.op_cons_head_eq h]
    cases t0 with
    | nil =>
      cases t with
      | nil => simp
      | cons => simp at this
    | cons =>
      cases t with
      | nil => simp at this
      | cons => simp_all

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

Goal state before:
pp: m1 m2 : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length m1 = List.length m2
⊢ ∀ (x : ℝ), (∀ f ∈ basis, 0 < f x) → (m1.mul m2).toFun basis x = (m1.toFun basis * m2.toFun basis) x

Tactic:
intro x

Goal state after:
m1 m2 : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length m1 = List.length m2
x : ℝ
⊢ (∀ f ∈ basis, 0 < f x) → (m1.mul m2).toFun basis x = (m1.toFun basis * m2.toFun basis) x
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.cons
exp : ℝ
exps : List ℝ
ih :
  ∀ {basis : Basis},
    WellFormedBasis basis →
      (fun a ↦ (List.zipWith (fun exp b ↦ b a ^ exp) (List.map (fun x ↦ -x) exps) basis).prod) =ᶠ[atTop] fun a ↦
        (List.zipWith (fun exp b ↦ b a ^ exp) exps basis).prod⁻¹
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ ∀ (x : ℝ),
    0 < basis_hd x ∧
        (fun a ↦ (List.zipWith (fun exp b ↦ b a ^ exp) (List.map (fun x ↦ -x) exps) basis_tl).prod) x =
          (fun a ↦ (List.zipWith (fun exp b ↦ b a ^ exp) exps basis_tl).prod⁻¹) x →
      (fun a ↦ (List.zipWith (fun exp b ↦ b a ^ exp) (List.map (fun x ↦ -x) (exp :: exps)) (basis_hd :: basis_tl)).prod)
          x =
        (fun a ↦ (List.zipWith (fun exp b ↦ b a ^ exp) (exp :: exps) (basis_hd :: basis_tl)).prod⁻¹) x

Tactic:
intro x

Goal state after:
case cons.cons
exp : ℝ
exps : List ℝ
ih :
  ∀ {basis : Basis},
    WellFormedBasis basis →
      (fun a ↦ (List.zipWith (fun exp b ↦ b a ^ exp) (List.map (fun x ↦ -x) exps) basis).prod) =ᶠ[atTop] fun a ↦
        (List.zipWith (fun exp b ↦ b a ^ exp) exps basis).prod⁻¹
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
x : ℝ
⊢ 0 < basis_hd x ∧
      (fun a ↦ (List.zipWith (fun exp b ↦ b a ^ exp) (List.map (fun x ↦ -x) exps) basis_tl).prod) x =
        (fun a ↦ (List.zipWith (fun exp b ↦ b a ^ exp) exps basis_tl).prod⁻¹) x →
    (fun a ↦ (List.zipWith (fun exp b ↦ b a ^ exp) (List.map (fun x ↦ -x) (exp :: exps)) (basis_hd :: basis_tl)).prod)
        x =
      (fun a ↦ (List.zipWith (fun exp b ↦ b a ^ exp) (exp :: exps) (basis_hd :: basis_tl)).prod⁻¹) x
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: m : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
⊢ ∀ (x : ℝ), (∀ f ∈ basis, 0 < f x) → 0 < m.toFun basis x

Tactic:
intro x

Goal state after:
m : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
x : ℝ
⊢ (∀ f ∈ basis, 0 < f x) → 0 < m.toFun basis x
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: m : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
⊢ ∀ (x : ℝ), (∀ f ∈ basis, 0 < f x) → (log ∘ m.toFun basis) x = m.toLogFun basis x

Tactic:
intro x

Goal state after:
m : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
x : ℝ
⊢ (∀ f ∈ basis, 0 < f x) → (log ∘ m.toFun basis) x = m.toLogFun basis x
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case seq.h_Pairwise
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_coef : ∀ x ∈ ms.seq, x.2.Sorted
h_Pairwise : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) ms.seq
⊢ Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk ms.seq 0).seq

Tactic:
· simpa using h_Pairwise

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

Goal state before:
pp: exps_hd : ℝ
exps_tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_nonzero : 0 < exps_hd
h_equiv : log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) ~[atTop] exps_hd • log ∘ basis_hd
h_log : Tendsto (log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop atTop
⊢ ∀ (x : ℝ),
    0 < toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) x →
      (rexp ∘ log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) x =
        toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) x

Tactic:
intro x

Goal state after:
exps_hd : ℝ
exps_tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_nonzero : 0 < exps_hd
h_equiv : log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) ~[atTop] exps_hd • log ∘ basis_hd
h_log : Tendsto (log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop atTop
x : ℝ
⊢ 0 < toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) x →
    (rexp ∘ log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) x =
      toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) x
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case seq.h_Pairwise
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_coef : ∀ x ∈ (mk ms.seq 0).seq, x.2.Sorted
h_Pairwise : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk ms.seq 0).seq
⊢ Seq.Pairwise (fun x1 x2 ↦ x1 > x2) ms.seq

Tactic:
· simpa using h_Pairwise

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

Goal state before:
pp: exps_hd : ℝ
exps_tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_nonzero : exps_hd < 0
h_equiv : log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) ~[atTop] exps_hd • log ∘ basis_hd
h_log : Tendsto (log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop atBot
hmono : Tendsto (rexp ∘ log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop (𝓝 0)
⊢ ∀ (x : ℝ),
    0 < toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) x →
      (rexp ∘ log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) x =
        toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) x

Tactic:
intro x

Goal state after:
exps_hd : ℝ
exps_tl : UnitMonomial
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_nonzero : exps_hd < 0
h_equiv : log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) ~[atTop] exps_hd • log ∘ basis_hd
h_log : Tendsto (log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop atBot
hmono : Tendsto (rexp ∘ log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop (𝓝 0)
x : ℝ
⊢ 0 < toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) x →
    (rexp ∘ log ∘ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) x =
      toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) x