harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean
theorem exists_nat_measure_lt_two_inv (hfg : TendstoInMeasure μ f atTop g) (n : ℕ) :
    ∃ N, ∀ m ≥ N, μ { x | (2 : ℝ)⁻¹ ^ n ≤ dist (f m x) (g x) } ≤ (2⁻¹ : ℝ≥0∞) ^ n

Proof state:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
n : ℕ
⊢ ∃ N, ∀ m_1 ≥ N, μ {x | 2⁻¹ ^ n ≤ dist (f m_1 x) (g x)} ≤ 2⁻¹ ^ n

Tactic:
specialize hfg ((2⁻¹ : ℝ) ^ n) (by simp only [Real.rpow_natCast, inv_pos, zero_lt_two, pow_pos])

Result:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
n : ℕ
hfg : Tendsto (fun i => μ {x | 2⁻¹ ^ n ≤ dist (f i x) (g x)}) atTop (𝓝 0)
⊢ ∃ N, ∀ m_1 ≥ N, μ {x | 2⁻¹ ^ n ≤ dist (f m_1 x) (g x)} ≤ 2⁻¹ ^ n

Proof state:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
n : ℕ
hfg : Tendsto (fun i => μ {x | 2⁻¹ ^ n ≤ dist (f i x) (g x)}) atTop (𝓝 0)
⊢ ∃ N, ∀ m_1 ≥ N, μ {x | 2⁻¹ ^ n ≤ dist (f m_1 x) (g x)} ≤ 2⁻¹ ^ n

Tactic:
rw [ENNReal.tendsto_atTop_zero] at hfg

Result:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
n : ℕ
hfg : ∀ ε > 0, ∃ N, ∀ n_1 ≥ N, μ {x | 2⁻¹ ^ n ≤ dist (f n_1 x) (g x)} ≤ ε
⊢ ∃ N, ∀ m_1 ≥ N, μ {x | 2⁻¹ ^ n ≤ dist (f m_1 x) (g x)} ≤ 2⁻¹ ^ n

Proof state:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
n : ℕ
⊢ 0 < 2⁻¹ ^ n

Tactic:
simp only [Real.rpow_natCast, inv_pos, zero_lt_two, pow_pos]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
n : ℕ
hfg : ∀ ε > 0, ∃ N, ∀ n_1 ≥ N, μ {x | 2⁻¹ ^ n ≤ dist (f n_1 x) (g x)} ≤ ε
⊢ ∃ N, ∀ m_1 ≥ N, μ {x | 2⁻¹ ^ n ≤ dist (f m_1 x) (g x)} ≤ 2⁻¹ ^ n

Tactic:
exact hfg ((2 : ℝ≥0∞)⁻¹ ^ n) (pos_iff_ne_zero.mpr fun h_zero => by simpa using pow_eq_zero h_zero)

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
n : ℕ
hfg : ∀ ε > 0, ∃ N, ∀ n_1 ≥ N, μ {x | 2⁻¹ ^ n ≤ dist (f n_1 x) (g x)} ≤ ε
h_zero : 2⁻¹ ^ n = 0
⊢ False

Tactic:
simpa using pow_eq_zero h_zero

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean
theorem spineToSimplex_edge (f : Path X n) (j l : ℕ) (hjl : j + l ≤ n) :
    X.map (intervalEdge j l hjl).op (spineToSimplex f) =
      spineToDiagonal (Path.interval f j l hjl)

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ X.map (intervalEdge j l hjl).op (spineToSimplex f) = diagonal X (X.map (subinterval j l hjl).op (spineToSimplex f))

Tactic:
unfold diagonal

Result:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ X.map (intervalEdge j l hjl).op (spineToSimplex f) =
    X.map (diag l).op (X.map (subinterval j l hjl).op (spineToSimplex f))

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ X.map (intervalEdge j l hjl).op (spineToSimplex f) = diagonal X (spineToSimplex (f.interval j l hjl))

Tactic:
rw [← congrArg (diagonal X) (spineToSimplex_interval f j l hjl)]

Result:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ X.map (intervalEdge j l hjl).op (spineToSimplex f) = diagonal X (X.map (subinterval j l hjl).op (spineToSimplex f))

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ X.map (intervalEdge j l hjl).op (spineToSimplex f) = spineToDiagonal (f.interval j l hjl)

Tactic:
unfold spineToDiagonal

Result:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ X.map (intervalEdge j l hjl).op (spineToSimplex f) = diagonal X (spineToSimplex (f.interval j l hjl))

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ X.map (intervalEdge j l hjl).op (spineToSimplex f) =
    X.map (diag l).op (X.map (subinterval j l hjl).op (spineToSimplex f))

Tactic:
simp only [← FunctorToTypes.map_comp_apply, ← op_comp, diag_subinterval_eq]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Center.lean
@[simp] lemma inv_mem_centralizer₀ (ha : a ∈ centralizer s) : a⁻¹ ∈ centralizer s

Proof state:
case inl
G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
ha : 0 ∈ s.centralizer
⊢ 0⁻¹ ∈ s.centralizer

Tactic:
rw [inv_zero]

Result:
case inl
G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
ha : 0 ∈ s.centralizer
⊢ 0 ∈ s.centralizer

Proof state:
case inr
G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
a : G₀
ha : a ∈ s.centralizer
ha₀ : a ≠ 0
⊢ a⁻¹ ∈ s.centralizer

Tactic:
rintro c hc

Result:
case inr
G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
a : G₀
ha : a ∈ s.centralizer
ha₀ : a ≠ 0
c : G₀
hc : c ∈ s
⊢ c * a⁻¹ = a⁻¹ * c

Proof state:
case inr
G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
a : G₀
ha : a ∈ s.centralizer
ha₀ : a ≠ 0
c : G₀
hc : c ∈ s
⊢ c * a⁻¹ = a⁻¹ * c

Tactic:
rw [mul_inv_eq_iff_eq_mul₀ ha₀, mul_assoc, eq_inv_mul_iff_mul_eq₀ ha₀, ha c hc]

Result:
no goals

Proof state:
case inl
G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
ha : 0 ∈ s.centralizer
⊢ 0 ∈ s.centralizer

Tactic:
exact zero_mem_centralizer

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
a : G₀
ha : a ∈ s.centralizer
⊢ a⁻¹ ∈ s.centralizer

Tactic:
obtain rfl | ha₀ := eq_or_ne a 0

Result:
case inl
G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
ha : 0 ∈ s.centralizer
⊢ 0⁻¹ ∈ s.centralizer

case inr
G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
a : G₀
ha : a ∈ s.centralizer
ha₀ : a ≠ 0
⊢ a⁻¹ ∈ s.centralizer
-- Mathlib/Data/Fin/Basic.lean
lemma eq_one_of_neq_zero (i : Fin 2) (hi : i ≠ 0) : i = 1

Proof state:
i : Fin 2
hi : i ≠ 0
⊢ i = 1

Tactic:
fin_omega

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem generate_neBot_iff {s : Set (Set α)} :
    NeBot (generate s) ↔ ∀ t, t ⊆ s → t.Finite → (⋂₀ t).Nonempty :=
  (hasBasis_generate s).neBot_iff.trans <| by simp only [← and_imp, and_comm]

Proof state:
α : Type u_1
s : Set (Set α)
⊢ (∀ {i : Set (Set α)}, i.Finite ∧ i ⊆ s → (⋂₀ i).Nonempty) ↔ ∀ t ⊆ s, t.Finite → (⋂₀ t).Nonempty

Tactic:
simp only [← and_imp, and_comm]

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/PInfty.lean
theorem PInfty_f_comp_QInfty_f (n : ℕ) : (PInfty.f n : X _⦋n⦌ ⟶ _) ≫ QInfty.f n = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ PInfty.f n ≫ (𝟙 K[X] - PInfty).f n = 0

Tactic:
simp only [HomologicalComplex.sub_f_apply, HomologicalComplex.id_f, comp_sub, comp_id,
  PInfty_f_idem, sub_self]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ PInfty.f n ≫ QInfty.f n = 0

Tactic:
dsimp only [QInfty]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ PInfty.f n ≫ (𝟙 K[X] - PInfty).f n = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_swap (a : Array α) (i j : Nat) (hi hj) (k : Nat) : (a.swap i j hi hj)[k]? =
    if j = k then some a[i] else if i = k then some a[j] else a[k]?

Proof state:
α : Type u_1
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
k : Nat
⊢ (a.swap i j hi hj)[k]? = if j = k then some a[i] else if i = k then some a[j] else a[k]?

Tactic:
simp [swap_def, getElem?_set]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma le_add_pred_of_pos (a : ℕ) (hb : b ≠ 0) : a ≤ b + (a - 1)

Proof state:
b a : ℕ
hb : b ≠ 0
⊢ a ≤ b + (a - 1)

Tactic:
omega

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem nhdsSet_prod_le_of_disjoint_cocompact {f : Filter Y} (hs : IsCompact s)
    (hf : Disjoint f (Filter.cocompact Y)) :
    𝓝ˢ s ×ˢ f ≤ 𝓝ˢ (s ×ˢ Set.univ)

Proof state:
case intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : Filter Y
hs : IsCompact s
hf : Disjoint f (cocompact Y)
K : Set Y
hKf : K ∈ f
hK : IsCompact K
⊢ 𝓝ˢ s ×ˢ f ≤ 𝓝ˢ (s ×ˢ univ)

Tactic:
calc
  𝓝ˢ s ×ˢ f
  _ ≤ 𝓝ˢ s ×ˢ 𝓟 K        := Filter.prod_mono_right _ (Filter.le_principal_iff.mpr hKf)
  _ ≤ 𝓝ˢ s ×ˢ 𝓝ˢ K       := Filter.prod_mono_right _ principal_le_nhdsSet
  _ = 𝓝ˢ (s ×ˢ K)         := (hs.nhdsSet_prod_eq hK).symm
  _ ≤ 𝓝ˢ (s ×ˢ Set.univ)  := nhdsSet_mono (prod_mono_right le_top)

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : Filter Y
hs : IsCompact s
hf : Disjoint f (cocompact Y)
⊢ 𝓝ˢ s ×ˢ f ≤ 𝓝ˢ (s ×ˢ univ)

Tactic:
obtain ⟨K, hKf, hK⟩ := (disjoint_cocompact_right f).mp hf

Result:
case intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : Filter Y
hs : IsCompact s
hf : Disjoint f (cocompact Y)
K : Set Y
hKf : K ∈ f
hK : IsCompact K
⊢ 𝓝ˢ s ×ˢ f ≤ 𝓝ˢ (s ×ˢ univ)
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem log_ne_zero {x : ℝ} : log x ≠ 0 ↔ x ≠ 0 ∧ x ≠ 1 ∧ x ≠ -1

Proof state:
x : ℝ
⊢ log x ≠ 0 ↔ x ≠ 0 ∧ x ≠ 1 ∧ x ≠ -1

Tactic:
simpa only [not_or] using log_eq_zero.not

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_sign_neg_right (x y : V) : (o.oangle x (-y)).sign = -(o.oangle x y).sign

Proof state:
case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
⊢ (o.oangle x (-y)).sign = -(o.oangle x y).sign

Tactic:
by_cases hy : y = 0

Result:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : y = 0
⊢ (o.oangle x (-y)).sign = -(o.oangle x y).sign

case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : ¬y = 0
⊢ (o.oangle x (-y)).sign = -(o.oangle x y).sign

Proof state:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : y = 0
⊢ (o.oangle x (-y)).sign = -(o.oangle x y).sign

Tactic:
simp [hy]

Result:
no goals

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ (o.oangle x (-y)).sign = -(o.oangle x y).sign

Tactic:
by_cases hx : x = 0

Result:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x = 0
⊢ (o.oangle x (-y)).sign = -(o.oangle x y).sign

case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
⊢ (o.oangle x (-y)).sign = -(o.oangle x y).sign

Proof state:
case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : ¬y = 0
⊢ (o.oangle x (-y)).sign = -(o.oangle x y).sign

Tactic:
rw [o.oangle_neg_right hx hy, Real.Angle.sign_add_pi]

Result:
no goals

Proof state:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x = 0
⊢ (o.oangle x (-y)).sign = -(o.oangle x y).sign

Tactic:
simp [hx]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
protected lemma mul_le_of_le_div (k x y : ℕ) (h : x ≤ y / k) : x * k ≤ y

Proof state:
k x y : ℕ
h : x ≤ y / k
hk : ¬k = 0
⊢ x * k ≤ y

Tactic:
rwa [← le_div_iff_mul_le (Nat.pos_iff_ne_zero.2 hk)]

Result:
no goals

Proof state:
k x y : ℕ
h : x ≤ y / k
hk : k = 0
⊢ x * k ≤ y

Tactic:
rw [hk, Nat.mul_zero]

Result:
k x y : ℕ
h : x ≤ y / k
hk : k = 0
⊢ 0 ≤ y

Proof state:
k x y : ℕ
h : x ≤ y / k
hk : k = 0
⊢ 0 ≤ y

Tactic:
exact zero_le _

Result:
no goals

Proof state:
k x y : ℕ
h : x ≤ y / k
⊢ x * k ≤ y

Tactic:
if hk : k = 0 then
  rw [hk, Nat.mul_zero]; exact zero_le _
else
  rwa [← le_div_iff_mul_le (Nat.pos_iff_ne_zero.2 hk)]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem adjoint_id :
    ContinuousLinearMap.adjoint (ContinuousLinearMap.id 𝕜 E) = ContinuousLinearMap.id 𝕜 E

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
⊢ adjoint (id 𝕜 E) = id 𝕜 E

Tactic:
refine Eq.symm ?_

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
⊢ id 𝕜 E = adjoint (id 𝕜 E)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
⊢ id 𝕜 E = adjoint (id 𝕜 E)

Tactic:
rw [eq_adjoint_iff]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
⊢ ∀ (x y : E), ⟪(id 𝕜 E) x, y⟫_𝕜 = ⟪x, (id 𝕜 E) y⟫_𝕜

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
⊢ ∀ (x y : E), ⟪(id 𝕜 E) x, y⟫_𝕜 = ⟪x, (id 𝕜 E) y⟫_𝕜

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
/-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic. -/
@[fun_prop]
lemma AnalyticAt.pow {f : E → A} {z : E} (hf : AnalyticAt 𝕜 f z) (n : ℕ) :
    AnalyticAt 𝕜 (fun x ↦ f x ^ n) z

Proof state:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_8
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
f : E → A
z : E
hf : AnalyticWithinAt 𝕜 f Set.univ z
n : ℕ
⊢ AnalyticWithinAt 𝕜 (fun x => f x ^ n) Set.univ z

Tactic:
exact hf.pow n

Result:
no goals

Proof state:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_8
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
f : E → A
z : E
hf : AnalyticAt 𝕜 f z
n : ℕ
⊢ AnalyticAt 𝕜 (fun x => f x ^ n) z

Tactic:
rw [← analyticWithinAt_univ] at hf ⊢

Result:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_8
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
f : E → A
z : E
hf : AnalyticWithinAt 𝕜 f Set.univ z
n : ℕ
⊢ AnalyticWithinAt 𝕜 (fun x => f x ^ n) Set.univ z
-- Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean
lemma log_ofReal_of_pos {x : ℝ} (hx : 0 < x) : log (ENNReal.ofReal x) = Real.log x

Proof state:
x : ℝ
hx : 0 < x
⊢ (ENNReal.ofReal x).log = ↑(Real.log x)

Tactic:
rw [log_ofReal, if_neg hx.not_le]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem degree_T [Nontrivial R] (n : ℤ) : (T n : R[T;T⁻¹]).degree = n

Proof state:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℤ
⊢ (T n).degree = ↑n

Tactic:
rw [← one_mul (T n), ← map_one C]

Result:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℤ
⊢ (C 1 * T n).degree = ↑n

Proof state:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℤ
⊢ (C 1 * T n).degree = ↑n

Tactic:
exact degree_C_mul_T n 1 (one_ne_zero : (1 : R) ≠ 0)

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem exists_pos_lt_mul {a : α} (h : 0 < a) (b : α) : ∃ c : α, 0 < c ∧ b < c * a :=
  let ⟨c, hc₀, hc⟩ := exists_pos_mul_lt h b;
  ⟨c⁻¹, inv_pos.2 hc₀, by rwa [← div_eq_inv_mul, lt_div_iff₀ hc₀]⟩

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a : α
h : 0 < a
b c : α
hc₀ : 0 < c
hc : b * c < a
⊢ b < c⁻¹ * a

Tactic:
rwa [← div_eq_inv_mul, lt_div_iff₀ hc₀]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma exact_iff_of_epi_of_isIso_of_mono (φ : S₁ ⟶ S₂) [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] :
    S₁.Exact ↔ S₂.Exact

Proof state:
case mp
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ S₁.Exact → S₂.Exact

Tactic:
rintro ⟨h₁, z₁⟩

Result:
case mp.mk.intro
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
h₁ : S₁.HomologyData
z₁ : IsZero h₁.left.H
⊢ S₂.Exact

Proof state:
case mpr
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ S₂.Exact → S₁.Exact

Tactic:
rintro ⟨h₂, z₂⟩

Result:
case mpr.mk.intro
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
h₂ : S₂.HomologyData
z₂ : IsZero h₂.left.H
⊢ S₁.Exact

Proof state:
case mp.mk.intro
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
h₁ : S₁.HomologyData
z₁ : IsZero h₁.left.H
⊢ S₂.Exact

Tactic:
exact ⟨HomologyData.ofEpiOfIsIsoOfMono φ h₁, z₁⟩

Result:
no goals

Proof state:
case mpr.mk.intro
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
h₂ : S₂.HomologyData
z₂ : IsZero h₂.left.H
⊢ S₁.Exact

Tactic:
exact ⟨HomologyData.ofEpiOfIsIsoOfMono' φ h₂, z₂⟩

Result:
no goals

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ S₁.Exact ↔ S₂.Exact

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ S₁.Exact → S₂.Exact

case mpr
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ S₂.Exact → S₁.Exact
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem contains_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : a == b) :
    m.contains a = m.contains b

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
a b : α
hab : (a == b) = true
⊢ m.contains a = m.contains b

Tactic:
simp_to_raw using Raw₀.contains_congr

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem sub_add_cancel {n m : Nat} (h : m ≤ n) : n - m + m = n

Proof state:
n m : Nat
h : m ≤ n
⊢ n - m + m = n

Tactic:
rw [Nat.add_comm, Nat.add_sub_of_le h]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem kernMap_principal {s : Set α} : kernMap m (𝓟 s) = 𝓟 (kernImage m s)

Proof state:
α : Type u_1
β : Type u_2
m : α → β
s : Set α
g : Filter β
⊢ g ≤ kernMap m (𝓟 s) ↔ g ≤ 𝓟 (kernImage m s)

Tactic:
rw [← comap_le_iff_le_kernMap, le_principal_iff, le_principal_iff, mem_comap'']

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : α → β
s : Set α
⊢ kernMap m (𝓟 s) = 𝓟 (kernImage m s)

Tactic:
refine eq_of_forall_le_iff (fun g ↦ ?_)

Result:
α : Type u_1
β : Type u_2
m : α → β
s : Set α
g : Filter β
⊢ g ≤ kernMap m (𝓟 s) ↔ g ≤ 𝓟 (kernImage m s)
-- Mathlib/Data/ENNReal/Holder.lean
lemma lt_top_iff_one_lt : p < ∞ ↔ 1 < q

Proof state:
p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
⊢ 1 ≠ q ↔ 1 ≤ q ∧ 1 ≠ q

Tactic:
simp [one_le q p]

Result:
no goals

Proof state:
p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
⊢ p < ⊤ ↔ 1 < q

Tactic:
rw [lt_top_iff_ne_top, ne_top_iff_ne_one _ q, ne_comm, lt_iff_le_and_ne]

Result:
p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
⊢ 1 ≠ q ↔ 1 ≤ q ∧ 1 ≠ q
-- Mathlib/Algebra/Homology/ComplexShape.lean
lemma prev_eq_self' (c : ComplexShape ι) (j : ι) (hj : ∀ i, ¬ c.Rel i j) :
    c.prev j = j :=
  dif_neg (by simpa using hj)

Proof state:
ι : Type u_1
c : ComplexShape ι
j : ι
hj : ∀ (i : ι), ¬c.Rel i j
⊢ ¬∃ i, c.Rel i j

Tactic:
simpa using hj

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma negAddY_of_Z_eq_zero_left [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P)
    (hPz : P z = 0) : W'.negAddY P Q = P y ^ 2 * Q z * W'.negY Q

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -3 * 0 ^ 2 * Q x * Q y + 3 * 0 * Q x ^ 2 * P y - P y ^ 2 * Q y * Q z + P y * Q y ^ 2 * 0 + W'.a₁ * 0 * Q y ^ 2 * 0 -
                              W'.a₁ * Q x * P y ^ 2 * Q z -
                            W'.a₂ * 0 ^ 2 * Q y * Q z +
                          W'.a₂ * Q x ^ 2 * P y * 0 +
                        2 * W'.a₂ * 0 * Q x * P y * Q z -
                      2 * W'.a₂ * 0 * Q x * Q y * 0 -
                    W'.a₃ * P y ^ 2 * Q z ^ 2 +
                  W'.a₃ * Q y ^ 2 * 0 ^ 2 +
                W'.a₄ * 0 * P y * Q z ^ 2 -
              2 * W'.a₄ * 0 * Q y * 0 * Q z +
            2 * W'.a₄ * Q x * P y * 0 * Q z -
          W'.a₄ * Q x * Q y * 0 ^ 2 +
        3 * W'.a₆ * P y * 0 * Q z ^ 2 -
      3 * W'.a₆ * Q y * 0 ^ 2 * Q z =
    P y ^ 2 * Q z * (-Q y - W'.a₁ * Q x - W'.a₃ * Q z)

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.negAddY P Q = P y ^ 2 * Q z * W'.negY Q

Tactic:
rw [negAddY, hPz, X_eq_zero_of_Z_eq_zero hP hPz, negY]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -3 * 0 ^ 2 * Q x * Q y + 3 * 0 * Q x ^ 2 * P y - P y ^ 2 * Q y * Q z + P y * Q y ^ 2 * 0 + W'.a₁ * 0 * Q y ^ 2 * 0 -
                              W'.a₁ * Q x * P y ^ 2 * Q z -
                            W'.a₂ * 0 ^ 2 * Q y * Q z +
                          W'.a₂ * Q x ^ 2 * P y * 0 +
                        2 * W'.a₂ * 0 * Q x * P y * Q z -
                      2 * W'.a₂ * 0 * Q x * Q y * 0 -
                    W'.a₃ * P y ^ 2 * Q z ^ 2 +
                  W'.a₃ * Q y ^ 2 * 0 ^ 2 +
                W'.a₄ * 0 * P y * Q z ^ 2 -
              2 * W'.a₄ * 0 * Q y * 0 * Q z +
            2 * W'.a₄ * Q x * P y * 0 * Q z -
          W'.a₄ * Q x * Q y * 0 ^ 2 +
        3 * W'.a₆ * P y * 0 * Q z ^ 2 -
      3 * W'.a₆ * Q y * 0 ^ 2 * Q z =
    P y ^ 2 * Q z * (-Q y - W'.a₁ * Q x - W'.a₃ * Q z)
-- Mathlib/Algebra/Lie/BaseChange.lean
@[simp]
lemma baseChange_bot : (⊥ : LieSubmodule R L M).baseChange A = ⊥

Proof state:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ { toSubmodule := ⊥, lie_mem := ⋯ } = ⊥

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ baseChange A ⊥ = ⊥

Tactic:
simp only [baseChange, bot_toSubmodule, Submodule.baseChange_bot,
  Submodule.bot_toAddSubmonoid]

Result:
R : Type u_1
A : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ { toSubmodule := ⊥, lie_mem := ⋯ } = ⊥