harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Padics/RingHoms.lean
theorem zmod_congr_of_sub_mem_span (n : ℕ) (x : ℤ_[p]) (a b : ℕ)
    (ha : x - a ∈ (Ideal.span {(p : ℤ_[p]) ^ n}))
    (hb : x - b ∈ (Ideal.span {(p : ℤ_[p]) ^ n})) : (a : ZMod (p ^ n)) = b

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℕ
ha : x - ↑a ∈ Ideal.span {↑p ^ n}
hb : x - ↑b ∈ Ideal.span {↑p ^ n}
⊢ ↑a = ↑b

Tactic:
simpa using zmod_congr_of_sub_mem_span_aux n x a b ha hb

Result:
no goals
-- Mathlib/Algebra/Ring/Hom/Defs.lean
theorem comp_zero (g : β →ₙ+* γ) : g.comp (0 : α →ₙ+* β) = 0

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
g : β →ₙ+* γ
⊢ g.comp 0 = 0

Tactic:
ext

Result:
case a
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
g : β →ₙ+* γ
x✝ : α
⊢ (g.comp 0) x✝ = 0 x✝

Proof state:
case a
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
g : β →ₙ+* γ
x✝ : α
⊢ (g.comp 0) x✝ = 0 x✝

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem ins_eq_fill {path : Path α} {t : RBNode α} :
    path.Balanced c₀ n₀ c n → t.Balanced c n → path.ins t = (path.fill t).setBlack
  | .root, h => rfl
  | .redL hb H, ha | .redR ha H, hb => by unfold ins; exact ins_eq_fill H (.red ha hb)
  | .blackL hb H, ha => by rw [ins, fill, ← ins_eq_fill H (.black ha hb), balance1_eq ha]
  | .blackR ha H, hb => by rw [ins, fill, ← ins_eq_fill H (.black ha hb), balance2_eq hb]

Proof state:
α : Type u_1
c₀ : RBColor
n₀ : Nat
c✝ : RBColor
n✝ : Nat
path : Path α
t : RBNode α
n : Nat
c : RBColor
x✝ : RBNode α
c₁✝ : RBColor
v✝ : α
parent✝ : Path α
ha : x✝.Balanced c₁✝ n
H : Path.Balanced c₀ n₀ parent✝ black (n + 1)
hb : t.Balanced c n
⊢ (right black x✝ v✝ parent✝).ins t = ((right black x✝ v✝ parent✝).fill t).setBlack

Tactic:
rw [ins, fill, ← ins_eq_fill H (.black ha hb), balance2_eq hb]

Result:
no goals

Proof state:
α : Type u_1
c₀ : RBColor
n₀ : Nat
c : RBColor
n✝ : Nat
path : Path α
t : RBNode α
n : Nat
x✝ : RBNode α
v✝ : α
parent✝ : Path α
ha : x✝.Balanced black n
H : Path.Balanced c₀ n₀ parent✝ red n
hb : t.Balanced black n
⊢ (right red x✝ v✝ parent✝).ins t = ((right red x✝ v✝ parent✝).fill t).setBlack

Tactic:
unfold ins

Result:
α : Type u_1
c₀ : RBColor
n₀ : Nat
c : RBColor
n✝ : Nat
path : Path α
t : RBNode α
n : Nat
x✝ : RBNode α
v✝ : α
parent✝ : Path α
ha : x✝.Balanced black n
H : Path.Balanced c₀ n₀ parent✝ red n
hb : t.Balanced black n
⊢ parent✝.ins (node red x✝ v✝ t) = ((right red x✝ v✝ parent✝).fill t).setBlack

Proof state:
α : Type u_1
c₀ : RBColor
n₀ : Nat
c✝ : RBColor
n✝ : Nat
path : Path α
t : RBNode α
n : Nat
c : RBColor
y✝ : RBNode α
c₂✝ : RBColor
parent✝ : Path α
v✝ : α
hb : y✝.Balanced c₂✝ n
H : Path.Balanced c₀ n₀ parent✝ black (n + 1)
ha : t.Balanced c n
⊢ (left black parent✝ v✝ y✝).ins t = ((left black parent✝ v✝ y✝).fill t).setBlack

Tactic:
rw [ins, fill, ← ins_eq_fill H (.black ha hb), balance1_eq ha]

Result:
no goals

Proof state:
α : Type u_1
c₀ : RBColor
n₀ : Nat
c : RBColor
n✝ : Nat
path : Path α
t : RBNode α
n : Nat
x✝ : RBNode α
v✝ : α
parent✝ : Path α
ha : x✝.Balanced black n
H : Path.Balanced c₀ n₀ parent✝ red n
hb : t.Balanced black n
⊢ parent✝.ins (node red x✝ v✝ t) = ((right red x✝ v✝ parent✝).fill t).setBlack

Tactic:
exact ins_eq_fill H (.red ha hb)

Result:
no goals
-- Mathlib/Data/Set/Image.lean
@[simp]
lemma forall_subset_image_iff {p : Set β → Prop} : (∀ t ⊆ f '' s, p t) ↔ ∀ t ⊆ s, p (f '' t)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
p : Set β → Prop
⊢ (∀ t ⊆ f '' s, p t) ↔ ∀ t ⊆ s, p (f '' t)

Tactic:
simp [subset_image_iff]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem Monic.sub_of_right {p q : R[X]} (hq : q.leadingCoeff = -1) (hpq : degree p < degree q) :
    Monic (p - q)

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
this : (-q).coeff (-q).natDegree = 1
⊢ (p - q).Monic

Tactic:
rw [sub_eq_add_neg]

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
this : (-q).coeff (-q).natDegree = 1
⊢ (p + -q).Monic

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
this : (-q).coeff (-q).natDegree = 1
⊢ p.degree < (-q).degree

Tactic:
rwa [degree_neg]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
⊢ (p - q).Monic

Tactic:
have : (-q).coeff (-q).natDegree = 1 := by
  rw [natDegree_neg, coeff_neg, show q.coeff q.natDegree = -1 from hq, neg_neg]

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
this : (-q).coeff (-q).natDegree = 1
⊢ (p - q).Monic

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
this : (-q).coeff (-q).natDegree = 1
⊢ (p + -q).Monic

Tactic:
apply Monic.add_of_right this

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
this : (-q).coeff (-q).natDegree = 1
⊢ p.degree < (-q).degree

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
⊢ (-q).coeff (-q).natDegree = 1

Tactic:
rw [natDegree_neg, coeff_neg, show q.coeff q.natDegree = -1 from hq, neg_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem filterMap_val [BEq α] [Hashable α] {m : Raw₀ α β} {f : (a : α) → β a → Option (δ a)} :
    m.val.filterMap f = m.filterMap f

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
f : (a : α) → β a → Option (δ a)
⊢ Raw.filterMap f m.val = (Raw₀.filterMap f m).val

Tactic:
simp [Raw.filterMap, m.2]

Result:
no goals
-- Mathlib/Logic/Function/Basic.lean
theorem eq_mp_bijective {α β : Sort _} (h : α = β) : Function.Bijective (Eq.mp h)

Proof state:
case refl
α : Sort u_3
⊢ Bijective ⋯.mp

Tactic:
exact ⟨fun _ _ ↦ id, fun x ↦ ⟨x, rfl⟩⟩

Result:
no goals

Proof state:
α β : Sort u_3
h : α = β
⊢ Bijective h.mp

Tactic:
cases h

Result:
case refl
α : Sort u_3
⊢ Bijective ⋯.mp
-- Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean
@[reassoc (attr := simp)] lemma w₀₂_τ₂ : S.v₀₁.τ₂ ≫ S.v₁₂.τ₂ = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.v₀₁.τ₂ ≫ S.v₁₂.τ₂ = 0

Tactic:
rw [← comp_τ₂, S.w₀₂, zero_τ₂]

Result:
no goals
-- Mathlib/RingTheory/FiniteType.lean
theorem of_comp_finiteType {f : A →+* B} {g : B →+* C} (h : (g.comp f).FiniteType) :
    g.FiniteType

Proof state:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : (g.comp f).FiniteType
⊢ g.FiniteType

Tactic:
algebraize [f, g, g.comp f]

Result:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : (g.comp f).FiniteType
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
algebraizeInst✝ : Algebra.FiniteType A C
⊢ g.FiniteType

Proof state:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : (g.comp f).FiniteType
algInst✝² : Algebra A B := f.toAlgebra
algInst✝¹ : Algebra B C := g.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap A C))
algebraizeInst✝ : Algebra.FiniteType A C
⊢ g.FiniteType

Tactic:
exact Algebra.FiniteType.of_restrictScalars_finiteType A B C

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Prod.lean
@[simp] lemma fst_map_swap : (ρ.map Prod.swap).fst = ρ.snd

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ρ : Measure (α × β)
⊢ (map Prod.swap ρ).fst = ρ.snd

Tactic:
rw [Measure.fst, Measure.map_map measurable_fst measurable_swap]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ρ : Measure (α × β)
⊢ map (Prod.fst ∘ Prod.swap) ρ = ρ.snd

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ρ : Measure (α × β)
⊢ map (Prod.fst ∘ Prod.swap) ρ = ρ.snd

Tactic:
rfl

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem forall_and_left [Nonempty α] (q : Prop) (p : α → Prop) :
    (∀ x, q ∧ p x) ↔ (q ∧ ∀ x, p x)

Proof state:
α : Sort u_1
inst✝ : Nonempty α
q : Prop
p : α → Prop
⊢ (∀ (x : α), q ∧ p x) ↔ q ∧ ∀ (x : α), p x

Tactic:
rw [forall_and, forall_const]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean
theorem Sphere.center_eq_iff_eq_of_mem {s₁ s₂ : Sphere P} {p : P} (hs₁ : p ∈ s₁) (hs₂ : p ∈ s₂) :
    s₁.center = s₂.center ↔ s₁ = s₂

Proof state:
P : Type u_2
inst✝ : MetricSpace P
s₁ s₂ : Sphere P
p : P
hs₁ : p ∈ s₁
hs₂ : p ∈ s₂
h : s₁.center = s₂.center
⊢ s₁.radius = s₂.radius

Tactic:
rw [mem_sphere] at hs₁ hs₂

Result:
P : Type u_2
inst✝ : MetricSpace P
s₁ s₂ : Sphere P
p : P
hs₁ : dist p s₁.center = s₁.radius
hs₂ : dist p s₂.center = s₂.radius
h : s₁.center = s₂.center
⊢ s₁.radius = s₂.radius

Proof state:
P : Type u_2
inst✝ : MetricSpace P
s₁ s₂ : Sphere P
p : P
hs₁ : p ∈ s₁
hs₂ : p ∈ s₂
⊢ s₁.center = s₂.center ↔ s₁ = s₂

Tactic:
refine ⟨fun h => Sphere.ext h ?_, fun h => h ▸ rfl⟩

Result:
P : Type u_2
inst✝ : MetricSpace P
s₁ s₂ : Sphere P
p : P
hs₁ : p ∈ s₁
hs₂ : p ∈ s₂
h : s₁.center = s₂.center
⊢ s₁.radius = s₂.radius

Proof state:
P : Type u_2
inst✝ : MetricSpace P
s₁ s₂ : Sphere P
p : P
hs₁ : dist p s₁.center = s₁.radius
hs₂ : dist p s₂.center = s₂.radius
h : s₁.center = s₂.center
⊢ s₁.radius = s₂.radius

Tactic:
rw [← hs₁, ← hs₂, h]

Result:
no goals
-- Mathlib/Analysis/Convex/AmpleSet.lean
theorem preimage {s : Set F} (h : AmpleSet s) (L : E ≃ᵃL[ℝ] F) : AmpleSet (L ⁻¹' s)

Proof state:
F : Type u_1
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module ℝ F
inst✝³ : TopologicalSpace F
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module ℝ E
inst✝ : TopologicalSpace E
s : Set F
h : AmpleSet s
L : E ≃ᵃL[ℝ] F
⊢ AmpleSet (⇑L.symm '' s)

Tactic:
exact h.image L.symm

Result:
no goals

Proof state:
F : Type u_1
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module ℝ F
inst✝³ : TopologicalSpace F
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module ℝ E
inst✝ : TopologicalSpace E
s : Set F
h : AmpleSet s
L : E ≃ᵃL[ℝ] F
⊢ AmpleSet (⇑L ⁻¹' s)

Tactic:
rw [← L.image_symm_eq_preimage]

Result:
F : Type u_1
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module ℝ F
inst✝³ : TopologicalSpace F
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module ℝ E
inst✝ : TopologicalSpace E
s : Set F
h : AmpleSet s
L : E ≃ᵃL[ℝ] F
⊢ AmpleSet (⇑L.symm '' s)
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem prod_map (s : Finset α) (e : α ↪ γ) (f : γ → β) :
    ∏ x ∈ s.map e, f x = ∏ x ∈ s, f (e x)

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset α
e : α ↪ γ
f : γ → β
⊢ ∏ x ∈ map e s, f x = ∏ x ∈ s, f (e x)

Tactic:
rw [Finset.prod, Finset.map_val, Multiset.map_map]

Result:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset α
e : α ↪ γ
f : γ → β
⊢ (Multiset.map ((fun x => f x) ∘ ⇑e) s.val).prod = ∏ x ∈ s, f (e x)

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset α
e : α ↪ γ
f : γ → β
⊢ (Multiset.map ((fun x => f x) ∘ ⇑e) s.val).prod = ∏ x ∈ s, f (e x)

Tactic:
rfl

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
lemma integrable_exp_mul_of_le [IsFiniteMeasure μ] {X : Ω → ℝ} (t b : ℝ) (ht : 0 ≤ t)
    (hX : AEMeasurable X μ) (hb : ∀ᵐ ω ∂μ, X ω ≤ b) :
    Integrable (fun ω ↦ exp (t * X ω)) μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
t b : ℝ
ht : 0 ≤ t
hX : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
⊢ Integrable (fun ω => rexp (t * X ω)) μ

Tactic:
refine .of_mem_Icc 0 (rexp (t * b)) (measurable_exp.comp_aemeasurable (hX.const_mul t)) ?_

Result:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
t b : ℝ
ht : 0 ≤ t
hX : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
⊢ ∀ᵐ (ω : Ω) ∂μ, rexp (t * X ω) ∈ Set.Icc 0 (rexp (t * b))

Proof state:
case h
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
t b : ℝ
ht : 0 ≤ t
hX : AEMeasurable X μ
hb✝ : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
ω : Ω
hb : X ω ≤ b
⊢ rexp (t * X ω) ∈ Set.Icc 0 (rexp (t * b))

Tactic:
exact ⟨by positivity, by gcongr⟩

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
t b : ℝ
ht : 0 ≤ t
hX : AEMeasurable X μ
hb✝ : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
ω : Ω
hb : X ω ≤ b
⊢ 0 ≤ rexp (t * X ω)

Tactic:
positivity

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
t b : ℝ
ht : 0 ≤ t
hX : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
⊢ ∀ᵐ (ω : Ω) ∂μ, rexp (t * X ω) ∈ Set.Icc 0 (rexp (t * b))

Tactic:
filter_upwards [hb] with ω hb

Result:
case h
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
t b : ℝ
ht : 0 ≤ t
hX : AEMeasurable X μ
hb✝ : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
ω : Ω
hb : X ω ≤ b
⊢ rexp (t * X ω) ∈ Set.Icc 0 (rexp (t * b))

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
t b : ℝ
ht : 0 ≤ t
hX : AEMeasurable X μ
hb✝ : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b
ω : Ω
hb : X ω ≤ b
⊢ rexp (t * X ω) ≤ rexp (t * b)

Tactic:
gcongr

Result:
no goals
-- Mathlib/MeasureTheory/Integral/CircleTransform.lean
theorem continuous_circleTransform {R : ℝ} (hR : 0 < R) {f : ℂ → E} {z w : ℂ}
    (hf : ContinuousOn f <| sphere z R) (hw : w ∈ ball z R) :
    Continuous (circleTransform R z w f)

Proof state:
case hg.hg.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ Continuous fun x => (circleMap z R x - w)⁻¹

Tactic:
exact continuous_circleMap_inv hw

Result:
no goals

Proof state:
case hg.hg.hg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ ∀ (x : ℝ), circleMap z R x ∈ sphere z R

Tactic:
exact fun _ => (circleMap_mem_sphere _ hR.le) _

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ Continuous (circleTransform R z w f)

Tactic:
apply_rules [Continuous.smul, continuous_const]

Result:
case hg.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ Continuous (deriv (circleMap z R))

case hg.hg.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ Continuous fun x => (circleMap z R x - w)⁻¹

case hg.hg.hg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ Continuous fun x => f (circleMap z R x)

Proof state:
case hg.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ Continuous fun x => circleMap 0 R x * I

Tactic:
apply_rules [Continuous.mul, continuous_circleMap 0 R, continuous_const]

Result:
no goals

Proof state:
case hg.hg.hg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ Continuous fun x => f (circleMap z R x)

Tactic:
apply ContinuousOn.comp_continuous hf (continuous_circleMap z R)

Result:
case hg.hg.hg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ ∀ (x : ℝ), circleMap z R x ∈ sphere z R

Proof state:
case hg.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ Continuous (deriv (circleMap z R))

Tactic:
rw [funext <| deriv_circleMap _ _]

Result:
case hg.hf
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R : ℝ
hR : 0 < R
f : ℂ → E
z w : ℂ
hf : ContinuousOn f (sphere z R)
hw : w ∈ ball z R
⊢ Continuous fun x => circleMap 0 R x * I
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem mem_rootSet' {p : T[X]} {S : Type*} [CommRing S] [IsDomain S] [Algebra T S] {a : S} :
    a ∈ p.rootSet S ↔ p.map (algebraMap T S) ≠ 0 ∧ aeval a p = 0

Proof state:
T : Type w
inst✝³ : CommRing T
p : T[X]
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : S
⊢ a ∈ p.rootSet S ↔ map (algebraMap T S) p ≠ 0 ∧ (aeval a) p = 0

Tactic:
classical
rw [rootSet_def, Finset.mem_coe, mem_toFinset, mem_aroots']

Result:
no goals

Proof state:
T : Type w
inst✝³ : CommRing T
p : T[X]
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : S
⊢ a ∈ p.rootSet S ↔ map (algebraMap T S) p ≠ 0 ∧ (aeval a) p = 0

Tactic:
rw [rootSet_def, Finset.mem_coe, mem_toFinset, mem_aroots']

Result:
no goals
-- Mathlib/Computability/Ackermann.lean
theorem one_lt_ack_succ_right : ∀ m n, 1 < ack m (n + 1)
  | 0, n => by simp
  | m + 1, n => by
    rw [ack_succ_succ]
    obtain ⟨h, h⟩ := exists_eq_succ_of_ne_zero (ack_pos (m + 1) n).ne'
    rw [h]
    apply one_lt_ack_succ_right

Proof state:
case intro
m n h✝ : ℕ
h : ack (m + 1) n = h✝.succ
⊢ 1 < ack m h✝.succ

Tactic:
apply one_lt_ack_succ_right

Result:
no goals

Proof state:
n : ℕ
⊢ 1 < ack 0 (n + 1)

Tactic:
simp

Result:
no goals

Proof state:
case intro
m n h✝ : ℕ
h : ack (m + 1) n = h✝.succ
⊢ 1 < ack m (ack (m + 1) n)

Tactic:
rw [h]

Result:
case intro
m n h✝ : ℕ
h : ack (m + 1) n = h✝.succ
⊢ 1 < ack m h✝.succ

Proof state:
m n : ℕ
⊢ 1 < ack (m + 1) (n + 1)

Tactic:
rw [ack_succ_succ]

Result:
m n : ℕ
⊢ 1 < ack m (ack (m + 1) n)

Proof state:
m n : ℕ
⊢ 1 < ack m (ack (m + 1) n)

Tactic:
obtain ⟨h, h⟩ := exists_eq_succ_of_ne_zero (ack_pos (m + 1) n).ne'

Result:
case intro
m n h✝ : ℕ
h : ack (m + 1) n = h✝.succ
⊢ 1 < ack m (ack (m + 1) n)
-- Mathlib/Algebra/Algebra/Basic.lean
theorem surjective_algebraMap_of_linearMap (hb : Surjective b) :
    Surjective (algebraMap F E) := fun x ↦ by
  obtain ⟨x, rfl⟩ := hb x
  obtain ⟨y, hy⟩ := hb (b 1 * b 1)
  refine ⟨x * y, ?_⟩
  obtain ⟨z, hz⟩ := hb 1
  apply_fun (x • z • ·) at hy
  rwa [← map_smul, smul_eq_mul, mul_comm, ← smul_mul_assoc, ← map_smul _ z, smul_eq_mul, mul_one,
    ← smul_eq_mul, map_smul, hz, one_mul, ← map_smul, smul_eq_mul, mul_one, smul_smul,
    ← Algebra.algebraMap_eq_smul_one] at hy

Proof state:
case intro.intro
F : Type u_1
E : Type u_2
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
b : F →ₗ[F] E
hb : Surjective ⇑b
x y : F
hy : b y = b 1 * b 1
⊢ (algebraMap F E) (x * y) = b x

Tactic:
obtain ⟨z, hz⟩ := hb 1

Result:
case intro.intro.intro
F : Type u_1
E : Type u_2
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
b : F →ₗ[F] E
hb : Surjective ⇑b
x y : F
hy : b y = b 1 * b 1
z : F
hz : b z = 1
⊢ (algebraMap F E) (x * y) = b x

Proof state:
F : Type u_1
E : Type u_2
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
b : F →ₗ[F] E
hb : Surjective ⇑b
x : E
⊢ ∃ a, (algebraMap F E) a = x

Tactic:
obtain ⟨x, rfl⟩ := hb x

Result:
case intro
F : Type u_1
E : Type u_2
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
b : F →ₗ[F] E
hb : Surjective ⇑b
x : F
⊢ ∃ a, (algebraMap F E) a = b x

Proof state:
case intro.intro.intro
F : Type u_1
E : Type u_2
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
b : F →ₗ[F] E
hb : Surjective ⇑b
x y z : F
hz : b z = 1
hy : x • z • b y = x • z • (b 1 * b 1)
⊢ (algebraMap F E) (x * y) = b x

Tactic:
rwa [← map_smul, smul_eq_mul, mul_comm, ← smul_mul_assoc, ← map_smul _ z, smul_eq_mul, mul_one,
  ← smul_eq_mul, map_smul, hz, one_mul, ← map_smul, smul_eq_mul, mul_one, smul_smul,
  ← Algebra.algebraMap_eq_smul_one] at hy

Result:
no goals

Proof state:
case intro
F : Type u_1
E : Type u_2
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
b : F →ₗ[F] E
hb : Surjective ⇑b
x : F
⊢ ∃ a, (algebraMap F E) a = b x

Tactic:
obtain ⟨y, hy⟩ := hb (b 1 * b 1)

Result:
case intro.intro
F : Type u_1
E : Type u_2
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
b : F →ₗ[F] E
hb : Surjective ⇑b
x y : F
hy : b y = b 1 * b 1
⊢ ∃ a, (algebraMap F E) a = b x

Proof state:
case intro.intro
F : Type u_1
E : Type u_2
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
b : F →ₗ[F] E
hb : Surjective ⇑b
x y : F
hy : b y = b 1 * b 1
⊢ ∃ a, (algebraMap F E) a = b x

Tactic:
refine ⟨x * y, ?_⟩

Result:
case intro.intro
F : Type u_1
E : Type u_2
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
b : F →ₗ[F] E
hb : Surjective ⇑b
x y : F
hy : b y = b 1 * b 1
⊢ (algebraMap F E) (x * y) = b x
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
private lemma continuousAt_mul_top_ne_zero {a : ℝ} (h : a ≠ 0) :
    ContinuousAt (fun p : EReal × EReal ↦ p.1 * p.2) (⊤, a)

Proof state:
case inr
a : ℝ
h : a ≠ 0
a_pos : a > 0
⊢ ContinuousAt (fun p => p.1 * p.2) (⊤, ↑a)

Tactic:
exact continuousAt_mul_top_pos a_pos

Result:
no goals

Proof state:
a : ℝ
h : a ≠ 0
⊢ ContinuousAt (fun p => p.1 * p.2) (⊤, ↑a)

Tactic:
rcases lt_or_gt_of_ne h with a_neg | a_pos

Result:
case inl
a : ℝ
h : a ≠ 0
a_neg : a < 0
⊢ ContinuousAt (fun p => p.1 * p.2) (⊤, ↑a)

case inr
a : ℝ
h : a ≠ 0
a_pos : a > 0
⊢ ContinuousAt (fun p => p.1 * p.2) (⊤, ↑a)

Proof state:
case inl
a : ℝ
h : a ≠ 0
a_neg : a < 0
⊢ ContinuousAt (fun p => p.1 * p.2) (⊤, ↑a)

Tactic:
exact neg_neg a ▸ continuousAt_mul_symm2 (continuousAt_mul_top_pos (neg_pos.2 a_neg))

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
lemma differentiableAt_completedCosZeta
    (a : UnitAddCircle) {s : ℂ} (hs : s ≠ 0) (hs' : s ≠ 1 ∨ a ≠ 0) :
    DifferentiableAt ℂ (completedCosZeta a) s

Proof state:
case refine_2.refine_2
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
ha : a ≠ 0
⊢ (if a = 0 then 1 else 0) = 0

Tactic:
simpa

Result:
no goals

Proof state:
case refine_2.refine_1
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
h : s ≠ 1
⊢ s / 2 ≠ ↑(1 / 2)

Tactic:
simpa [push_cast] using h ∘ (div_left_inj' two_ne_zero).mp

Result:
no goals

Proof state:
case refine_2
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
⊢ s / 2 ≠ ↑(1 / 2) ∨ (if a = 0 then 1 else 0) = 0

Tactic:
refine Or.imp (fun h ↦ ?_) (fun ha ↦ ?_) hs'

Result:
case refine_2.refine_1
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
h : s ≠ 1
⊢ s / 2 ≠ ↑(1 / 2)

case refine_2.refine_2
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
ha : a ≠ 0
⊢ (if a = 0 then 1 else 0) = 0

Proof state:
case refine_1
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
⊢ s / 2 ≠ 0

Tactic:
exact div_ne_zero_iff.mpr ⟨hs, two_ne_zero⟩

Result:
no goals

Proof state:
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
⊢ DifferentiableAt ℂ (completedCosZeta a) s

Tactic:
refine (((hurwitzEvenFEPair a).symm.differentiableAt_Λ (Or.inl ?_) ?_).comp s
    (differentiableAt_id.div_const _)).div_const _

Result:
case refine_1
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
⊢ s / 2 ≠ 0

case refine_2
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
⊢ s / 2 ≠ ↑(hurwitzEvenFEPair a).symm.k ∨ (hurwitzEvenFEPair a).symm.g₀ = 0

Proof state:
case refine_2
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
⊢ s / 2 ≠ ↑(hurwitzEvenFEPair a).symm.k ∨ (hurwitzEvenFEPair a).symm.g₀ = 0

Tactic:
change s / 2 ≠ ↑(1 / 2 : ℝ) ∨ (if a = 0 then 1 else 0) = 0

Result:
case refine_2
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
⊢ s / 2 ≠ ↑(1 / 2) ∨ (if a = 0 then 1 else 0) = 0