harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/NoncommPiCoprod.lean
theorem noncommPiCoprod_range [Fintype ι]
    {hcomm : Pairwise fun i j : ι => ∀ (x : H i) (y : H j), Commute (ϕ i x) (ϕ j y)} :
    (noncommPiCoprod ϕ hcomm).range = ⨆ i : ι, (ϕ i).range

Proof state:
G : Type u_1
inst✝² : Group G
ι : Type u_2
H : ι → Type u_3
inst✝¹ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
inst✝ : Fintype ι
hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
⊢ (noncommPiCoprod ϕ hcomm).range = ⨆ i, (ϕ i).range

Tactic:
letI := Classical.decEq ι

Result:
G : Type u_1
inst✝² : Group G
ι : Type u_2
H : ι → Type u_3
inst✝¹ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
inst✝ : Fintype ι
hcomm : Pairwise fun i j => ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
this : DecidableEq ι := Classical.decEq ι
⊢ (noncommPiCoprod ϕ hcomm).range = ⨆ i, (ϕ i).range
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem opow_zero (a : Ordinal) : a ^ (0 : Ordinal) = 1

Proof state:
case inl

⊢ 0 ^ 0 = 1

Tactic:
rw [zero_opow', Ordinal.sub_zero]

Result:
no goals

Proof state:
case inr
a : Ordinal.{u_1}
h : a ≠ 0
⊢ a ^ 0 = 1

Tactic:
rw [opow_of_ne_zero h, limitRecOn_zero]

Result:
no goals

Proof state:
a : Ordinal.{u_1}
⊢ a ^ 0 = 1

Tactic:
obtain rfl | h := eq_or_ne a 0

Result:
case inl

⊢ 0 ^ 0 = 1

case inr
a : Ordinal.{u_1}
h : a ≠ 0
⊢ a ^ 0 = 1
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
theorem getElem?_zero_mul_tail_prod (l : List M) : l[0]?.getD 1 * l.tail.prod = l.prod

Proof state:
M : Type u_4
inst✝ : Monoid M
l : List M
⊢ l[0]?.getD 1 * l.tail.prod = l.prod

Tactic:
cases l <;> simp

Result:
no goals
-- Mathlib/CategoryTheory/Closed/Cartesian.lean
theorem pre_id (A : C) [Exponentiable A] : pre (𝟙 A) = 𝟙 _

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ChosenFiniteProducts C
A : C
inst✝ : Exponentiable A
⊢ (conjugateEquiv (exp.adjunction A) (exp.adjunction A)) (𝟙 ((tensoringLeft C).obj A)) = 𝟙 (exp A)

Tactic:
aesop_cat

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ChosenFiniteProducts C
A : C
inst✝ : Exponentiable A
⊢ pre (𝟙 A) = 𝟙 (exp A)

Tactic:
simp only [pre, Functor.map_id]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ChosenFiniteProducts C
A : C
inst✝ : Exponentiable A
⊢ (conjugateEquiv (exp.adjunction A) (exp.adjunction A)) (𝟙 ((tensoringLeft C).obj A)) = 𝟙 (exp A)
-- Mathlib/Algebra/Homology/BifunctorAssociator.lean
@[reassoc (attr := simp)]
lemma ι_D₃  :
    ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h ≫ D₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' =
      d₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'

Proof state:
case neg
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_5
C₄ : Type u_6
inst✝¹⁹ : Category.{u_17, u_1} C₁
inst✝¹⁸ : Category.{u_16, u_2} C₂
inst✝¹⁷ : Category.{u_14, u_5} C₃
inst✝¹⁶ : Category.{u_13, u_6} C₄
inst✝¹⁵ : Category.{u_15, u_3} C₁₂
inst✝¹⁴ : HasZeroMorphisms C₁
inst✝¹³ : HasZeroMorphisms C₂
inst✝¹² : HasZeroMorphisms C₃
inst✝¹¹ : Preadditive C₁₂
inst✝¹⁰ : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
inst✝⁹ : F₁₂.PreservesZeroMorphisms
inst✝⁸ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝⁷ : G.Additive
inst✝⁶ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst✝⁵ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : TotalComplexShape c₁₂ c₃ c₄
inst✝² : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝¹ : DecidableEq ι₁₂
inst✝ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j j' : ι₄
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
h₁ : c₃.Rel i₃ (c₃.next i₃)
h₂ : ¬c₁₂.π c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), c₃.next i₃) = j'
⊢ (G.map (K₁.ιMapBifunctor K₂ F₁₂ c₁₂ i₁ i₂ (c₁.π c₂ c₁₂ (i₁, i₂)) ⋯)).app (K₃.X i₃) ≫
      mapBifunctor.d₂ (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄ (c₁.π c₂ c₁₂ (i₁, i₂)) i₃ j' =
    c₁₂.ε₂ c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃) •
      (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).map (K₃.d i₃ (c₃.next i₃)) ≫
        ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ (c₃.next i₃) j'

Tactic:
rw [mapBifunctor.d₂_eq_zero' _ _ _ _ _ h₁ _ h₂, comp_zero,
  ιOrZero_eq_zero _ _ _ _ _ _ _ _ _ _ _ h₂, comp_zero, smul_zero]

Result:
no goals
-- Mathlib/NumberTheory/BernoulliPolynomials.lean
theorem derivative_bernoulli_add_one (k : ℕ) :
    Polynomial.derivative (bernoulli (k + 1)) = (k + 1) * bernoulli k

Proof state:
k m : ℕ
x✝ : m ∈ range (k + 1)
⊢ (monomial (k - m)) (_root_.bernoulli m * ↑((k + 1).choose m * (k + 1 - m))) =
    (monomial (k - m)) (_root_.bernoulli m * ↑(k.choose m * (k + 1)))

Tactic:
congr 3

Result:
case h.e_6.h.e_a.e_a
k m : ℕ
x✝ : m ∈ range (k + 1)
⊢ (k + 1).choose m * (k + 1 - m) = k.choose m * (k + 1)

Proof state:
k m : ℕ
x✝ : m ∈ range (k + 1)
⊢ (monomial (k - m)) (_root_.bernoulli m * ↑((k + 1).choose m) * ↑(k + 1 - m)) =
    (↑k + 1) * (monomial (k - m)) (_root_.bernoulli m * ↑(k.choose m))

Tactic:
conv_rhs => rw [← Nat.cast_one, ← Nat.cast_add, ← C_eq_natCast, C_mul_monomial, mul_comm]

Result:
k m : ℕ
x✝ : m ∈ range (k + 1)
⊢ (monomial (k - m)) (_root_.bernoulli m * ↑((k + 1).choose m) * ↑(k + 1 - m)) =
    (monomial (k - m)) (_root_.bernoulli m * ↑(k.choose m) * ↑(k + 1))

Proof state:
k : ℕ
⊢ range (k + 1) = range (k + 1)

Tactic:
rfl

Result:
no goals

Proof state:
k : ℕ
⊢ ∑ x ∈ range (k + 1 + 1), (monomial (k - x)) (_root_.bernoulli x * ↑((k + 1).choose x) * ↑(k + 1 - x)) =
    (↑k + 1) * ∑ i ∈ range (k + 1), (monomial (k - i)) (_root_.bernoulli i * ↑(k.choose i))

Tactic:
rw [range_add_one, sum_insert not_mem_range_self, tsub_self, cast_zero, mul_zero,
  map_zero, zero_add, mul_sum]

Result:
k : ℕ
⊢ ∑ x ∈ range (k + 1), (monomial (k - x)) (_root_.bernoulli x * ↑((k + 1).choose x) * ↑(k + 1 - x)) =
    ∑ i ∈ range (k + 1), (↑k + 1) * (monomial (k - i)) (_root_.bernoulli i * ↑(k.choose i))

Proof state:
case h.e_6.h.e_a.e_a
k m : ℕ
x✝ : m ∈ range (k + 1)
⊢ (k + 1).choose m * (k + 1 - m) = k.choose m * (k + 1)

Tactic:
rw [(choose_mul_succ_eq k m).symm]

Result:
no goals

Proof state:
k : ℕ
⊢ ∑ x ∈ range (k + 1), (monomial (k - x)) (_root_.bernoulli x * ↑((k + 1).choose x) * ↑(k + 1 - x)) =
    ∑ i ∈ range (k + 1), (↑k + 1) * (monomial (k - i)) (_root_.bernoulli i * ↑(k.choose i))

Tactic:
refine sum_congr (by rfl) fun m _ => ?_

Result:
k m : ℕ
x✝ : m ∈ range (k + 1)
⊢ (monomial (k - m)) (_root_.bernoulli m * ↑((k + 1).choose m) * ↑(k + 1 - m)) =
    (↑k + 1) * (monomial (k - m)) (_root_.bernoulli m * ↑(k.choose m))

Proof state:
k m : ℕ
x✝ : m ∈ range (k + 1)
⊢ (monomial (k - m)) (_root_.bernoulli m * ↑((k + 1).choose m) * ↑(k + 1 - m)) =
    (monomial (k - m)) (_root_.bernoulli m * ↑(k.choose m) * ↑(k + 1))

Tactic:
rw [mul_assoc, mul_assoc, ← Nat.cast_mul, ← Nat.cast_mul]

Result:
k m : ℕ
x✝ : m ∈ range (k + 1)
⊢ (monomial (k - m)) (_root_.bernoulli m * ↑((k + 1).choose m * (k + 1 - m))) =
    (monomial (k - m)) (_root_.bernoulli m * ↑(k.choose m * (k + 1)))

Proof state:
k : ℕ
⊢ derivative (bernoulli (k + 1)) = (↑k + 1) * bernoulli k

Tactic:
simp_rw [bernoulli, derivative_sum, derivative_monomial, Nat.sub_sub, Nat.add_sub_add_right]

Result:
k : ℕ
⊢ ∑ x ∈ range (k + 1 + 1), (monomial (k - x)) (_root_.bernoulli x * ↑((k + 1).choose x) * ↑(k + 1 - x)) =
    (↑k + 1) * ∑ i ∈ range (k + 1), (monomial (k - i)) (_root_.bernoulli i * ↑(k.choose i))
-- Mathlib/Probability/Independence/Kernel.lean
theorem iIndepFun.indepFun_finset (S T : Finset ι) (hST : Disjoint S T)
    (hf_Indep : iIndepFun m f κ μ) (hf_meas : ∀ i, Measurable (f i)) :
    IndepFun (fun a (i : S) => f i a) (fun a (i : T) => f i a) κ μ

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun m f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᶠ[ae μ] ⇑η
hη : IsMarkovKernel η
πSβ : Set (Set ((i : { x // x ∈ S }) → β ↑i)) := univ.pi '' univ.pi fun i => {s | MeasurableSet s}
πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i => f (↑i) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
⊢ MeasurableSpace.comap (fun a i => f (↑i) a) MeasurableSpace.pi = generateFrom πS

Tactic:
rw [generateFrom_pi.symm, comap_generateFrom]

Result:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun m f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᶠ[ae μ] ⇑η
hη : IsMarkovKernel η
πSβ : Set (Set ((i : { x // x ∈ S }) → β ↑i)) := univ.pi '' univ.pi fun i => {s | MeasurableSet s}
πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i => f (↑i) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
⊢ generateFrom ((preimage fun a i => f (↑i) a) '' (univ.pi '' univ.pi fun i => {s | MeasurableSet s})) = generateFrom πS
-- Mathlib/Probability/Independence/Kernel.lean
theorem iIndepFun.indepFun_finset (S T : Finset ι) (hST : Disjoint S T)
    (hf_Indep : iIndepFun m f κ μ) (hf_meas : ∀ i, Measurable (f i)) :
    IndepFun (fun a (i : S) => f i a) (fun a (i : T) => f i a) κ μ

Proof state:
case h.mpr
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : μ ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᶠ[ae μ] ⇑η
hη : IsMarkovKernel η
πSβ : Set (Set ((i : { x // x ∈ S }) → β ↑i)) := univ.pi '' univ.pi fun i => {s | MeasurableSet s}
πS : Set (Set Ω) := {s | ∃ t ∈ πSβ, (fun a i => f (↑i) a) ⁻¹' t = s}
hπS_pi : IsPiSystem πS
hπS_gen : MeasurableSpace.comap (fun a i => f (↑i) a) MeasurableSpace.pi = generateFrom πS
πTβ : Set (Set ((i : { x // x ∈ T }) → β ↑i)) := univ.pi '' univ.pi fun i => {s | MeasurableSet s}
πT : Set (Set Ω) := {s | ∃ t ∈ πTβ, (fun a i => f (↑i) a) ⁻¹' t = s}
hπT_pi : IsPiSystem πT
hπT_gen : MeasurableSpace.comap (fun a i => f (↑i) a) MeasurableSpace.pi = generateFrom πT
s : Set ((i : { x // x ∈ S }) → β ↑i)
sets_s : (i : { x // x ∈ S }) → Set (β ↑i)
hs2 : univ.pi sets_s = s
t : Set ((i : { x // x ∈ T }) → β ↑i)
sets_t : (i : { x // x ∈ T }) → Set (β ↑i)
ht2 : univ.pi sets_t = t
hs1 : ∀ (i : { x // x ∈ S }), MeasurableSet (sets_s i)
ht1 : ∀ (i : { x // x ∈ T }), MeasurableSet (sets_t i)
sets_s' : (i : ι) → Set (β i) := fun i => if hi : i ∈ S then sets_s ⟨i, hi⟩ else univ
h_sets_s'_eq : ∀ {i : ι} (hi : i ∈ S), sets_s' i = sets_s ⟨i, hi⟩
h_sets_s'_univ : ∀ {i : ι}, i ∈ T → sets_s' i = univ
sets_t' : (i : ι) → Set (β i) := fun i => if hi : i ∈ T then sets_t ⟨i, hi⟩ else univ
h_sets_t'_univ : ∀ {i : ι}, i ∈ S → sets_t' i = univ
h_meas_s' : ∀ i ∈ S, MeasurableSet (sets_s' i)
h_meas_t' : ∀ i ∈ T, MeasurableSet (sets_t' i)
h_eq_inter_S : (fun ω i => f (↑i) ω) ⁻¹' univ.pi sets_s = ⋂ i ∈ S, f i ⁻¹' sets_s' i
h_eq_inter_T : (fun ω i => f (↑i) ω) ⁻¹' univ.pi sets_t = ⋂ i ∈ T, f i ⁻¹' sets_t' i
hf_Indep :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (η a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (η a) (f i ⁻¹' sets i)
x : Ω
h : ∀ (i : ι), i ∈ S ∨ i ∈ T → f i x ∈ sets_s' i ∩ sets_t' i
⊢ (∀ i ∈ S, f i x ∈ sets_s' i) ∧ ∀ i ∈ T, f i x ∈ sets_t' i

Tactic:
exact ⟨fun i hi => (h i (Or.inl hi)).1, fun i hi => (h i (Or.inr hi)).2⟩

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate (hx : x ∈ periodicPts f)
    (hm : IsPeriodicPt f m (f^[n] x)) : IsPeriodicPt f m x

Proof state:
α : Type u_1
f : α → α
x : α
m n : ℕ
hx : x ∈ periodicPts f
hm : IsPeriodicPt f m (f^[n] x)
⊢ IsPeriodicPt f m x

Tactic:
rcases hx with ⟨r, hr, hr'⟩

Result:
case intro.intro
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
⊢ IsPeriodicPt f m x

Proof state:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ f^[m] x = x

Tactic:
convert (hm.apply_iterate ((n / r + 1) * r - n)).eq <;>
  rw [← iterate_add_apply, Nat.sub_add_cancel this, iterate_mul, (hr'.iterate _).eq]

Result:
no goals

Proof state:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ IsPeriodicPt f m x

Tactic:
unfold IsPeriodicPt IsFixedPt

Result:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
this : n ≤ (n / r + 1) * r
⊢ f^[m] x = x

Proof state:
case intro.intro
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
⊢ n ≤ n / r * r + r

Tactic:
exact (Nat.lt_div_mul_add hr).le

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
⊢ IsPeriodicPt f m x

Tactic:
suffices n ≤ (n / r + 1) * r by
  unfold IsPeriodicPt IsFixedPt
  convert (hm.apply_iterate ((n / r + 1) * r - n)).eq <;>
    rw [← iterate_add_apply, Nat.sub_add_cancel this, iterate_mul, (hr'.iterate _).eq]

Result:
case intro.intro
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
⊢ n ≤ (n / r + 1) * r

Proof state:
case intro.intro
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
⊢ n ≤ (n / r + 1) * r

Tactic:
rw [Nat.add_mul, one_mul]

Result:
case intro.intro
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m (f^[n] x)
r : ℕ
hr : r > 0
hr' : IsPeriodicPt f r x
⊢ n ≤ n / r * r + r
-- Mathlib/Order/Hom/Lattice.lean
theorem map_sdiff' (a b : α) : f (a \ b) = f a \ f b

Proof state:
F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : BooleanAlgebra α
inst✝² : BooleanAlgebra β
inst✝¹ : FunLike F α β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ f (a \ b) = f a \ f b

Tactic:
rw [sdiff_eq, sdiff_eq, map_inf, map_compl']

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/SeminormFromBounded.lean
theorem seminormFromBounded_one_le (f_nonneg : 0 ≤ f)
    (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y) :
    seminormFromBounded' f 1 ≤ 1

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
f_ne_zero : ¬f ≠ 0
x✝ : R
⊢ f x✝ / f x✝ ≤ 1

Tactic:
push_neg at f_ne_zero

Result:
case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x✝ : R
f_ne_zero : f = 0
⊢ f x✝ / f x✝ ≤ 1

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
f_ne_zero : ¬f ≠ 0
⊢ seminormFromBounded' f 1 ≤ 1

Tactic:
simp_rw [seminormFromBounded', one_mul]

Result:
case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
f_ne_zero : ¬f ≠ 0
⊢ ⨆ y, f y / f y ≤ 1

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x✝ : R
f_ne_zero : f = 0
⊢ f x✝ / f x✝ ≤ 1

Tactic:
simp only [f_ne_zero, Pi.zero_apply, div_zero, zero_le_one]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
f_ne_zero : ¬f ≠ 0
⊢ ⨆ y, f y / f y ≤ 1

Tactic:
refine ciSup_le (fun _ ↦ ?_)

Result:
case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
f_ne_zero : ¬f ≠ 0
x✝ : R
⊢ f x✝ / f x✝ ≤ 1

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
f_ne_zero : f ≠ 0
⊢ seminormFromBounded' f 1 ≤ 1

Tactic:
exact le_of_eq (seminormFromBounded_one f_ne_zero f_nonneg f_mul)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
⊢ seminormFromBounded' f 1 ≤ 1

Tactic:
by_cases f_ne_zero : f ≠ 0

Result:
case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
f_ne_zero : f ≠ 0
⊢ seminormFromBounded' f 1 ≤ 1

case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
f_ne_zero : ¬f ≠ 0
⊢ seminormFromBounded' f 1 ≤ 1
-- Mathlib/Algebra/Field/Subfield/Basic.lean
theorem mem_sSup_of_directedOn {S : Set (Subfield K)} (Sne : S.Nonempty) (hS : DirectedOn (· ≤ ·) S)
    {x : K} : x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Proof state:
K : Type u
inst✝ : DivisionRing K
S : Set (Subfield K)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 => x1 ≤ x2) S
x : K
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
haveI : Nonempty S := Sne.to_subtype

Result:
K : Type u
inst✝ : DivisionRing K
S : Set (Subfield K)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 => x1 ≤ x2) S
x : K
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Proof state:
K : Type u
inst✝ : DivisionRing K
S : Set (Subfield K)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 => x1 ≤ x2) S
x : K
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, Subtype.exists, exists_prop]

Result:
no goals
-- Mathlib/Analysis/Calculus/TangentCone.lean
theorem tangentCone_nonempty_of_properSpace [ProperSpace E]
    {s : Set E} {x : E} (hx : (𝓝[s \ {x}] x).NeBot) :
    (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : ProperSpace E
s : Set E
x : E
hx : (𝓝[s \ {x}] x).NeBot
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
hv : ∀ (n : ℕ), v n ∈ s \ {x} ∩ Metric.ball x (u n)
d : ℕ → E := fun n => v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : ℕ → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
⊢ Tendsto (fun n => ‖c n‖⁻¹) atTop (𝓝 0) ∧ ∃ a, ∀ (b : ℕ), a ≤ b → 0 < ‖c b‖⁻¹

Tactic:
have B (n : ℕ) : ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * u n := by
  apply (hc n).trans
  gcongr
  specialize hv n
  simp only [mem_inter_iff, mem_diff, mem_singleton_iff, Metric.mem_ball, dist_eq_norm] at hv
  simpa using hv.2.le

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : ProperSpace E
s : Set E
x : E
hx : (𝓝[s \ {x}] x).NeBot
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
hv : ∀ (n : ℕ), v n ∈ s \ {x} ∩ Metric.ball x (u n)
d : ℕ → E := fun n => v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : ℕ → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
B : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * u n
⊢ Tendsto (fun n => ‖c n‖⁻¹) atTop (𝓝 0) ∧ ∃ a, ∀ (b : ℕ), a ≤ b → 0 < ‖c b‖⁻¹

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : ProperSpace E
s : Set E
x : E
hx : (𝓝[s \ {x}] x).NeBot
⊢ (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty

Tactic:
obtain ⟨u, -, u_pos, u_lim⟩ :
    ∃ u, StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (𝓝 (0 : ℝ)) :=
  exists_seq_strictAnti_tendsto (0 : ℝ)

Result:
case intro.intro.intro
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : ProperSpace E
s : Set E
x : E
hx : (𝓝[s \ {x}] x).NeBot
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
⊢ (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty
-- Mathlib/Algebra/FreeAlgebra.lean
theorem induction {C : FreeAlgebra R X → Prop}
    (h_grade0 : ∀ r, C (algebraMap R (FreeAlgebra R X) r)) (h_grade1 : ∀ x, C (ι R x))
    (h_mul : ∀ a b, C a → C b → C (a * b)) (h_add : ∀ a b, C a → C b → C (a + b))
    (a : FreeAlgebra R X) : C a

Proof state:
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C ((algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  { carrier := C, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := h_grade0 }
of : X → ↥s := Subtype.coind (ι R) h_grade1
of_id : AlgHom.id R (FreeAlgebra R X) = s.val.comp ((lift R) of)
⊢ C a

Tactic:
suffices a = lift R of a by
  rw [this]
  exact Subtype.prop (lift R of a)

Result:
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C ((algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  { carrier := C, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := h_grade0 }
of : X → ↥s := Subtype.coind (ι R) h_grade1
of_id : AlgHom.id R (FreeAlgebra R X) = s.val.comp ((lift R) of)
⊢ a = ↑(((lift R) of) a)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C ((algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  { carrier := C, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := h_grade0 }
of : X → ↥s := Subtype.coind (ι R) h_grade1
of_id : AlgHom.id R (FreeAlgebra R X) = s.val.comp ((lift R) of)
this : a = ↑(((lift R) of) a)
⊢ C a

Tactic:
rw [this]

Result:
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C ((algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  { carrier := C, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := h_grade0 }
of : X → ↥s := Subtype.coind (ι R) h_grade1
of_id : AlgHom.id R (FreeAlgebra R X) = s.val.comp ((lift R) of)
this : a = ↑(((lift R) of) a)
⊢ C ↑(((lift R) of) a)