harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem linearIsometryEquiv_comp_rightAngleRotation (φ : E ≃ₗᵢ[ℝ] E)
    (hφ : 0 < LinearMap.det (φ.toLinearEquiv : E →ₗ[ℝ] E)) (x : E) : φ (J x) = J (φ x)

Proof state:
case h.e'_3.h.e'_5.h.e'_5
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
x : E
⊢ Fintype.card (Fin 2) = finrank ℝ E

Tactic:
rw [@Fact.out (finrank ℝ E = 2), Fintype.card_fin]

Result:
no goals

Proof state:
case h.e'_2.h.e'_6.h.e'_6
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
x : E
⊢ x = φ.symm (φ x)

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_3.h.e'_5.h.e'_5
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
x : E
⊢ o = (map (Fin 2) φ.toLinearEquiv) o

Tactic:
symm

Result:
case h.e'_3.h.e'_5.h.e'_5
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
x : E
⊢ (map (Fin 2) φ.toLinearEquiv) o = o

Proof state:
case h.e'_3.h.e'_5.h.e'_5
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
x : E
⊢ (map (Fin 2) φ.toLinearEquiv) o = o

Tactic:
rwa [← o.map_eq_iff_det_pos φ.toLinearEquiv] at hφ

Result:
case h.e'_3.h.e'_5.h.e'_5
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
x : E
⊢ Fintype.card (Fin 2) = finrank ℝ E

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
x : E
⊢ φ (o.rightAngleRotation x) = o.rightAngleRotation (φ x)

Tactic:
convert (o.rightAngleRotation_map φ (φ x)).symm

Result:
case h.e'_2.h.e'_6.h.e'_6
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
x : E
⊢ x = φ.symm (φ x)

case h.e'_3.h.e'_5.h.e'_5
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
x : E
⊢ o = (map (Fin 2) φ.toLinearEquiv) o
-- Mathlib/LinearAlgebra/AffineSpace/Ordered.lean
theorem map_le_lineMap_iff_slope_le_slope (hab : a < b) (h₀ : 0 < r) (h₁ : r < 1) :
    f c ≤ lineMap (f a) (f b) r ↔ slope f a c ≤ slope f c b

Proof state:
k : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
f : k → E
a b r : k
hab : a < b
h₀ : 0 < r
h₁ : r < 1
⊢ f ((lineMap a b) r) ≤ (lineMap (f a) (f b)) r ↔ slope f a ((lineMap a b) r) ≤ slope f ((lineMap a b) r) b

Tactic:
rw [map_le_lineMap_iff_slope_le_slope_left (mul_pos h₀ (sub_pos.2 hab)), ←
  lineMap_slope_lineMap_slope_lineMap f a b r, right_le_lineMap_iff_le h₁]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Measure.lean
theorem haar_singleton [IsTopologicalGroup G] [BorelSpace G] (g : G) : μ {g} = μ {(1 : G)}

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : IsTopologicalGroup G
inst✝ : BorelSpace G
g : G
⊢ μ {g} = μ {1}

Tactic:
convert measure_preimage_mul μ g⁻¹ _

Result:
case h.e'_2.h.e'_6
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : IsTopologicalGroup G
inst✝ : BorelSpace G
g : G
⊢ {g} = (fun h => g⁻¹ * h) ⁻¹' {1}

Proof state:
case h.e'_2.h.e'_6
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : IsTopologicalGroup G
inst✝ : BorelSpace G
g : G
⊢ {g} = (fun h => g⁻¹ * h) ⁻¹' {1}

Tactic:
simp only [mul_one, preimage_mul_left_singleton, inv_inv]

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem isLeftInversion_simple_iff_isLeftDescent (w : W) (i : B) :
    cs.IsLeftInversion w (s i) ↔ cs.IsLeftDescent w i

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.IsLeftInversion w (cs.simple i) ↔ cs.IsLeftDescent w i

Tactic:
simp [IsLeftInversion, IsLeftDescent, cs.isReflection_simple i]

Result:
no goals
-- Mathlib/NumberTheory/LucasLehmer.lean
theorem ext {x y : X q} (h₁ : x.1 = y.1) (h₂ : x.2 = y.2) : x = y

Proof state:
case mk
q : ℕ+
y : X q
fst✝ snd✝ : ZMod ↑q
h₁ : (fst✝, snd✝).1 = y.1
h₂ : (fst✝, snd✝).2 = y.2
⊢ (fst✝, snd✝) = y

Tactic:
cases y

Result:
case mk.mk
q : ℕ+
fst✝¹ snd✝¹ fst✝ snd✝ : ZMod ↑q
h₁ : (fst✝¹, snd✝¹).1 = (fst✝, snd✝).1
h₂ : (fst✝¹, snd✝¹).2 = (fst✝, snd✝).2
⊢ (fst✝¹, snd✝¹) = (fst✝, snd✝)

Proof state:
q : ℕ+
x y : X q
h₁ : x.1 = y.1
h₂ : x.2 = y.2
⊢ x = y

Tactic:
cases x

Result:
case mk
q : ℕ+
y : X q
fst✝ snd✝ : ZMod ↑q
h₁ : (fst✝, snd✝).1 = y.1
h₂ : (fst✝, snd✝).2 = y.2
⊢ (fst✝, snd✝) = y

Proof state:
case mk.mk
q : ℕ+
fst✝¹ snd✝¹ fst✝ snd✝ : ZMod ↑q
h₁ : (fst✝¹, snd✝¹).1 = (fst✝, snd✝).1
h₂ : (fst✝¹, snd✝¹).2 = (fst✝, snd✝).2
⊢ (fst✝¹, snd✝¹) = (fst✝, snd✝)

Tactic:
congr

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/SubboxInduction.lean
theorem subbox_induction_on {p : Box ι → Prop} (I : Box ι)
    (H_ind : ∀ J ≤ I, (∀ J' ∈ splitCenter J, p J') → p J)
    (H_nhds : ∀ z ∈ Box.Icc I, ∃ U ∈ 𝓝[Box.Icc I] z, ∀ J ≤ I, ∀ (m : ℕ),
      z ∈ Box.Icc J → Box.Icc J ⊆ U →
        (∀ i, J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J) :
    p I

Proof state:
case intro
ι : Type u_1
inst✝ : Fintype ι
p : Box ι → Prop
I : Box ι
H_ind : ∀ J ≤ I, (∀ J' ∈ splitCenter J, p J') → p J
H_nhds :
  ∀ z ∈ Box.Icc I,
    ∃ U ∈ 𝓝[Box.Icc I] z,
      ∀ J ≤ I,
        ∀ (m : ℕ),
          z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J
J : Box ι
hle : J ≤ I
hs : ∀ (s : Set ι), p (J.splitCenterBox s)
s : Set ι
h' : J.splitCenterBox s ∈ splitCenter J
⊢ p (J.splitCenterBox s)

Tactic:
exact hs s

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
p : Box ι → Prop
I : Box ι
H_ind : ∀ J ≤ I, (∀ J' ∈ splitCenter J, p J') → p J
H_nhds :
  ∀ z ∈ Box.Icc I,
    ∃ U ∈ 𝓝[Box.Icc I] z,
      ∀ J ≤ I,
        ∀ (m : ℕ),
          z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J
J : Box ι
hle : J ≤ I
hs : ∀ (s : Set ι), p (J.splitCenterBox s)
J' : Box ι
h' : J' ∈ splitCenter J
⊢ p J'

Tactic:
rcases mem_splitCenter.1 h' with ⟨s, rfl⟩

Result:
case intro
ι : Type u_1
inst✝ : Fintype ι
p : Box ι → Prop
I : Box ι
H_ind : ∀ J ≤ I, (∀ J' ∈ splitCenter J, p J') → p J
H_nhds :
  ∀ z ∈ Box.Icc I,
    ∃ U ∈ 𝓝[Box.Icc I] z,
      ∀ J ≤ I,
        ∀ (m : ℕ),
          z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J
J : Box ι
hle : J ≤ I
hs : ∀ (s : Set ι), p (J.splitCenterBox s)
s : Set ι
h' : J.splitCenterBox s ∈ splitCenter J
⊢ p (J.splitCenterBox s)

Proof state:
ι : Type u_1
inst✝ : Fintype ι
p : Box ι → Prop
I : Box ι
H_ind : ∀ J ≤ I, (∀ J' ∈ splitCenter J, p J') → p J
H_nhds :
  ∀ z ∈ Box.Icc I,
    ∃ U ∈ 𝓝[Box.Icc I] z,
      ∀ J ≤ I,
        ∀ (m : ℕ),
          z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J
⊢ p I

Tactic:
refine subbox_induction_on' I (fun J hle hs => H_ind J hle fun J' h' => ?_) H_nhds

Result:
ι : Type u_1
inst✝ : Fintype ι
p : Box ι → Prop
I : Box ι
H_ind : ∀ J ≤ I, (∀ J' ∈ splitCenter J, p J') → p J
H_nhds :
  ∀ z ∈ Box.Icc I,
    ∃ U ∈ 𝓝[Box.Icc I] z,
      ∀ J ≤ I,
        ∀ (m : ℕ),
          z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J
J : Box ι
hle : J ≤ I
hs : ∀ (s : Set ι), p (J.splitCenterBox s)
J' : Box ι
h' : J' ∈ splitCenter J
⊢ p J'
-- Mathlib/Order/Filter/Basic.lean
theorem inter_eventuallyEq_left {s t : Set α} {l : Filter α} :
    (s ∩ t : Set α) =ᶠ[l] s ↔ ∀ᶠ x in l, x ∈ s → x ∈ t

Proof state:
α : Type u
s t : Set α
l : Filter α
⊢ s ∩ t =ᶠ[l] s ↔ ∀ᶠ (x : α) in l, x ∈ s → x ∈ t

Tactic:
simp only [eventuallyEq_set, mem_inter_iff, and_iff_left_iff_imp]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
theorem absNorm_bot : absNorm (⊥ : Ideal S) = 0

Proof state:
S : Type u_1
inst✝³ : CommRing S
inst✝² : Nontrivial S
inst✝¹ : IsDedekindDomain S
inst✝ : Module.Free ℤ S
⊢ absNorm ⊥ = 0

Tactic:
rw [← Ideal.zero_eq_bot, _root_.map_zero]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_le_one_of_one_le_of_neg {x : ℝ≥0∞} {z : ℝ} (hx : 1 ≤ x) (hz : z < 0) : x ^ z ≤ 1

Proof state:
case coe
z : ℝ
hz : z < 0
x✝ : ℝ≥0
hx : 1 ≤ x✝
⊢ ↑x✝ ^ z ≤ 1

Tactic:
simp [← coe_rpow_of_ne_zero (ne_of_gt (lt_of_lt_of_le zero_lt_one hx)),
  NNReal.rpow_le_one_of_one_le_of_nonpos hx (le_of_lt hz)]

Result:
no goals

Proof state:
case top
z : ℝ
hz : z < 0
hx : 1 ≤ ⊤
⊢ ⊤ ^ z ≤ 1

Tactic:
simp [top_rpow_of_neg hz, zero_lt_one]

Result:
no goals

Proof state:
x : ℝ≥0∞
z : ℝ
hx : 1 ≤ x
hz : z < 0
⊢ x ^ z ≤ 1

Tactic:
cases x

Result:
case top
z : ℝ
hz : z < 0
hx : 1 ≤ ⊤
⊢ ⊤ ^ z ≤ 1

case coe
z : ℝ
hz : z < 0
x✝ : ℝ≥0
hx : 1 ≤ ↑x✝
⊢ ↑x✝ ^ z ≤ 1

Proof state:
case coe
z : ℝ
hz : z < 0
x✝ : ℝ≥0
hx : 1 ≤ ↑x✝
⊢ ↑x✝ ^ z ≤ 1

Tactic:
simp only [one_le_coe_iff, some_eq_coe] at hx

Result:
case coe
z : ℝ
hz : z < 0
x✝ : ℝ≥0
hx : 1 ≤ x✝
⊢ ↑x✝ ^ z ≤ 1
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem exists_pos_sum_of_countable {ε : ℝ≥0∞} (hε : ε ≠ 0) (ι) [Countable ι] :
    ∃ ε' : ι → ℝ≥0, (∀ i, 0 < ε' i) ∧ (∑' i, (ε' i : ℝ≥0∞)) < ε

Proof state:
case intro.intro.intro.intro
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
x : ℝ≥0
right✝ : ↑x < ε
h0r : 0 < ↑x
hrε : ↑x < ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), ↑(ε' i) < ε

Tactic:
rcases NNReal.exists_pos_sum_of_countable (coe_pos.1 h0r).ne' ι with ⟨ε', hp, c, hc, hcr⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
x : ℝ≥0
right✝ : ↑x < ε
h0r : 0 < ↑x
hrε : ↑x < ε
ε' : ι → ℝ≥0
hp : ∀ (i : ι), 0 < ε' i
c : ℝ≥0
hc : HasSum ε' c
hcr : c < x
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), ↑(ε' i) < ε

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
x : ℝ≥0
right✝ : ↑x < ε
h0r : 0 < ↑x
hrε : ↑x < ε
ε' : ι → ℝ≥0
hp : ∀ (i : ι), 0 < ε' i
c : ℝ≥0
hc : HasSum ε' c
hcr : c < x
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), ↑(ε' i) < ε

Tactic:
exact ⟨ε', hp, (ENNReal.tsum_coe_eq hc).symm ▸ lt_trans (coe_lt_coe.2 hcr) hrε⟩

Result:
no goals

Proof state:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), ↑(ε' i) < ε

Tactic:
rcases exists_between (pos_iff_ne_zero.2 hε) with ⟨r, h0r, hrε⟩

Result:
case intro.intro
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
r : ℝ≥0∞
h0r : 0 < r
hrε : r < ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), ↑(ε' i) < ε

Proof state:
case intro.intro
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
r : ℝ≥0∞
h0r : 0 < r
hrε : r < ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), ↑(ε' i) < ε

Tactic:
rcases lt_iff_exists_coe.1 hrε with ⟨x, rfl, _⟩

Result:
case intro.intro.intro.intro
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
x : ℝ≥0
right✝ : ↑x < ε
h0r : 0 < ↑x
hrε : ↑x < ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), ↑(ε' i) < ε
-- Mathlib/RingTheory/Localization/Ideal.lean
theorem bot_lt_comap_prime [IsDomain R] (hM : M ≤ R⁰) (p : Ideal S) [hpp : p.IsPrime]
    (hp0 : p ≠ ⊥) : ⊥ < Ideal.comap (algebraMap R S) p

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : IsDomain R
hM : M ≤ R⁰
p : Ideal S
hpp : p.IsPrime
hp0 : p ≠ ⊥
this : IsDomain S
⊢ ⊥ < Ideal.comap (algebraMap R S) p

Tactic:
rw [← Ideal.comap_bot_of_injective (algebraMap R S) (IsLocalization.injective _ hM)]

Result:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : IsDomain R
hM : M ≤ R⁰
p : Ideal S
hpp : p.IsPrime
hp0 : p ≠ ⊥
this : IsDomain S
⊢ Ideal.comap (algebraMap R S) ⊥ < Ideal.comap (algebraMap R S) p

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : IsDomain R
hM : M ≤ R⁰
p : Ideal S
hpp : p.IsPrime
hp0 : p ≠ ⊥
⊢ ⊥ < Ideal.comap (algebraMap R S) p

Tactic:
haveI : IsDomain S := isDomain_of_le_nonZeroDivisors _ hM

Result:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : IsDomain R
hM : M ≤ R⁰
p : Ideal S
hpp : p.IsPrime
hp0 : p ≠ ⊥
this : IsDomain S
⊢ ⊥ < Ideal.comap (algebraMap R S) p

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : IsDomain R
hM : M ≤ R⁰
p : Ideal S
hpp : p.IsPrime
hp0 : p ≠ ⊥
this : IsDomain S
⊢ Ideal.comap (algebraMap R S) ⊥ < Ideal.comap (algebraMap R S) p

Tactic:
convert (orderIsoOfPrime M S).lt_iff_lt.mpr (show (⟨⊥, Ideal.bot_prime⟩ :
  { p : Ideal S // p.IsPrime }) < ⟨p, hpp⟩ from hp0.bot_lt)

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem X_dvd_iff {φ : R⟦X⟧} : (X : R⟦X⟧) ∣ φ ↔ constantCoeff R φ = 0

Proof state:
case mpr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : (coeff R 0) φ = 0
m : ℕ
hm : m < 1
⊢ (coeff R m) φ = 0

Tactic:
rwa [Nat.eq_zero_of_le_zero (Nat.le_of_succ_le_succ hm)]

Result:
no goals

Proof state:
case mp
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : ∀ m < 1, (coeff R m) φ = 0
⊢ (coeff R 0) φ = 0

Tactic:
exact h 0 zero_lt_one

Result:
no goals

Proof state:
case mpr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : (coeff R 0) φ = 0
⊢ ∀ m < 1, (coeff R m) φ = 0

Tactic:
intro m hm

Result:
case mpr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : (coeff R 0) φ = 0
m : ℕ
hm : m < 1
⊢ (coeff R m) φ = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (∀ m < 1, (coeff R m) φ = 0) ↔ (coeff R 0) φ = 0

Tactic:
constructor <;> intro h

Result:
case mp
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : ∀ m < 1, (coeff R m) φ = 0
⊢ (coeff R 0) φ = 0

case mpr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : (coeff R 0) φ = 0
⊢ ∀ m < 1, (coeff R m) φ = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ X ∣ φ ↔ (constantCoeff R) φ = 0

Tactic:
rw [← pow_one (X : R⟦X⟧), X_pow_dvd_iff, ← coeff_zero_eq_constantCoeff_apply]

Result:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (∀ m < 1, (coeff R m) φ = 0) ↔ (coeff R 0) φ = 0
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
theorem lt_tan {x : ℝ} (h1 : 0 < x) (h2 : x < π / 2) : x < tan x

Proof state:
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
z : ℝ
hz : z ∈ U
⊢ z ∈ {x | cos x ≠ 0}

Tactic:
simp only [mem_setOf_eq]

Result:
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
z : ℝ
hz : z ∈ U
⊢ cos z ≠ 0

Proof state:
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
⊢ x < tan x

Tactic:
have cos_pos {y : ℝ} (hy : y ∈ U) : 0 < cos y := by
  exact cos_pos_of_mem_Ioo (Ico_subset_Ioo_left (neg_lt_zero.mpr half_pi_pos) hy)

Result:
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
⊢ x < tan x
-- Mathlib/Topology/Category/Profinite/CofilteredLimit.lean
theorem exists_locallyConstant {α : Type*} (hC : IsLimit C) (f : LocallyConstant C.pt α) :
    ∃ (j : J) (g : LocallyConstant (F.obj j) α), f = g.comap (C.π.app _).hom

Proof state:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
ff : Quotient S.toSetoid → α := ⇑f.lift
h✝ : IsEmpty (Quotient S.toSetoid)
this✝ : ∃ j, IsEmpty ↑(F.obj j).toTop
j : J
hj : IsEmpty ↑(F.obj j).toTop
A : Set α
this : (fun a => hj.elim a) ⁻¹' A = ∅
⊢ IsOpen ((fun a => hj.elim a) ⁻¹' A)

Tactic:
rw [this]

Result:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
ff : Quotient S.toSetoid → α := ⇑f.lift
h✝ : IsEmpty (Quotient S.toSetoid)
this✝ : ∃ j, IsEmpty ↑(F.obj j).toTop
j : J
hj : IsEmpty ↑(F.obj j).toTop
A : Set α
this : (fun a => hj.elim a) ⁻¹' A = ∅
⊢ IsOpen ∅
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem ContDiffWithinAt.contDiffOn' (hm : m ≤ n) (h' : m = ∞ → n = ω)
    (h : ContDiffWithinAt 𝕜 n f s x) :
    ∃ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn 𝕜 m f (insert x s ∩ u)

Proof state:
case intro.intro.intro.intro.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
m✝ n : WithTop ℕ∞
h : ContDiffWithinAt 𝕜 n f s x
hn : n ≠ ω
m : ℕ
hm : ↑m ≤ n
h' : ↑m = ∞ → n = ω
t : Set E
ht : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn (↑m) f p t
u : Set E
huo : IsOpen u
hxu : x ∈ u
hut : u ∩ insert x s ⊆ t
⊢ ∃ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn 𝕜 (↑m) f (insert x s ∩ u)

Tactic:
rw [inter_comm] at hut

Result:
case intro.intro.intro.intro.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
m✝ n : WithTop ℕ∞
h : ContDiffWithinAt 𝕜 n f s x
hn : n ≠ ω
m : ℕ
hm : ↑m ≤ n
h' : ↑m = ∞ → n = ω
t : Set E
ht : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn (↑m) f p t
u : Set E
huo : IsOpen u
hxu : x ∈ u
hut : insert x s ∩ u ⊆ t
⊢ ∃ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn 𝕜 (↑m) f (insert x s ∩ u)
-- Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean
@[reassoc]
lemma triangleMapOfHomotopy_comm₃ :
    mapOfHomotopy H ≫ (triangle φ₂).mor₃ = (triangle φ₁).mor₃ ≫ a⟦1⟧'

Proof state:
case h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K₁ L₁ K₂ L₂ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
p : ℤ
⊢ (desc φ₁
            ((Cochain.ofHom a).comp (inl φ₂) mapOfHomotopy.proof_4 +
              (Cochain.ofHomotopy H).comp (Cochain.ofHom (inr φ₂)) mapOfHomotopy.proof_5)
            (b ≫ inr φ₂) ⋯).f
        p ≫
      ((-↑(fst φ₂)).rightShift 1 0 triangle.proof_3).v p p ⋯ =
    ((-↑(fst φ₁)).rightShift 1 0 triangle.proof_3).v p p ⋯ ≫ a.f (p + 1)

Tactic:
simp only [Int.reduceNeg, Cochain.rightShift_neg, Cochain.neg_v, shiftFunctor_obj_X',
  Cochain.rightShift_v _ 1 0 _ p p _ (p + 1) rfl, shiftFunctor_obj_X, shiftFunctorObjXIso,
  HomologicalComplex.XIsoOfEq_rfl, Iso.refl_inv, comp_id, Preadditive.comp_neg,
  Preadditive.neg_comp, ext_from_iff _ _ _ rfl, inl_v_desc_f_assoc, Cochain.add_v,
  Cochain.zero_cochain_comp_v, Cochain.ofHom_v, Cochain.comp_zero_cochain_v, Preadditive.add_comp,
  assoc, inl_v_fst_v, inr_f_fst_v, comp_zero, add_zero, inl_v_fst_v_assoc, inr_f_desc_f_assoc,
  HomologicalComplex.comp_f, neg_zero, inr_f_fst_v_assoc, zero_comp, and_self]

Result:
no goals

Proof state:
case h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K₁ L₁ K₂ L₂ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
p : ℤ
⊢ (mapOfHomotopy H ≫ (triangle φ₂).mor₃).f p =
    ((triangle φ₁).mor₃ ≫ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map a).f p

Tactic:
dsimp [mapOfHomotopy, triangle]

Result:
case h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K₁ L₁ K₂ L₂ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
p : ℤ
⊢ (desc φ₁
            ((Cochain.ofHom a).comp (inl φ₂) mapOfHomotopy.proof_4 +
              (Cochain.ofHomotopy H).comp (Cochain.ofHom (inr φ₂)) mapOfHomotopy.proof_5)
            (b ≫ inr φ₂) ⋯).f
        p ≫
      ((-↑(fst φ₂)).rightShift 1 0 triangle.proof_3).v p p ⋯ =
    ((-↑(fst φ₁)).rightShift 1 0 triangle.proof_3).v p p ⋯ ≫ a.f (p + 1)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K₁ L₁ K₂ L₂ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
⊢ mapOfHomotopy H ≫ (triangle φ₂).mor₃ = (triangle φ₁).mor₃ ≫ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map a

Tactic:
ext p

Result:
case h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K₁ L₁ K₂ L₂ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
p : ℤ
⊢ (mapOfHomotopy H ≫ (triangle φ₂).mor₃).f p =
    ((triangle φ₁).mor₃ ≫ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map a).f p
-- Mathlib/CategoryTheory/Limits/Shapes/Products.lean
theorem Sigma.eqToHom_comp_ι {J : Type*} (f : J → C) [HasCoproduct f] {j j' : J} (w : j = j') :
    eqToHom (by simp [w]) ≫ Sigma.ι f j' = Sigma.ι f j

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
f : J → C
inst✝ : HasCoproduct f
j j' : J
w : j = j'
⊢ eqToHom ⋯ ≫ ι f j' = ι f j

Tactic:
cases w

Result:
case refl
C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
f : J → C
inst✝ : HasCoproduct f
j : J
⊢ eqToHom ⋯ ≫ ι f j = ι f j

Proof state:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
f : J → C
inst✝ : HasCoproduct f
j j' : J
w : j = j'
⊢ f j = f j'

Tactic:
simp [w]

Result:
no goals

Proof state:
case refl
C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
f : J → C
inst✝ : HasCoproduct f
j : J
⊢ eqToHom ⋯ ≫ ι f j = ι f j

Tactic:
simp

Result:
no goals