harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Kaehler/JacobiZariski.lean
lemma exact_δ_map :
    Function.Exact (δ Q P) (mapBaseChange R S T)

Proof state:
case hF
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
i : P.vars
⊢ (D R T) ((algebraMap S T) (P.val i)) =
    (Q.comp P).toExtension.toKaehler
      ((Extension.CotangentSpace.map (Q.toComp P).toExtensionHom) (P.cotangentSpaceBasis i))

Tactic:
rw [cotangentSpaceBasis_apply]

Result:
case hF
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
i : P.vars
⊢ (D R T) ((algebraMap S T) (P.val i)) =
    (Q.comp P).toExtension.toKaehler
      ((Extension.CotangentSpace.map (Q.toComp P).toExtensionHom) (1 ⊗ₜ[P.Ring] (D R P.Ring) (X i)))

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
⊢ Function.Exact
    ⇑(SnakeLemma.δ' (LinearMap.baseChange T P.toExtension.cotangentComplex) (Q.comp P).toExtension.cotangentComplex
        Q.toExtension.cotangentComplex
        (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))
        (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) ⋯
        (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))
        (Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom) ⋯ ⋯ ⋯ Extension.h1Cotangentι ⋯
        (LinearMap.baseChange T P.toExtension.toKaehler) ⋯ ⋯ ⋯)
    ⇑(mapBaseChange R S T)

Tactic:
apply SnakeLemma.exact_δ_left (π₂ := (Q.comp P).toExtension.toKaehler)
  (hπ₂ := (Q.comp P).toExtension.exact_cotangentComplex_toKaehler)

Result:
case hF
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
⊢ mapBaseChange R S T ∘ₗ LinearMap.baseChange T P.toExtension.toKaehler =
    (Q.comp P).toExtension.toKaehler ∘ₗ
      LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom)

case h
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
⊢ Function.Surjective ⇑(LinearMap.baseChange T P.toExtension.toKaehler)

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
i : P.vars
⊢ (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom) (1 ⊗ₜ[P.Ring] (D R P.Ring) (X i)) = ?m.443979

Tactic:
exact Extension.CotangentSpace.map_tmul ..

Result:
no goals
-- Mathlib/GroupTheory/Perm/Finite.lean
theorem perm_inv_on_of_perm_on_finset {s : Finset α} {f : Perm α} (h : ∀ x ∈ s, f x ∈ s) {y : α}
    (hy : y ∈ s) : f⁻¹ y ∈ s

Proof state:
case h.e'_5
α : Type u
s : Finset α
f : Perm α
h : ∀ x ∈ s, f x ∈ s
y : α
hy : y ∈ s
h0 : ∀ y ∈ s, ∃ x, ∃ (hx : x ∈ s), y = (fun i x => f i) x hx
y2 : α
hy2 : y2 ∈ s
heq : y = (fun i x => f i) y2 hy2
⊢ f⁻¹ ((fun i x => f i) y2 hy2) = y2

Tactic:
simp only [inv_apply_self]

Result:
no goals

Proof state:
case intro.intro
α : Type u
s : Finset α
f : Perm α
h : ∀ x ∈ s, f x ∈ s
y : α
hy : y ∈ s
h0 : ∀ y ∈ s, ∃ x, ∃ (hx : x ∈ s), y = (fun i x => f i) x hx
y2 : α
hy2 : y2 ∈ s
heq : y = (fun i x => f i) y2 hy2
⊢ f⁻¹ y ∈ s

Tactic:
convert hy2

Result:
case h.e'_5
α : Type u
s : Finset α
f : Perm α
h : ∀ x ∈ s, f x ∈ s
y : α
hy : y ∈ s
h0 : ∀ y ∈ s, ∃ x, ∃ (hx : x ∈ s), y = (fun i x => f i) x hx
y2 : α
hy2 : y2 ∈ s
heq : y = (fun i x => f i) y2 hy2
⊢ f⁻¹ y = y2

Proof state:
case h.e'_5
α : Type u
s : Finset α
f : Perm α
h : ∀ x ∈ s, f x ∈ s
y : α
hy : y ∈ s
h0 : ∀ y ∈ s, ∃ x, ∃ (hx : x ∈ s), y = (fun i x => f i) x hx
y2 : α
hy2 : y2 ∈ s
heq : y = (fun i x => f i) y2 hy2
⊢ f⁻¹ y = y2

Tactic:
rw [heq]

Result:
case h.e'_5
α : Type u
s : Finset α
f : Perm α
h : ∀ x ∈ s, f x ∈ s
y : α
hy : y ∈ s
h0 : ∀ y ∈ s, ∃ x, ∃ (hx : x ∈ s), y = (fun i x => f i) x hx
y2 : α
hy2 : y2 ∈ s
heq : y = (fun i x => f i) y2 hy2
⊢ f⁻¹ ((fun i x => f i) y2 hy2) = y2

Proof state:
α : Type u
s : Finset α
f : Perm α
h : ∀ x ∈ s, f x ∈ s
y : α
hy : y ∈ s
⊢ f⁻¹ y ∈ s

Tactic:
have h0 : ∀ y ∈ s, ∃ (x : _) (hx : x ∈ s), y = (fun i (_ : i ∈ s) => f i) x hx :=
  Finset.surj_on_of_inj_on_of_card_le (fun x hx => (fun i _ => f i) x hx) (fun a ha => h a ha)
    (fun a₁ a₂ ha₁ ha₂ heq => (Equiv.apply_eq_iff_eq f).mp heq) rfl.ge

Result:
α : Type u
s : Finset α
f : Perm α
h : ∀ x ∈ s, f x ∈ s
y : α
hy : y ∈ s
h0 : ∀ y ∈ s, ∃ x, ∃ (hx : x ∈ s), y = (fun i x => f i) x hx
⊢ f⁻¹ y ∈ s

Proof state:
α : Type u
s : Finset α
f : Perm α
h : ∀ x ∈ s, f x ∈ s
y : α
hy : y ∈ s
h0 : ∀ y ∈ s, ∃ x, ∃ (hx : x ∈ s), y = (fun i x => f i) x hx
⊢ f⁻¹ y ∈ s

Tactic:
obtain ⟨y2, hy2, heq⟩ := h0 y hy

Result:
case intro.intro
α : Type u
s : Finset α
f : Perm α
h : ∀ x ∈ s, f x ∈ s
y : α
hy : y ∈ s
h0 : ∀ y ∈ s, ∃ x, ∃ (hx : x ∈ s), y = (fun i x => f i) x hx
y2 : α
hy2 : y2 ∈ s
heq : y = (fun i x => f i) y2 hy2
⊢ f⁻¹ y ∈ s
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
/-- The two-variable Jacobi theta function is periodic in `τ` with period 2. -/
lemma jacobiTheta₂_add_right (z τ : ℂ) : jacobiTheta₂ z (τ + 2) = jacobiTheta₂ z τ

Proof state:
z τ : ℂ
n : ℤ
⊢ cexp (↑π * I * ↑n ^ 2 * 2) = 1

Tactic:
rw [(by push_cast; ring : (π * I * n ^ 2 * 2 : ℂ) = (n ^ 2 :) * (2 * π * I)), exp_int_mul,
  exp_two_pi_mul_I, one_zpow]

Result:
no goals

Proof state:
z τ : ℂ
n : ℤ
⊢ ↑π * I * ↑n ^ 2 * 2 = ↑n ^ 2 * (2 * ↑π * I)

Tactic:
ring

Result:
no goals

Proof state:
z τ : ℂ
n : ℤ
⊢ jacobiTheta₂_term n z (τ + 2) = jacobiTheta₂_term n z τ

Tactic:
simp_rw [jacobiTheta₂_term, Complex.exp_add]

Result:
z τ : ℂ
n : ℤ
⊢ cexp (2 * ↑π * I * ↑n * z) * cexp (↑π * I * ↑n ^ 2 * (τ + 2)) =
    cexp (2 * ↑π * I * ↑n * z) * cexp (↑π * I * ↑n ^ 2 * τ)

Proof state:
z τ : ℂ
n : ℤ
this : cexp (↑π * I * ↑n ^ 2 * 2) = 1
⊢ cexp (2 * ↑π * I * ↑n * z) * cexp (↑π * I * ↑n ^ 2 * (τ + 2)) =
    cexp (2 * ↑π * I * ↑n * z) * cexp (↑π * I * ↑n ^ 2 * τ)

Tactic:
rw [mul_add, Complex.exp_add, this, mul_one]

Result:
no goals

Proof state:
z τ : ℂ
n : ℤ
⊢ cexp (2 * ↑π * I * ↑n * z) * cexp (↑π * I * ↑n ^ 2 * (τ + 2)) =
    cexp (2 * ↑π * I * ↑n * z) * cexp (↑π * I * ↑n ^ 2 * τ)

Tactic:
suffices cexp (π * I * n ^ 2 * 2 : ℂ) = 1 by rw [mul_add, Complex.exp_add, this, mul_one]

Result:
z τ : ℂ
n : ℤ
⊢ cexp (↑π * I * ↑n ^ 2 * 2) = 1

Proof state:
z τ : ℂ
n : ℤ
⊢ ↑π * I * ↑n ^ 2 * 2 = ↑(n ^ 2) * (2 * ↑π * I)

Tactic:
push_cast

Result:
z τ : ℂ
n : ℤ
⊢ ↑π * I * ↑n ^ 2 * 2 = ↑n ^ 2 * (2 * ↑π * I)

Proof state:
z τ : ℂ
⊢ jacobiTheta₂ z (τ + 2) = jacobiTheta₂ z τ

Tactic:
refine tsum_congr (fun n ↦ ?_)

Result:
z τ : ℂ
n : ℤ
⊢ jacobiTheta₂_term n z (τ + 2) = jacobiTheta₂_term n z τ
-- Mathlib/MeasureTheory/Measure/Tight.lean
theorem isTightMeasureSet_singleton_of_innerRegularWRT [OpensMeasurableSpace α] [IsFiniteMeasure μ]
    (h : μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) MeasurableSet) :
    IsTightMeasureSet {μ}

Proof state:
case inl.intro.intro.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet
ε : ℝ≥0∞
hε : 0 < ε
r : ℝ≥0∞ := μ univ
hεr : ε < r
hεr' : r - ε < r
K : Set α
left✝ : K ⊆ univ
hKμ : r - ε < μ K
hK_compact : IsCompact K
hK_closed : IsClosed K
⊢ μ univ ≤ ε + μ K

Tactic:
rw [ENNReal.sub_lt_iff_lt_right (ne_top_of_lt hεr) hεr.le, add_comm] at hKμ

Result:
case inl.intro.intro.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet
ε : ℝ≥0∞
hε : 0 < ε
r : ℝ≥0∞ := μ univ
hεr : ε < r
hεr' : r - ε < r
K : Set α
left✝ : K ⊆ univ
hKμ : r < ε + μ K
hK_compact : IsCompact K
hK_closed : IsClosed K
⊢ μ univ ≤ ε + μ K

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsFiniteMeasure μ
h : μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet
ε : ℝ≥0∞
hε : 0 < ε
r : ℝ≥0∞ := μ univ
⊢ ∃ K, IsCompact K ∧ ∀ μ_1 ∈ {μ}, μ_1 Kᶜ ≤ ε

Tactic:
cases lt_or_ge ε r with
| inl hεr =>
  have hεr' : r - ε < r := ENNReal.sub_lt_self (measure_ne_top μ _) (zero_le'.trans_lt hεr).ne'
    hε.ne'
  obtain ⟨K, _, ⟨hK_compact, hK_closed⟩, hKμ⟩ := h .univ (r - ε) hεr'
  refine ⟨K, hK_compact, ?_⟩
  simp only [mem_singleton_iff, forall_eq]
  rw [measure_compl hK_closed.measurableSet (measure_ne_top μ _), tsub_le_iff_right]
  rw [ENNReal.sub_lt_iff_lt_right (ne_top_of_lt hεr) hεr.le, add_comm] at hKμ
  exact hKμ.le
| inr hεr => exact ⟨∅, isCompact_empty, by simpa⟩

Result:
no goals
-- Mathlib/CategoryTheory/Limits/VanKampen.lean
theorem BinaryCofan.isVanKampen_iff (c : BinaryCofan X Y) :
    IsVanKampenColimit c ↔
      ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt)
        (_ : αX ≫ c.inl = c'.inl ≫ f) (_ : αY ≫ c.inr = c'.inr ≫ f),
        Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ c.inl = c'.inl ≫ f →
      αY ≫ c.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)
F' : Discrete WalkingPair ⥤ C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
h : NatTrans.Equifibered α
X' : C := F'.obj { as := WalkingPair.left }
Y' : C := F'.obj { as := WalkingPair.right }
⊢ F' = pair X' Y'

Tactic:
apply Functor.hext

Result:
case h_obj
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ c.inl = c'.inl ≫ f →
      αY ≫ c.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)
F' : Discrete WalkingPair ⥤ C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
h : NatTrans.Equifibered α
X' : C := F'.obj { as := WalkingPair.left }
Y' : C := F'.obj { as := WalkingPair.right }
⊢ ∀ (X : Discrete WalkingPair), F'.obj X = (pair X' Y').obj X

case h_map
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ c.inl = c'.inl ≫ f →
      αY ≫ c.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)
F' : Discrete WalkingPair ⥤ C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
h : NatTrans.Equifibered α
X' : C := F'.obj { as := WalkingPair.left }
Y' : C := F'.obj { as := WalkingPair.right }
⊢ ∀ (X Y : Discrete WalkingPair) (f : X ⟶ Y), HEq (F'.map f) ((pair X' Y').map f)

Proof state:
case h_obj
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
    αX ≫ c.inl = c'.inl ≫ f →
      αY ≫ c.inr = c'.inr ≫ f → (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)
F' : Discrete WalkingPair ⥤ C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
h : NatTrans.Equifibered α
X' : C := F'.obj { as := WalkingPair.left }
Y' : C := F'.obj { as := WalkingPair.right }
⊢ ∀ (X : Discrete WalkingPair), F'.obj X = (pair X' Y').obj X

Tactic:
rintro ⟨⟨⟩⟩ <;> rfl

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleWith.lean
theorem int_sub_iff : LiouvilleWith p (m - x) ↔ LiouvilleWith p x

Proof state:
p x : ℝ
m : ℤ
⊢ LiouvilleWith p (↑m - x) ↔ LiouvilleWith p x

Tactic:
simp [sub_eq_add_neg]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean
/-- All `P_σ` are split epis as composition of such. -/
lemma isSplitEpi_P_σ {x y : SimplexCategoryGenRel} {e : x ⟶ y} (he : P_σ e) : IsSplitEpi e

Proof state:
case comp_of.σ
x y : SimplexCategoryGenRel
e : x ⟶ y
x✝ : SimplexCategoryGenRel
n✝ : ℕ
i✝ : Fin (n✝ + 1)
f✝ : x✝ ⟶ mk (n✝ + 1)
hf✝ : degeneracies.multiplicativeClosure f✝
hf_ih✝ : IsSplitEpi f✝
⊢ IsSplitEpi (f✝ ≫ σ i✝)

Tactic:
infer_instance

Result:
no goals

Proof state:
case id
x y : SimplexCategoryGenRel
e : x ⟶ y
x✝ : SimplexCategoryGenRel
⊢ IsSplitEpi (𝟙 x✝)

Tactic:
infer_instance

Result:
no goals

Proof state:
case of
x✝¹ y : SimplexCategoryGenRel
e : x✝¹ ⟶ y
x✝ y✝ : SimplexCategoryGenRel
x : x✝ ⟶ y✝
hx : degeneracies x
⊢ IsSplitEpi x

Tactic:
cases hx

Result:
case of.σ
x y : SimplexCategoryGenRel
e : x ⟶ y
n✝ : ℕ
i✝ : Fin (n✝ + 1)
⊢ IsSplitEpi (σ i✝)

Proof state:
case comp_of
x y : SimplexCategoryGenRel
e : x ⟶ y
x✝ y✝ z✝ : SimplexCategoryGenRel
f✝ : x✝ ⟶ y✝
g✝ : y✝ ⟶ z✝
hf✝ : degeneracies.multiplicativeClosure f✝
h : degeneracies g✝
hf_ih✝ : IsSplitEpi f✝
⊢ IsSplitEpi (f✝ ≫ g✝)

Tactic:
cases h

Result:
case comp_of.σ
x y : SimplexCategoryGenRel
e : x ⟶ y
x✝ : SimplexCategoryGenRel
n✝ : ℕ
i✝ : Fin (n✝ + 1)
f✝ : x✝ ⟶ mk (n✝ + 1)
hf✝ : degeneracies.multiplicativeClosure f✝
hf_ih✝ : IsSplitEpi f✝
⊢ IsSplitEpi (f✝ ≫ σ i✝)

Proof state:
case of.σ
x y : SimplexCategoryGenRel
e : x ⟶ y
n✝ : ℕ
i✝ : Fin (n✝ + 1)
⊢ IsSplitEpi (σ i✝)

Tactic:
infer_instance

Result:
no goals

Proof state:
x y : SimplexCategoryGenRel
e : x ⟶ y
he : P_σ e
⊢ IsSplitEpi e

Tactic:
induction he with
| of x hx => cases hx; infer_instance
| id => infer_instance
| comp_of _ _ _ h => cases h; infer_instance

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem exists_lt_mul_omega0' {o : Ordinal} ⦃a⦄ (h : a < o * ω) :
    ∃ i : ℕ, a < o * ↑i + o

Proof state:
case intro.intro.intro
o a : Ordinal.{u_1}
h : a < o * ω
i : ℕ
hi : ↑i < ω
h' : a < o * ↑i
⊢ ∃ i, a < o * ↑i + o

Tactic:
exact ⟨i, h'.trans_le (le_add_right _ _)⟩

Result:
no goals

Proof state:
o a : Ordinal.{u_1}
h : a < o * ω
⊢ ∃ i, a < o * ↑i + o

Tactic:
obtain ⟨i, hi, h'⟩ := (lt_mul_of_limit isLimit_omega0).1 h

Result:
case intro.intro
o a : Ordinal.{u_1}
h : a < o * ω
i : Ordinal.{u_1}
hi : i < ω
h' : a < o * i
⊢ ∃ i, a < o * ↑i + o

Proof state:
case intro.intro
o a : Ordinal.{u_1}
h : a < o * ω
i : Ordinal.{u_1}
hi : i < ω
h' : a < o * i
⊢ ∃ i, a < o * ↑i + o

Tactic:
obtain ⟨i, rfl⟩ := lt_omega0.1 hi

Result:
case intro.intro.intro
o a : Ordinal.{u_1}
h : a < o * ω
i : ℕ
hi : ↑i < ω
h' : a < o * ↑i
⊢ ∃ i, a < o * ↑i + o
-- Mathlib/Data/Real/ConjExponents.lean
lemma coe_conjExponent {p : ℝ≥0} (hp : 1 < p) : p.conjExponent = conjExponent p

Proof state:
p : ℝ≥0
hp : 1 < p
⊢ ↑(p / (p - 1)) = 1 + ↑(p - 1)⁻¹

Tactic:
norm_cast

Result:
p : ℝ≥0
hp : 1 < p
⊢ p / (p - 1) = 1 + (p - 1)⁻¹

Proof state:
p : ℝ≥0
hp : 1 < p
⊢ p / (p - 1) = 1 + (p - 1)⁻¹

Tactic:
field_simp [(tsub_pos_of_lt hp).ne']

Result:
p : ℝ≥0
hp : 1 < p
⊢ p = p - 1 + 1

Proof state:
p : ℝ≥0
hp : 1 < p
⊢ ↑(p / (p - 1)) = 1 + (↑(p - 1))⁻¹

Tactic:
rw [← coe_inv (tsub_pos_of_lt hp).ne']

Result:
p : ℝ≥0
hp : 1 < p
⊢ ↑(p / (p - 1)) = 1 + ↑(p - 1)⁻¹

Proof state:
p : ℝ≥0
hp : 1 < p
⊢ ↑p.conjExponent = (↑p).conjExponent

Tactic:
rw [NNReal.conjExponent, conjExponent]

Result:
p : ℝ≥0
hp : 1 < p
⊢ ↑(p / (p - 1)) = 1 + (↑p - 1)⁻¹

Proof state:
p : ℝ≥0
hp : 1 < p
⊢ p = p - 1 + 1

Tactic:
rw [tsub_add_cancel_of_le hp.le]

Result:
no goals

Proof state:
p : ℝ≥0
hp : 1 < p
⊢ ↑(p / (p - 1)) = 1 + (↑p - 1)⁻¹

Tactic:
norm_cast

Result:
p : ℝ≥0
hp : 1 < p
⊢ ↑(p / (p - 1)) = 1 + (↑(p - 1))⁻¹
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem map_sum_le {ι : Type*} {s : Finset ι} {f : ι → R} {g : Γ₀} (hf : ∀ i ∈ s, v (f i) ≤ g) :
    v (∑ i ∈ s, f i) ≤ g

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s : Finset ι
f : ι → R
g : Γ₀
hf : ∀ i ∈ s, v (f i) ≤ g
⊢ v (∑ i ∈ s, f i) ≤ g

Tactic:
classical
refine
  Finset.induction_on s (fun _ => v.map_zero ▸ zero_le')
    (fun a s has ih hf => ?_) hf
rw [Finset.forall_mem_insert] at hf; rw [Finset.sum_insert has]
exact v.map_add_le hf.1 (ih hf.2)

Result:
no goals

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s✝ : Finset ι
f : ι → R
g : Γ₀
hf✝ : ∀ i ∈ s✝, v (f i) ≤ g
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, v (f i) ≤ g) → v (∑ i ∈ s, f i) ≤ g
hf : v (f a) ≤ g ∧ ∀ x ∈ s, v (f x) ≤ g
⊢ v (f a + ∑ x ∈ s, f x) ≤ g

Tactic:
exact v.map_add_le hf.1 (ih hf.2)

Result:
no goals

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s✝ : Finset ι
f : ι → R
g : Γ₀
hf✝ : ∀ i ∈ s✝, v (f i) ≤ g
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, v (f i) ≤ g) → v (∑ i ∈ s, f i) ≤ g
hf : v (f a) ≤ g ∧ ∀ x ∈ s, v (f x) ≤ g
⊢ v (∑ i ∈ insert a s, f i) ≤ g

Tactic:
rw [Finset.sum_insert has]

Result:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s✝ : Finset ι
f : ι → R
g : Γ₀
hf✝ : ∀ i ∈ s✝, v (f i) ≤ g
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, v (f i) ≤ g) → v (∑ i ∈ s, f i) ≤ g
hf : v (f a) ≤ g ∧ ∀ x ∈ s, v (f x) ≤ g
⊢ v (f a + ∑ x ∈ s, f x) ≤ g

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s : Finset ι
f : ι → R
g : Γ₀
hf : ∀ i ∈ s, v (f i) ≤ g
⊢ v (∑ i ∈ s, f i) ≤ g

Tactic:
refine
  Finset.induction_on s (fun _ => v.map_zero ▸ zero_le')
    (fun a s has ih hf => ?_) hf

Result:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s✝ : Finset ι
f : ι → R
g : Γ₀
hf✝ : ∀ i ∈ s✝, v (f i) ≤ g
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, v (f i) ≤ g) → v (∑ i ∈ s, f i) ≤ g
hf : ∀ i ∈ insert a s, v (f i) ≤ g
⊢ v (∑ i ∈ insert a s, f i) ≤ g

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s✝ : Finset ι
f : ι → R
g : Γ₀
hf✝ : ∀ i ∈ s✝, v (f i) ≤ g
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, v (f i) ≤ g) → v (∑ i ∈ s, f i) ≤ g
hf : ∀ i ∈ insert a s, v (f i) ≤ g
⊢ v (∑ i ∈ insert a s, f i) ≤ g

Tactic:
rw [Finset.forall_mem_insert] at hf

Result:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s✝ : Finset ι
f : ι → R
g : Γ₀
hf✝ : ∀ i ∈ s✝, v (f i) ≤ g
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, v (f i) ≤ g) → v (∑ i ∈ s, f i) ≤ g
hf : v (f a) ≤ g ∧ ∀ x ∈ s, v (f x) ≤ g
⊢ v (∑ i ∈ insert a s, f i) ≤ g
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Fold.lean
theorem fold_succ {α : Type u} (n : Nat) (f : (i : Nat) → i < n + 1 → α → α) (init : α) :
    fold (n + 1) f init = f n (by omega) (fold n (fun i h => f i (by omega)) init)

Proof state:
α : Type u
n : Nat
f : (i : Nat) → i < n + 1 → α → α
init : α
⊢ n < n + 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type u
n : Nat
f : (i : Nat) → i < n + 1 → α → α
init : α
i : Nat
h : i < n
⊢ i < n + 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type u
n : Nat
f : (i : Nat) → i < n + 1 → α → α
init : α
⊢ (n + 1).fold f init = f n ⋯ (n.fold (fun i h => f i ⋯) init)

Tactic:
simp [fold]

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem corec_eq (f : α → β) (g : α → α) (a : α) : corec f g a = f a :: corec f g (g a)

Proof state:
α : Type u
β : Type v
f : α → β
g : α → α
a : α
⊢ f a :: map f (iterate g (g a)) = f a :: corec f g (g a)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β
g : α → α
a : α
⊢ corec f g a = f a :: corec f g (g a)

Tactic:
rw [corec_def, map_eq, head_iterate, tail_iterate]

Result:
α : Type u
β : Type v
f : α → β
g : α → α
a : α
⊢ f a :: map f (iterate g (g a)) = f a :: corec f g (g a)
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
theorem isClosed_zeroLocus (s : Set A) : IsClosed (zeroLocus 𝒜 s)

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
s : Set A
⊢ ∃ s_1, zeroLocus 𝒜 s = zeroLocus 𝒜 s_1

Tactic:
exact ⟨s, rfl⟩

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
s : Set A
⊢ IsClosed (zeroLocus 𝒜 s)

Tactic:
rw [isClosed_iff_zeroLocus]

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
s : Set A
⊢ ∃ s_1, zeroLocus 𝒜 s = zeroLocus 𝒜 s_1
-- Mathlib/Order/Interval/Set/Disjoint.lean
theorem biUnion_Ico_eq_Iio_self_iff {p : ι → Prop} {f : ∀ i, p i → α} {a : α} :
    ⋃ (i) (hi : p i), Ico (f i hi) a = Iio a ↔ ∀ x < a, ∃ i hi, f i hi ≤ x

Proof state:
ι : Sort u
α : Type v
inst✝ : LinearOrder α
p : ι → Prop
f : (i : ι) → p i → α
a : α
⊢ ⋃ i, ⋃ (hi : p i), Ico (f i hi) a = Iio a ↔ ∀ x < a, ∃ i, ∃ (hi : p i), f i hi ≤ x

Tactic:
simp [← Ici_inter_Iio, ← iUnion_inter, subset_def]

Result:
no goals
-- Mathlib/GroupTheory/Perm/ConjAct.lean
theorem mem_cycleFactorsFinset_conj'
    (k : ConjAct (Perm α)) (g c : Perm α) :
    k • c ∈ (k • g).cycleFactorsFinset ↔ c ∈ g.cycleFactorsFinset

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ ConjAct.ofConjAct k * c * (ConjAct.ofConjAct k)⁻¹ ∈
      (ConjAct.ofConjAct k * g * (ConjAct.ofConjAct k)⁻¹).cycleFactorsFinset ↔
    c ∈ g.cycleFactorsFinset

Tactic:
apply mem_cycleFactorsFinset_conj g k

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ k • c ∈ (k • g).cycleFactorsFinset ↔ c ∈ g.cycleFactorsFinset

Tactic:
simp only [ConjAct.smul_def]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ ConjAct.ofConjAct k * c * (ConjAct.ofConjAct k)⁻¹ ∈
      (ConjAct.ofConjAct k * g * (ConjAct.ofConjAct k)⁻¹).cycleFactorsFinset ↔
    c ∈ g.cycleFactorsFinset
-- Mathlib/RingTheory/PowerSeries/Trunc.lean
lemma trunc_X_of {n : ℕ} (hn : 2 ≤ n) : trunc n X = (Polynomial.X : R[X])

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : 2 ≤ n
⊢ trunc n X = Polynomial.X

Tactic:
cases n with
| zero => contradiction
| succ n =>
  cases n with
  | zero => contradiction
  | succ n => exact trunc_X n

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : 2 ≤ n + 1
⊢ trunc (n + 1) X = Polynomial.X

Tactic:
cases n with
| zero => contradiction
| succ n => exact trunc_X n

Result:
no goals

Proof state:
case succ.zero
R : Type u_1
inst✝ : Semiring R
hn : 2 ≤ 0 + 1
⊢ trunc (0 + 1) X = Polynomial.X

Tactic:
contradiction

Result:
no goals

Proof state:
case succ.succ
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : 2 ≤ n + 1 + 1
⊢ trunc (n + 1 + 1) X = Polynomial.X

Tactic:
exact trunc_X n

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝ : Semiring R
hn : 2 ≤ 0
⊢ trunc 0 X = Polynomial.X

Tactic:
contradiction

Result:
no goals