harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Filter/AtTopBot/Archimedean.lean
theorem Filter.Eventually.intCast_atBot [StrictOrderedRing R] [Archimedean R] {p : R → Prop}
    (h : ∀ᶠ (x : R) in atBot, p x) : ∀ᶠ (n : ℤ) in atBot, p n

Proof state:
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atBot, p x
⊢ ∀ᶠ (n : ℤ) in Filter.comap Int.cast atBot, p ↑n

Tactic:
exact h.comap _

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atBot, p x
⊢ ∀ᶠ (n : ℤ) in atBot, p ↑n

Tactic:
rw [← Int.comap_cast_atBot (R := R)]

Result:
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atBot, p x
⊢ ∀ᶠ (n : ℤ) in Filter.comap Int.cast atBot, p ↑n
-- Mathlib/Data/List/Intervals.lean
theorem filter_lt (n m l : ℕ) :
    ((Ico n m).filter fun x => x < l) = Ico n (min m l)

Proof state:
case inr
n m l : ℕ
hlm : l ≤ m
⊢ filter (fun x => decide (x < l)) (Ico n m) = Ico n (m ⊓ l)

Tactic:
rw [min_eq_right hlm, filter_lt_of_ge hlm]

Result:
no goals

Proof state:
case inl
n m l : ℕ
hml : m ≤ l
⊢ filter (fun x => decide (x < l)) (Ico n m) = Ico n (m ⊓ l)

Tactic:
rw [min_eq_left hml, filter_lt_of_top_le hml]

Result:
no goals

Proof state:
n m l : ℕ
⊢ filter (fun x => decide (x < l)) (Ico n m) = Ico n (m ⊓ l)

Tactic:
rcases le_total m l with hml | hlm

Result:
case inl
n m l : ℕ
hml : m ≤ l
⊢ filter (fun x => decide (x < l)) (Ico n m) = Ico n (m ⊓ l)

case inr
n m l : ℕ
hlm : l ≤ m
⊢ filter (fun x => decide (x < l)) (Ico n m) = Ico n (m ⊓ l)
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem IsCompact.locallyCompactSpace_of_mem_nhds_of_group {K : Set G} (hK : IsCompact K) {x : G}
    (h : K ∈ 𝓝 x) : LocallyCompactSpace G

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
⊢ WeaklyLocallyCompactSpace G

Tactic:
refine ⟨fun y ↦ ⟨(y * x⁻¹) • K, ?_, ?_⟩⟩

Result:
case refine_1
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
y : G
⊢ IsCompact ((y * x⁻¹) • K)

case refine_2
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
y : G
⊢ (y * x⁻¹) • K ∈ 𝓝 y

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
y : G
⊢ K ∈ 𝓝 ((y * x⁻¹)⁻¹ • y)

Tactic:
simpa using h

Result:
no goals

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
⊢ LocallyCompactSpace G

Tactic:
suffices WeaklyLocallyCompactSpace G from inferInstance

Result:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
⊢ WeaklyLocallyCompactSpace G

Proof state:
case refine_1
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
y : G
⊢ IsCompact ((y * x⁻¹) • K)

Tactic:
exact hK.smul _

Result:
no goals

Proof state:
case refine_2
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
y : G
⊢ (y * x⁻¹) • K ∈ 𝓝 y

Tactic:
rw [← preimage_smul_inv]

Result:
case refine_2
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
y : G
⊢ (fun x_1 => (y * x⁻¹)⁻¹ • x_1) ⁻¹' K ∈ 𝓝 y

Proof state:
case refine_2
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
x : G
h : K ∈ 𝓝 x
y : G
⊢ (fun x_1 => (y * x⁻¹)⁻¹ • x_1) ⁻¹' K ∈ 𝓝 y

Tactic:
exact (continuous_const_smul _).continuousAt.preimage_mem_nhds (by simpa using h)

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem _root_.Bornology.IsBounded.cthickening {α : Type*} [PseudoMetricSpace α] {δ : ℝ} {E : Set α}
    (h : IsBounded E) : IsBounded (cthickening δ E)

Proof state:
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
h : Bornology.IsBounded E
this : Bornology.IsBounded (thickening ((δ + 1) ⊔ 1) E)
⊢ Bornology.IsBounded (Metric.cthickening δ E)

Tactic:
apply this.subset

Result:
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
h : Bornology.IsBounded E
this : Bornology.IsBounded (thickening ((δ + 1) ⊔ 1) E)
⊢ Metric.cthickening δ E ⊆ thickening ((δ + 1) ⊔ 1) E

Proof state:
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
h : Bornology.IsBounded E
this : Bornology.IsBounded (thickening ((δ + 1) ⊔ 1) E)
⊢ Metric.cthickening δ E ⊆ thickening ((δ + 1) ⊔ 1) E

Tactic:
exact cthickening_subset_thickening' (zero_lt_one.trans_le (le_max_right _ _))
  ((lt_add_one _).trans_le (le_max_left _ _)) _

Result:
no goals

Proof state:
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
h : Bornology.IsBounded E
⊢ Bornology.IsBounded (Metric.cthickening δ E)

Tactic:
have : IsBounded (thickening (max (δ + 1) 1) E) := h.thickening

Result:
α : Type u_2
inst✝ : PseudoMetricSpace α
δ : ℝ
E : Set α
h : Bornology.IsBounded E
this : Bornology.IsBounded (thickening ((δ + 1) ⊔ 1) E)
⊢ Bornology.IsBounded (Metric.cthickening δ E)
-- Mathlib/Analysis/Calculus/Deriv/Slope.lean
lemma HasDerivAt.continuousAt_div [DecidableEq 𝕜] {f : 𝕜 → 𝕜} {c a : 𝕜} (hf : HasDerivAt f a c) :
    ContinuousAt (Function.update (fun x ↦ (f x - f c) / (x - c)) c a) c

Proof state:
𝕜 : Type u
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : DecidableEq 𝕜
f : 𝕜 → 𝕜
c a : 𝕜
hf : HasDerivAt f a c
⊢ ContinuousAt (Function.update (slope f c) c a) c

Tactic:
exact continuousAt_update_same.mpr <| hasDerivAt_iff_tendsto_slope.mp hf

Result:
no goals

Proof state:
𝕜 : Type u
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : DecidableEq 𝕜
f : 𝕜 → 𝕜
c a : 𝕜
hf : HasDerivAt f a c
⊢ ContinuousAt (Function.update (fun x => (f x - f c) / (x - c)) c a) c

Tactic:
rw [← slope_fun_def_field]

Result:
𝕜 : Type u
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : DecidableEq 𝕜
f : 𝕜 → 𝕜
c a : 𝕜
hf : HasDerivAt f a c
⊢ ContinuousAt (Function.update (slope f c) c a) c
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem left_le_opow (a : Ordinal) {b : Ordinal} (b1 : 0 < b) : a ≤ a ^ b

Proof state:
case inl.inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a = 0
⊢ 0 ≤ 0 ^ b

Tactic:
exact Ordinal.zero_le _

Result:
no goals

Proof state:
case inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
⊢ a ^ 1 ≤ a ^ b

Tactic:
rcases lt_or_eq_of_le a1 with a0 | a1

Result:
case inl.inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a < 1
⊢ a ^ 1 ≤ a ^ b

case inl.inr
a b : Ordinal.{u_1}
b1 : 0 < b
a1✝ : a ≤ 1
a1 : a = 1
⊢ a ^ 1 ≤ a ^ b

Proof state:
case inl.inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a = 0
⊢ a ^ 1 ≤ a ^ b

Tactic:
rw [a0, zero_opow Ordinal.one_ne_zero]

Result:
case inl.inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a = 0
⊢ 0 ≤ 0 ^ b

Proof state:
case inl.inr
a b : Ordinal.{u_1}
b1 : 0 < b
a1✝ : a ≤ 1
a1 : a = 1
⊢ a ^ 1 ≤ a ^ b

Tactic:
rw [a1, one_opow, one_opow]

Result:
no goals

Proof state:
case inl.inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a < 1
⊢ a ^ 1 ≤ a ^ b

Tactic:
rw [lt_one_iff_zero] at a0

Result:
case inl.inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
a0 : a = 0
⊢ a ^ 1 ≤ a ^ b

Proof state:
case inr
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a > 1
⊢ a ^ 1 ≤ a ^ b

Tactic:
rwa [opow_le_opow_iff_right a1, one_le_iff_pos]

Result:
no goals

Proof state:
a b : Ordinal.{u_1}
b1 : 0 < b
⊢ a ^ 1 ≤ a ^ b

Tactic:
rcases le_or_gt a 1 with a1 | a1

Result:
case inl
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a ≤ 1
⊢ a ^ 1 ≤ a ^ b

case inr
a b : Ordinal.{u_1}
b1 : 0 < b
a1 : a > 1
⊢ a ^ 1 ≤ a ^ b

Proof state:
a b : Ordinal.{u_1}
b1 : 0 < b
⊢ a ≤ a ^ b

Tactic:
nth_rw 1 [← opow_one a]

Result:
a b : Ordinal.{u_1}
b1 : 0 < b
⊢ a ^ 1 ≤ a ^ b
-- Mathlib/Probability/Variance.lean
/-- **Popoviciu's inequality on variance**

The variance of a random variable `X` satisfying `a ≤ X ≤ b` almost everywhere is at most
`((b - a) / 2) ^ 2`. -/
lemma variance_le_sq_of_bounded [IsProbabilityMeasure μ] {a b : ℝ} {X : Ω → ℝ}
    (h : ∀ᵐ ω ∂μ, X ω ∈ Set.Icc a b) (hX : AEMeasurable X μ) :
    variance X μ ≤ ((b - a) / 2) ^ 2 :=
  calc
    _ ≤ (b - μ[X]) * (μ[X] - a) := variance_le_sub_mul_sub h hX
    _ = ((b - a) / 2) ^ 2 - (μ[X] - (b + a) / 2) ^ 2

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
a b : ℝ
X : Ω → ℝ
h : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hX : AEMeasurable X μ
⊢ (b - ∫ (x : Ω), X x ∂μ) * (∫ (x : Ω), X x ∂μ - a) = ((b - a) / 2) ^ 2 - (∫ (x : Ω), X x ∂μ - (b + a) / 2) ^ 2

Tactic:
ring

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_eq_zero : ⌊a⌋₊ = 0 ↔ a < 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
⊢ ⌊a⌋₊ = 0 ↔ a < 1

Tactic:
rw [← lt_one_iff, ← @cast_one α]

Result:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
⊢ ⌊a⌋₊ < 1 ↔ a < ↑1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
⊢ ⌊a⌋₊ < 1 ↔ a < ↑1

Tactic:
exact floor_lt' Nat.one_ne_zero

Result:
no goals
-- Mathlib/GroupTheory/PushoutI.lean
theorem hom_ext_nonempty [hn : Nonempty ι]
    {f g : PushoutI φ →* K}
    (h : ∀ i, f.comp (of i : G i →* _) = g.comp (of i : G i →* _)) : f = g :=
  hom_ext h <| by
    cases hn with
    | intro i =>
      ext
      rw [← of_comp_eq_base i, ← MonoidHom.comp_assoc, h, MonoidHom.comp_assoc]

Proof state:
case intro
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
f g : PushoutI φ →* K
h : ∀ (i : ι), f.comp (of i) = g.comp (of i)
i : ι
⊢ f.comp (base φ) = g.comp (base φ)

Tactic:
ext

Result:
case intro.h
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
f g : PushoutI φ →* K
h : ∀ (i : ι), f.comp (of i) = g.comp (of i)
i : ι
x✝ : H
⊢ (f.comp (base φ)) x✝ = (g.comp (base φ)) x✝

Proof state:
case intro.h
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
f g : PushoutI φ →* K
h : ∀ (i : ι), f.comp (of i) = g.comp (of i)
i : ι
x✝ : H
⊢ (f.comp (base φ)) x✝ = (g.comp (base φ)) x✝

Tactic:
rw [← of_comp_eq_base i, ← MonoidHom.comp_assoc, h, MonoidHom.comp_assoc]

Result:
no goals

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
hn : Nonempty ι
f g : PushoutI φ →* K
h : ∀ (i : ι), f.comp (of i) = g.comp (of i)
⊢ f.comp (base φ) = g.comp (base φ)

Tactic:
cases hn with
| intro i =>
  ext
  rw [← of_comp_eq_base i, ← MonoidHom.comp_assoc, h, MonoidHom.comp_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem eq_not : ∀ {a b : Bool}, (a = (!b)) ↔ (a ≠ b)

Proof state:
⊢ ∀ {a b : Bool}, a = !b ↔ a ≠ b

Tactic:
decide

Result:
no goals
-- Mathlib/Data/Multiset/MapFold.lean
lemma erase_attach_map (s : Multiset α) (f : α → β) (x : {x // x ∈ s}) :
    (s.attach.erase x).map (fun j : {x // x ∈ s} ↦ f j) = (s.erase x).map f

Proof state:
α : Type u_1
β : Type v
inst✝ : DecidableEq α
s : Multiset α
f : α → β
x : { x // x ∈ s }
⊢ map (fun j => f ↑j) (s.attach.erase x) = map f (s.erase ↑x)

Tactic:
simp only [← Function.comp_apply (f := f)]

Result:
α : Type u_1
β : Type v
inst✝ : DecidableEq α
s : Multiset α
f : α → β
x : { x // x ∈ s }
⊢ map (fun x => (f ∘ val) x) (s.attach.erase x) = map f (s.erase ↑x)

Proof state:
α : Type u_1
β : Type v
inst✝ : DecidableEq α
s : Multiset α
f : α → β
x : { x // x ∈ s }
⊢ map (fun x => (f ∘ val) x) (s.attach.erase x) = map f (s.erase ↑x)

Tactic:
rw [← map_map, erase_attach_map_val]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Addition.lean
theorem support_neg {x : HahnSeries Γ R} : (-x).support = x.support

Proof state:
case h
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddGroup R
x : HahnSeries Γ R
x✝ : Γ
⊢ x✝ ∈ (-x).support ↔ x✝ ∈ x.support

Tactic:
simp

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddGroup R
x : HahnSeries Γ R
⊢ (-x).support = x.support

Tactic:
ext

Result:
case h
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddGroup R
x : HahnSeries Γ R
x✝ : Γ
⊢ x✝ ∈ (-x).support ↔ x✝ ∈ x.support
-- Mathlib/RingTheory/Polynomial/IntegralNormalization.lean
theorem leadingCoeff_smul_integralNormalization (p : S[X]) :
    p.leadingCoeff • integralNormalization p = scaleRoots p p.leadingCoeff

Proof state:
S : Type v
inst✝ : CommSemiring S
p : S[X]
⊢ p.leadingCoeff • p.integralNormalization = p.scaleRoots p.leadingCoeff

Tactic:
rw [Algebra.smul_def, algebraMap_eq, mul_comm, integralNormalization_mul_C_leadingCoeff]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
theorem tendsto_comp_exp_atBot {f : ℝ → α} :
    Tendsto (fun x => f (exp x)) atBot l ↔ Tendsto f (𝓝[>] 0) l

Proof state:
α : Type u_1
l : Filter α
f : ℝ → α
⊢ Tendsto (fun x => f (rexp x)) atBot l ↔ Tendsto (f ∘ rexp) atBot l

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
l : Filter α
f : ℝ → α
⊢ Tendsto (fun x => f (rexp x)) atBot l ↔ Tendsto f (𝓝[>] 0) l

Tactic:
rw [← map_exp_atBot, tendsto_map'_iff]

Result:
α : Type u_1
l : Filter α
f : ℝ → α
⊢ Tendsto (fun x => f (rexp x)) atBot l ↔ Tendsto (f ∘ rexp) atBot l
-- Mathlib/RingTheory/Ideal/Maximal.lean
theorem IsMaximal.exists_inv {I : Ideal α} (hI : I.IsMaximal) {x} (hx : x ∉ I) :
    ∃ y, ∃ i ∈ I, y * x + i = 1

Proof state:
case intro.intro.intro.intro
α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsMaximal
x : α
hx : x ∉ I
H₁ : 1 ∉ I
H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
y z : α
hz : z ∈ span ↑I
hy : 1 = y * x + z
⊢ z ∈ I

Tactic:
rwa [← span_eq I]

Result:
no goals

Proof state:
case intro
α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsMaximal
x : α
hx : x ∉ I
H₁ : 1 ∉ I
H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
⊢ ∃ y, ∃ i ∈ I, y * x + i = 1

Tactic:
rcases mem_span_insert.1
    (H₂ (span (insert x I)) x (Set.Subset.trans (subset_insert _ _) subset_span) hx
      (subset_span (mem_insert _ _))) with
  ⟨y, z, hz, hy⟩

Result:
case intro.intro.intro.intro
α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsMaximal
x : α
hx : x ∉ I
H₁ : 1 ∉ I
H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
y z : α
hz : z ∈ span ↑I
hy : 1 = y * x + z
⊢ ∃ y, ∃ i ∈ I, y * x + i = 1

Proof state:
α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsMaximal
x : α
hx : x ∉ I
⊢ ∃ y, ∃ i ∈ I, y * x + i = 1

Tactic:
obtain ⟨H₁, H₂⟩ := isMaximal_iff.1 hI

Result:
case intro
α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsMaximal
x : α
hx : x ∉ I
H₁ : 1 ∉ I
H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
⊢ ∃ y, ∃ i ∈ I, y * x + i = 1

Proof state:
case intro.intro.intro.intro
α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsMaximal
x : α
hx : x ∉ I
H₁ : 1 ∉ I
H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
y z : α
hz : z ∈ span ↑I
hy : 1 = y * x + z
⊢ ∃ y, ∃ i ∈ I, y * x + i = 1

Tactic:
refine ⟨y, z, ?_, hy.symm⟩

Result:
case intro.intro.intro.intro
α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsMaximal
x : α
hx : x ∉ I
H₁ : 1 ∉ I
H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
y z : α
hz : z ∈ span ↑I
hy : 1 = y * x + z
⊢ z ∈ I
-- Mathlib/CategoryTheory/MorphismProperty/RetractArgument.lean
lemma rlp_eq_of_le_rlp_of_hasFactorization_of_isStableUnderRetracts
    [HasFactorization W₁ W₂] [W₂.IsStableUnderRetracts] (h₂ : W₂ ≤ W₁.rlp) :
    W₁.rlp = W₂ :=
  le_antisymm (fun X Y p hp ↦ by
    have h := factorizationData W₁ W₂ p
    have := hp _ h.hi
    simpa using of_retract (RetractArrow.ofRightLiftingProperty h.fac) h.hp) h₂

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
W₁ W₂ : MorphismProperty C
inst✝¹ : W₁.HasFactorization W₂
inst✝ : W₂.IsStableUnderRetracts
h₂ : W₂ ≤ W₁.rlp
X Y : C
p : X ⟶ Y
hp : W₁.rlp p
⊢ W₂ p

Tactic:
have h := factorizationData W₁ W₂ p

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
W₁ W₂ : MorphismProperty C
inst✝¹ : W₁.HasFactorization W₂
inst✝ : W₂.IsStableUnderRetracts
h₂ : W₂ ≤ W₁.rlp
X Y : C
p : X ⟶ Y
hp : W₁.rlp p
h : W₁.MapFactorizationData W₂ p
⊢ W₂ p

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
W₁ W₂ : MorphismProperty C
inst✝¹ : W₁.HasFactorization W₂
inst✝ : W₂.IsStableUnderRetracts
h₂ : W₂ ≤ W₁.rlp
X Y : C
p : X ⟶ Y
hp : W₁.rlp p
h : W₁.MapFactorizationData W₂ p
⊢ W₂ p

Tactic:
have := hp _ h.hi

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
W₁ W₂ : MorphismProperty C
inst✝¹ : W₁.HasFactorization W₂
inst✝ : W₂.IsStableUnderRetracts
h₂ : W₂ ≤ W₁.rlp
X Y : C
p : X ⟶ Y
hp : W₁.rlp p
h : W₁.MapFactorizationData W₂ p
this : HasLiftingProperty h.i p
⊢ W₂ p

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
W₁ W₂ : MorphismProperty C
inst✝¹ : W₁.HasFactorization W₂
inst✝ : W₂.IsStableUnderRetracts
h₂ : W₂ ≤ W₁.rlp
X Y : C
p : X ⟶ Y
hp : W₁.rlp p
h : W₁.MapFactorizationData W₂ p
this : HasLiftingProperty h.i p
⊢ W₂ p

Tactic:
simpa using of_retract (RetractArrow.ofRightLiftingProperty h.fac) h.hp

Result:
no goals
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
theorem star_adjoin_comm (s : Set A) :
    star (NonUnitalAlgebra.adjoin R s) = NonUnitalAlgebra.adjoin R (star s) :=
  have this :
    ∀ t : Set A, NonUnitalAlgebra.adjoin R (star t) ≤ star (NonUnitalAlgebra.adjoin R t) := fun _ =>
    NonUnitalAlgebra.adjoin_le fun _ hx => NonUnitalAlgebra.subset_adjoin R hx
  le_antisymm (by simpa only [star_star] using NonUnitalSubalgebra.star_mono (this (star s)))
    (this s)

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
this : ∀ (t : Set A), NonUnitalAlgebra.adjoin R (star t) ≤ star (NonUnitalAlgebra.adjoin R t)
⊢ star (NonUnitalAlgebra.adjoin R s) ≤ NonUnitalAlgebra.adjoin R (star s)

Tactic:
simpa only [star_star] using NonUnitalSubalgebra.star_mono (this (star s))

Result:
no goals
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nadd_nat (n : ℕ) : a ♯ n = a + n

Proof state:
case zero
a : Ordinal.{u}
⊢ a ♯ ↑0 = a + ↑0

Tactic:
simp

Result:
no goals

Proof state:
a : Ordinal.{u}
n : ℕ
⊢ a ♯ ↑n = a + ↑n

Tactic:
induction' n with n hn

Result:
case zero
a : Ordinal.{u}
⊢ a ♯ ↑0 = a + ↑0

case succ
a : Ordinal.{u}
n : ℕ
hn : a ♯ ↑n = a + ↑n
⊢ a ♯ ↑(n + 1) = a + ↑(n + 1)

Proof state:
case succ
a : Ordinal.{u}
n : ℕ
hn : a ♯ ↑n = a + ↑n
⊢ a ♯ ↑(n + 1) = a + ↑(n + 1)

Tactic:
rw [Nat.cast_succ, add_one_eq_succ, nadd_succ, add_succ, hn]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean
protected lemma le_def : p ≤ q ↔ p.num * q.den ≤ q.num * p.den

Proof state:
p q : ℚ
⊢ p ≤ q ↔ p.num * ↑q.den ≤ q.num * ↑p.den

Tactic:
rw [← num_divInt_den q, ← num_divInt_den p]

Result:
p q : ℚ
⊢ p.num /. ↑p.den ≤ q.num /. ↑q.den ↔
    (p.num /. ↑p.den).num * ↑(q.num /. ↑q.den).den ≤ (q.num /. ↑q.den).num * ↑(p.num /. ↑p.den).den

Proof state:
p q : ℚ
⊢ p.num /. ↑p.den ≤ q.num /. ↑q.den ↔
    (p.num /. ↑p.den).num * ↑(q.num /. ↑q.den).den ≤ (q.num /. ↑q.den).num * ↑(p.num /. ↑p.den).den

Tactic:
conv_rhs => simp only [num_divInt_den]

Result:
p q : ℚ
⊢ p.num /. ↑p.den ≤ q.num /. ↑q.den ↔ p.num * ↑q.den ≤ q.num * ↑p.den

Proof state:
p q : ℚ
⊢ p.num /. ↑p.den ≤ q.num /. ↑q.den ↔ p.num * ↑q.den ≤ q.num * ↑p.den

Tactic:
exact Rat.divInt_le_divInt (mod_cast p.pos) (mod_cast q.pos)

Result:
no goals
-- Mathlib/Algebra/Ring/Subring/IntPolynomial.lean
theorem int_eval₂_eq (x : L) :
    eval₂ (algebraMap R L) x (P.int R hP) = aeval x P

Proof state:
K : Type u_1
inst✝² : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
n : ℕ
x✝ : n ∈ Finset.range (P.natDegree + 1)
⊢ (algebraMap (↥R) L) ((int R P hP).coeff n) * x ^ n = P.coeff n • x ^ n

Tactic:
rw [Algebra.smul_def]

Result:
K : Type u_1
inst✝² : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
n : ℕ
x✝ : n ∈ Finset.range (P.natDegree + 1)
⊢ (algebraMap (↥R) L) ((int R P hP).coeff n) * x ^ n = (algebraMap K L) (P.coeff n) * x ^ n

Proof state:
K : Type u_1
inst✝² : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
⊢ eval₂ (algebraMap (↥R) L) x (int R P hP) = (aeval x) P

Tactic:
rw [aeval_eq_sum_range, eval₂_eq_sum_range]

Result:
K : Type u_1
inst✝² : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
⊢ ∑ i ∈ Finset.range ((int R P hP).natDegree + 1), (algebraMap (↥R) L) ((int R P hP).coeff i) * x ^ i =
    ∑ i ∈ Finset.range (P.natDegree + 1), P.coeff i • x ^ i

Proof state:
K : Type u_1
inst✝² : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
⊢ ∑ i ∈ Finset.range ((int R P hP).natDegree + 1), (algebraMap (↥R) L) ((int R P hP).coeff i) * x ^ i =
    ∑ i ∈ Finset.range (P.natDegree + 1), P.coeff i • x ^ i

Tactic:
exact Finset.sum_congr rfl (fun n _ => by rw [Algebra.smul_def]; rfl)

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
R : Subring K
P : K[X]
hP : ∀ (n : ℕ), P.coeff n ∈ R
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
n : ℕ
x✝ : n ∈ Finset.range (P.natDegree + 1)
⊢ (algebraMap (↥R) L) ((int R P hP).coeff n) * x ^ n = (algebraMap K L) (P.coeff n) * x ^ n

Tactic:
rfl

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Density.lean
theorem swap_mem_interedges_iff (hr : Symmetric r) {x : α × α} :
    x.swap ∈ interedges r s t ↔ x ∈ interedges r t s

Proof state:
α : Type u_4
r : α → α → Prop
inst✝ : DecidableRel r
s t : Finset α
hr : Symmetric r
x : α × α
⊢ x.swap ∈ interedges r s t ↔ x ∈ interedges r t s

Tactic:
rw [mem_interedges_iff, mem_interedges_iff, hr.iff]

Result:
α : Type u_4
r : α → α → Prop
inst✝ : DecidableRel r
s t : Finset α
hr : Symmetric r
x : α × α
⊢ x.swap.1 ∈ s ∧ x.swap.2 ∈ t ∧ r x.swap.2 x.swap.1 ↔ x.1 ∈ t ∧ x.2 ∈ s ∧ r x.1 x.2

Proof state:
α : Type u_4
r : α → α → Prop
inst✝ : DecidableRel r
s t : Finset α
hr : Symmetric r
x : α × α
⊢ x.swap.1 ∈ s ∧ x.swap.2 ∈ t ∧ r x.swap.2 x.swap.1 ↔ x.1 ∈ t ∧ x.2 ∈ s ∧ r x.1 x.2

Tactic:
exact and_left_comm

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem gcd_mul_left_add_right (m n k : ℕ) : gcd m (m * k + n) = gcd m n

Proof state:
m n k : ℕ
⊢ m.gcd (m * k + n) = m.gcd n

Tactic:
simp [add_comm _ n]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Bernstein.lean
theorem bernstein_apply (n ν : ℕ) (x : I) :
    bernstein n ν x = (n.choose ν : ℝ) * (x : ℝ) ^ ν * (1 - (x : ℝ)) ^ (n - ν)

Proof state:
n ν : ℕ
x : ↑I
⊢ Polynomial.eval (↑x) (↑(n.choose ν) * Polynomial.X ^ ν * (1 - Polynomial.X) ^ (n - ν)) =
    ↑(n.choose ν) * ↑x ^ ν * (1 - ↑x) ^ (n - ν)

Tactic:
simp

Result:
no goals

Proof state:
n ν : ℕ
x : ↑I
⊢ (bernstein n ν) x = ↑(n.choose ν) * ↑x ^ ν * (1 - ↑x) ^ (n - ν)

Tactic:
dsimp [bernstein, Polynomial.toContinuousMapOn, Polynomial.toContinuousMap, bernsteinPolynomial]

Result:
n ν : ℕ
x : ↑I
⊢ Polynomial.eval (↑x) (↑(n.choose ν) * Polynomial.X ^ ν * (1 - Polynomial.X) ^ (n - ν)) =
    ↑(n.choose ν) * ↑x ^ ν * (1 - ↑x) ^ (n - ν)