harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem eq_pow_of_pell_lem {a y k : ℕ} (hy0 : y ≠ 0) (hk0 : k ≠ 0) (hyk : y ^ k < a) :
    (↑(y ^ k) : ℤ) < 2 * a * y - y * y - 1 :=
  have hya : y < a := (Nat.le_self_pow hk0 _).trans_lt hyk
  calc
    (↑(y ^ k) : ℤ) < a := Nat.cast_lt.2 hyk
    _ ≤ (a : ℤ) ^ 2 - (a - 1 : ℤ) ^ 2 - 1

Proof state:
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
⊢ ↑a ^ 2 - (↑a - ↑y) ^ 2 - 1 = 2 * ↑a * ↑y - ↑y * ↑y - 1

Tactic:
ring

Result:
no goals

Proof state:
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
⊢ ↑a ≤ ↑a ^ 2 - (↑a - 1) ^ 2 - 1

Tactic:
rw [sub_sq, mul_one, one_pow, sub_add, sub_sub_cancel, two_mul, sub_sub, ← add_sub,
  le_add_iff_nonneg_right, sub_nonneg, Int.add_one_le_iff]

Result:
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
⊢ 1 < ↑a

Proof state:
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
⊢ 1 < a

Tactic:
exact lt_of_le_of_lt (Nat.succ_le_of_lt (Nat.pos_of_ne_zero hy0)) hya

Result:
no goals

Proof state:
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
this : y ≤ a
⊢ ↑a ^ 2 - (↑a - 1) ^ 2 - 1 ≤ ↑a ^ 2 - (↑a - ↑y) ^ 2 - 1

Tactic:
gcongr <;> norm_cast <;> omega

Result:
no goals

Proof state:
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
⊢ 1 < ↑a

Tactic:
norm_cast

Result:
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
⊢ 1 < a

Proof state:
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
⊢ ↑a ^ 2 - (↑a - 1) ^ 2 - 1 ≤ ↑a ^ 2 - (↑a - ↑y) ^ 2 - 1

Tactic:
have := hya.le

Result:
a y k : ℕ
hy0 : y ≠ 0
hk0 : k ≠ 0
hyk : y ^ k < a
hya : y < a
this : y ≤ a
⊢ ↑a ^ 2 - (↑a - 1) ^ 2 - 1 ≤ ↑a ^ 2 - (↑a - ↑y) ^ 2 - 1
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem continuousOn_extend : ContinuousOn (f.extend I) (f.extend I).source

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ ContinuousOn (↑(f.symm.restr I.source).symm) f.source

Tactic:
exact f.continuousOn

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ ContinuousOn (↑(f.symm.restr I.source).symm) (f.extend I).source

Tactic:
rw [extend_source]

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ ContinuousOn (↑(f.symm.restr I.source).symm) f.source

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ ContinuousOn (↑(f.extend I)) (f.extend I).source

Tactic:
refine I.continuous.comp_continuousOn ?_

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ ContinuousOn (↑(f.symm.restr I.source).symm) (f.extend I).source
-- Mathlib/Data/Int/CardIntervalMod.lean
theorem count_modEq_card_eq_ceil (v : ℕ) :
    b.count (· ≡ v [MOD r]) = ⌈(b - (v % r : ℕ)) / (r : ℚ)⌉

Proof state:
b r : ℕ
hr : 0 < r
v : ℕ
⊢ 0 < ↑r

Tactic:
positivity

Result:
no goals

Proof state:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ v % r < r ∧ -↑(v % r) ≤ 0

Tactic:
exact ⟨mod_lt _ hr, by simp⟩

Result:
no goals

Proof state:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑b - ↑(v % r)) / ↑r⌉ - ⌈-↑(v % r) / ↑r⌉ = ⌈(↑b - ↑(v % r)) / ↑r⌉

Tactic:
rw [sub_eq_self, ceil_eq_zero_iff, Set.mem_Ioc, div_le_iff₀ hr', lt_div_iff₀ hr', neg_one_mul,
  zero_mul, neg_lt_neg_iff, cast_lt]

Result:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ v % r < r ∧ -↑(v % r) ≤ 0

Proof state:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑b - (↑(v % r) + ↑r * ↑(v / r))) / ↑r⌉ - ⌈(↑0 - (↑(v % r) + ↑r * ↑(v / r))) / ↑r⌉ = ?m.117730

Tactic:
simp_rw [← sub_sub, sub_div (_ - _), mul_div_cancel_left₀ _ hr'.ne', ceil_sub_nat]

Result:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑b - ↑(v % r)) / ↑r⌉ - ↑(v / r) - (⌈(↑0 - ↑(v % r)) / ↑r⌉ - ↑(v / r)) = ?m.117730

Proof state:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ↑(count (fun x => x ≡ v [MOD r]) b) = ⌈(↑b - ↑(v % r)) / ↑r⌉

Tactic:
rw [count_eq_card_filter_range, ← Ico_zero_eq_range, Ico_filter_modEq_card _ _ hr,
  max_eq_left (sub_nonneg.mpr <| by gcongr <;> positivity)]

Result:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑b - ↑v) / ↑r⌉ - ⌈(↑0 - ↑v) / ↑r⌉ = ⌈(↑b - ↑(v % r)) / ↑r⌉

Proof state:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑b - ↑v) / ↑r⌉ - ⌈(↑0 - ↑v) / ↑r⌉ = ⌈(↑b - ↑(v % r)) / ↑r⌉

Tactic:
conv_lhs =>
  rw [← div_add_mod v r, cast_add, cast_mul, add_comm]
  tactic => simp_rw [← sub_sub, sub_div (_ - _), mul_div_cancel_left₀ _ hr'.ne', ceil_sub_nat]
  rw [sub_sub_sub_cancel_right, cast_zero, zero_sub]

Result:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑b - ↑(v % r)) / ↑r⌉ - ⌈-↑(v % r) / ↑r⌉ = ⌈(↑b - ↑(v % r)) / ↑r⌉

Proof state:
b r : ℕ
hr : 0 < r
v : ℕ
⊢ ↑(count (fun x => x ≡ v [MOD r]) b) = ⌈(↑b - ↑(v % r)) / ↑r⌉

Tactic:
have hr' : 0 < (r : ℚ) := by positivity

Result:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ↑(count (fun x => x ≡ v [MOD r]) b) = ⌈(↑b - ↑(v % r)) / ↑r⌉

Proof state:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ⌈(↑0 - ↑v) / ↑r⌉ ≤ ⌈(↑b - ↑v) / ↑r⌉

Tactic:
gcongr <;> positivity

Result:
no goals

Proof state:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ -↑(v % r) ≤ 0

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem descPochhammer_eq_ascPochhammer (n : ℕ) :
    descPochhammer ℤ n = (ascPochhammer ℤ n).comp ((X : ℤ[X]) - n + 1)

Proof state:
case zero

⊢ descPochhammer ℤ 0 = (ascPochhammer ℤ 0).comp (X - ↑0 + 1)

Tactic:
rw [descPochhammer_zero, ascPochhammer_zero, one_comp]

Result:
no goals

Proof state:
case succ
n : ℕ
ih : descPochhammer ℤ n = (ascPochhammer ℤ n).comp (X - ↑n + 1)
⊢ descPochhammer ℤ (n + 1) = (ascPochhammer ℤ (n + 1)).comp (X - ↑(n + 1) + 1)

Tactic:
rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_right,
  ascPochhammer_succ_left, ih, X_mul, mul_X_comp, comp_assoc, add_comp, X_comp, one_comp]

Result:
no goals

Proof state:
n : ℕ
⊢ descPochhammer ℤ n = (ascPochhammer ℤ n).comp (X - ↑n + 1)

Tactic:
induction n with
| zero => rw [descPochhammer_zero, ascPochhammer_zero, one_comp]
| succ n ih =>
  rw [Nat.cast_succ, sub_add, add_sub_cancel_right, descPochhammer_succ_right,
    ascPochhammer_succ_left, ih, X_mul, mul_X_comp, comp_assoc, add_comp, X_comp, one_comp]

Result:
no goals
-- Mathlib/Data/Set/Finite/List.lean
lemma finite_length_lt : {l : List α | l.length < n}.Finite

Proof state:
case h.e'_2.h
α : Type u_1
inst✝ : Finite α
n : ℕ
x✝ : List α
⊢ x✝ ∈ {l | l.length < n} ↔ x✝ ∈ ⋃ i ∈ ↑(Finset.range n), {l | l.length = i}

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_2
α : Type u_1
inst✝ : Finite α
n : ℕ
⊢ {l | l.length < n} = ⋃ i ∈ ↑(Finset.range n), {l | l.length = i}

Tactic:
ext

Result:
case h.e'_2.h
α : Type u_1
inst✝ : Finite α
n : ℕ
x✝ : List α
⊢ x✝ ∈ {l | l.length < n} ↔ x✝ ∈ ⋃ i ∈ ↑(Finset.range n), {l | l.length = i}

Proof state:
α : Type u_1
inst✝ : Finite α
n : ℕ
⊢ {l | l.length < n}.Finite

Tactic:
convert (Finset.range n).finite_toSet.biUnion fun i _ ↦ finite_length_eq α i

Result:
case h.e'_2
α : Type u_1
inst✝ : Finite α
n : ℕ
⊢ {l | l.length < n} = ⋃ i ∈ ↑(Finset.range n), {l | l.length = i}
-- Mathlib/Algebra/Homology/ComplexShapeSigns.lean
lemma associative_ε₁_eq_mul (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) :
    ε₁ c₁ c₂₃ c (i₁, π c₂ c₃ c₂₃ (i₂, i₃)) =
      ε₁ c₁₂ c₃ c (π c₁ c₂ c₁₂ (i₁, i₂), i₃) * ε₁ c₁ c₂ c₁₂ (i₁, i₂)

Proof state:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : TotalComplexShape c₁₂ c₃ c
inst✝² : TotalComplexShape c₂ c₃ c₂₃
inst✝¹ : TotalComplexShape c₁ c₂₃ c
inst✝ : c₁.Associative c₂ c₃ c₁₂ c₂₃ c
i₁ : I₁
i₂ : I₂
i₃ : I₃
⊢ c₁.ε₁ c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) = c₁₂.ε₁ c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₁ c₂ c₁₂ (i₁, i₂)

Tactic:
apply Associative.ε₁_eq_mul

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
protected lemma MemLp.condExp (hf : MemLp f 2 μ) : MemLp (μ[f | m]) 2 μ

Proof state:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : InnerProductSpace ℝ E
hf : MemLp f 2 μ
⊢ MemLp (μ[f|m]) 2 μ

Tactic:
by_cases hm : m ≤ m₀

Result:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : InnerProductSpace ℝ E
hf : MemLp f 2 μ
hm : m ≤ m₀
⊢ MemLp (μ[f|m]) 2 μ

case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : InnerProductSpace ℝ E
hf : MemLp f 2 μ
hm : ¬m ≤ m₀
⊢ MemLp (μ[f|m]) 2 μ

Proof state:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : InnerProductSpace ℝ E
hf : MemLp f 2 μ
hm : ¬m ≤ m₀
⊢ MemLp (μ[f|m]) 2 μ

Tactic:
simp [condExp_of_not_le hm]

Result:
no goals

Proof state:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : InnerProductSpace ℝ E
hf : MemLp f 2 μ
hm : m ≤ m₀
⊢ MemLp (μ[f|m]) 2 μ

Tactic:
exact ⟨(stronglyMeasurable_condExp.mono hm).aestronglyMeasurable,
  eLpNorm_condExp_le.trans_lt hf.eLpNorm_lt_top⟩

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[reassoc (attr := simp)]
lemma d_snd_v' (n : ℤ) :
    (mappingCone φ).d (n - 1) n ≫ (snd φ).v n n (add_zero n) =
    (fst φ : Cochain (mappingCone φ) F 1).v (n - 1) n (by omega) ≫ φ.f n +
      (snd φ).v (n - 1) (n - 1) (add_zero _) ≫ G.d (n - 1) n

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
n : ℤ
⊢ (mappingCone φ).d (n - 1) n ≫ (snd φ).v n n ⋯ =
    (↑(fst φ)).v (n - 1) n ⋯ ≫ φ.f n + (snd φ).v (n - 1) (n - 1) ⋯ ≫ G.d (n - 1) n

Tactic:
apply d_snd_v

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.105015, u_1} C
inst✝³ : Category.{?u.105019, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
n : ℤ
⊢ n - 1 + 1 = n

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/BigOperators/GroupWithZero/Finset.lean
lemma prod_ne_zero_iff : ∏ x ∈ s, f x ≠ 0 ↔ ∀ a ∈ s, f a ≠ 0

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝² : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
⊢ (¬∃ a ∈ s, f a = 0) ↔ ∀ a ∈ s, f a ≠ 0

Tactic:
push_neg

Result:
ι : Type u_1
M₀ : Type u_4
inst✝² : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
⊢ (∀ a ∈ s, f a ≠ 0) ↔ ∀ a ∈ s, f a ≠ 0

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝² : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
⊢ (∀ a ∈ s, f a ≠ 0) ↔ ∀ a ∈ s, f a ≠ 0

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝² : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
⊢ ∏ x ∈ s, f x ≠ 0 ↔ ∀ a ∈ s, f a ≠ 0

Tactic:
rw [Ne, prod_eq_zero_iff]

Result:
ι : Type u_1
M₀ : Type u_4
inst✝² : CommMonoidWithZero M₀
f : ι → M₀
s : Finset ι
inst✝¹ : Nontrivial M₀
inst✝ : NoZeroDivisors M₀
⊢ (¬∃ a ∈ s, f a = 0) ↔ ∀ a ∈ s, f a ≠ 0
-- Mathlib/Topology/Algebra/GroupWithZero.lean
theorem continuousAt_zpow₀ (x : G₀) (m : ℤ) (h : x ≠ 0 ∨ 0 ≤ m) :
    ContinuousAt (fun x => x ^ m) x

Proof state:
case negSucc
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.negSucc m
hx : x ≠ 0
⊢ ContinuousAt (fun x => (x ^ (m + 1))⁻¹) x

Tactic:
exact (continuousAt_pow x (m + 1)).inv₀ (pow_ne_zero _ hx)

Result:
no goals

Proof state:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℤ
h : x ≠ 0 ∨ 0 ≤ m
⊢ ContinuousAt (fun x => x ^ m) x

Tactic:
rcases m with m | m

Result:
case ofNat
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.ofNat m
⊢ ContinuousAt (fun x => x ^ Int.ofNat m) x

case negSucc
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.negSucc m
⊢ ContinuousAt (fun x => x ^ Int.negSucc m) x

Proof state:
case negSucc
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.negSucc m
⊢ ContinuousAt (fun x => x ^ Int.negSucc m) x

Tactic:
simp only [zpow_negSucc]

Result:
case negSucc
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.negSucc m
⊢ ContinuousAt (fun x => (x ^ (m + 1))⁻¹) x

Proof state:
case negSucc
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.negSucc m
⊢ ContinuousAt (fun x => (x ^ (m + 1))⁻¹) x

Tactic:
have hx : x ≠ 0 := h.resolve_right (Int.negSucc_lt_zero m).not_le

Result:
case negSucc
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.negSucc m
hx : x ≠ 0
⊢ ContinuousAt (fun x => (x ^ (m + 1))⁻¹) x

Proof state:
case ofNat
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : HasContinuousInv₀ G₀
inst✝ : ContinuousMul G₀
x : G₀
m : ℕ
h : x ≠ 0 ∨ 0 ≤ Int.ofNat m
⊢ ContinuousAt (fun x => x ^ Int.ofNat m) x

Tactic:
simpa only [Int.ofNat_eq_coe, zpow_natCast] using continuousAt_pow x m

Result:
no goals
-- Mathlib/AlgebraicTopology/TopologicalSimplex.lean
lemma toTopObj_one_coe_add_coe_eq_one (f : ⦋1⦌.toTopObj) : (f 0 : ℝ) + f 1 = 1

Proof state:
f : ↑⦋1⦌.toTopObj
⊢ ↑f 0 + ↑f 1 = 1

Tactic:
rw [toTopObj_one_add_eq_one]

Result:
no goals

Proof state:
f : ↑⦋1⦌.toTopObj
⊢ ↑(↑f 0) + ↑(↑f 1) = 1

Tactic:
norm_cast

Result:
f : ↑⦋1⦌.toTopObj
⊢ ↑f 0 + ↑f 1 = 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem cond_true_left   : ∀(c f : Bool), cond c true f  = ( c || f)

Proof state:
⊢ ∀ (c f : Bool), (bif c then true else f) = (c || f)

Tactic:
decide

Result:
no goals
-- Mathlib/RingTheory/Localization/NormTrace.lean
theorem Algebra.discr_localizationLocalization (b : Basis ι R S) :
    Algebra.discr Rₘ (b.localizationLocalization Rₘ M Sₘ) =
    algebraMap R Rₘ (Algebra.discr R b)

Proof state:
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
Rₘ : Type u_3
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : Algebra R Rₘ
M : Submonoid R
inst✝⁹ : IsLocalization M Rₘ
Sₘ : Type u_5
inst✝⁸ : CommRing Sₘ
inst✝⁷ : Algebra S Sₘ
inst✝⁶ : Algebra Rₘ Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
ι : Type u_6
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
⊢ discr Rₘ ⇑(Basis.localizationLocalization Rₘ M Sₘ b) = (algebraMap R Rₘ) (discr R ⇑b)

Tactic:
rw [Algebra.discr_def, Algebra.discr_def, RingHom.map_det,
  Algebra.traceMatrix_localizationLocalization]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem drop_empty {n : Nat} : "".drop n = ""

Proof state:
n : Nat
⊢ "".drop n = ""

Tactic:
rw [drop_eq, List.drop_nil]

Result:
no goals
-- Mathlib/Topology/Irreducible.lean
theorem isPreirreducible_iff_closure : IsPreirreducible (closure s) ↔ IsPreirreducible s :=
  forall₄_congr fun u v hu hv => by
    iterate 3 rw [closure_inter_open_nonempty_iff]
    exacts [hu.inter hv, hv, hu]

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s u v : Set X
hu : IsOpen u
hv : IsOpen v
⊢ (s ∩ u).Nonempty → (s ∩ v).Nonempty → (closure s ∩ (u ∩ v)).Nonempty ↔
    (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty

X : Type u_1
inst✝ : TopologicalSpace X
s u v : Set X
hu : IsOpen u
hv : IsOpen v
⊢ IsOpen v

X : Type u_1
inst✝ : TopologicalSpace X
s u v : Set X
hu : IsOpen u
hv : IsOpen v
⊢ IsOpen u

Tactic:
rw [closure_inter_open_nonempty_iff]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s u v : Set X
hu : IsOpen u
hv : IsOpen v
⊢ IsOpen (u ∩ v)

X : Type u_1
inst✝ : TopologicalSpace X
s u v : Set X
hu : IsOpen u
hv : IsOpen v
⊢ IsOpen v

X : Type u_1
inst✝ : TopologicalSpace X
s u v : Set X
hu : IsOpen u
hv : IsOpen v
⊢ IsOpen u

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s u v : Set X
hu : IsOpen u
hv : IsOpen v
⊢ (closure s ∩ u).Nonempty → (closure s ∩ v).Nonempty → (closure s ∩ (u ∩ v)).Nonempty ↔
    (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty

Tactic:
iterate 3 rw [closure_inter_open_nonempty_iff]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s u v : Set X
hu : IsOpen u
hv : IsOpen v
⊢ IsOpen (u ∩ v)

X : Type u_1
inst✝ : TopologicalSpace X
s u v : Set X
hu : IsOpen u
hv : IsOpen v
⊢ IsOpen v

X : Type u_1
inst✝ : TopologicalSpace X
s u v : Set X
hu : IsOpen u
hv : IsOpen v
⊢ IsOpen u

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s u v : Set X
hu : IsOpen u
hv : IsOpen v
⊢ IsOpen (u ∩ v)

X : Type u_1
inst✝ : TopologicalSpace X
s u v : Set X
hu : IsOpen u
hv : IsOpen v
⊢ IsOpen v

X : Type u_1
inst✝ : TopologicalSpace X
s u v : Set X
hu : IsOpen u
hv : IsOpen v
⊢ IsOpen u

Tactic:
exacts [hu.inter hv, hv, hu]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem filter_lt_le_eq_Ioc [DecidablePred fun j => a < j ∧ j ≤ b] :
    ({j | a < j ∧ j ≤ b} : Finset _) = Ioc a b

Proof state:
α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j => a < j ∧ j ≤ b
⊢ filter (fun j => a < j ∧ j ≤ b) univ = Ioc a b

Tactic:
ext

Result:
case h
α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j => a < j ∧ j ≤ b
a✝ : α
⊢ a✝ ∈ filter (fun j => a < j ∧ j ≤ b) univ ↔ a✝ ∈ Ioc a b

Proof state:
case h
α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j => a < j ∧ j ≤ b
a✝ : α
⊢ a✝ ∈ filter (fun j => a < j ∧ j ≤ b) univ ↔ a✝ ∈ Ioc a b

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
theorem rTensor_exact : Exact (rTensor Q f) (rTensor Q g)

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
⊢ Exact ⇑(rTensor Q f) ⇑(rTensor Q g)

Tactic:
rw [rTensor_exact_iff_lTensor_exact]

Result:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
⊢ Exact ⇑(lTensor Q f) ⇑(lTensor Q g)

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
⊢ Exact ⇑(lTensor Q f) ⇑(lTensor Q g)

Tactic:
exact lTensor_exact Q hfg hg

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem neg_toSimpleFunc (f : Lp.simpleFunc E p μ) : toSimpleFunc (-f) =ᵐ[μ] -toSimpleFunc f

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
⊢ ⇑(toSimpleFunc (-f)) =ᶠ[ae μ] -⇑(toSimpleFunc f)

Tactic:
filter_upwards [toSimpleFunc_eq_toFun (-f), toSimpleFunc_eq_toFun f,
  Lp.coeFn_neg (f : Lp E p μ)] with _

Result:
case h
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
a✝ : α
⊢ (toSimpleFunc (-f)) a✝ = ↑↑↑(-f) a✝ →
    (toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑↑(-↑f) a✝ = (-↑↑↑f) a✝ → (toSimpleFunc (-f)) a✝ = (-⇑(toSimpleFunc f)) a✝

Proof state:
case h
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
a✝ : α
h✝¹ : (toSimpleFunc (-f)) a✝ = ↑(-↑↑f) a✝
h✝ : (toSimpleFunc f) a✝ = ↑↑↑f a✝
h : ↑(-↑↑f) a✝ = -↑↑↑f a✝
⊢ ↑(-↑↑f) a✝ = -↑↑↑f a✝

Tactic:
rw [h]

Result:
no goals

Proof state:
case h
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
a✝ : α
⊢ (toSimpleFunc (-f)) a✝ = ↑(-↑↑f) a✝ →
    (toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑(-↑↑f) a✝ = -↑↑↑f a✝ → (toSimpleFunc (-f)) a✝ = -(toSimpleFunc f) a✝

Tactic:
repeat intro h; rw [h]

Result:
no goals

Proof state:
case h
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
a✝ : α
⊢ (toSimpleFunc (-f)) a✝ = ↑↑↑(-f) a✝ →
    (toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑↑(-↑f) a✝ = (-↑↑↑f) a✝ → (toSimpleFunc (-f)) a✝ = (-⇑(toSimpleFunc f)) a✝

Tactic:
simp only [Pi.neg_apply, AddSubgroup.coe_neg]

Result:
case h
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
a✝ : α
⊢ (toSimpleFunc (-f)) a✝ = ↑(-↑↑f) a✝ →
    (toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑(-↑↑f) a✝ = -↑↑↑f a✝ → (toSimpleFunc (-f)) a✝ = -(toSimpleFunc f) a✝

Proof state:
case h
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
a✝ : α
h✝ : (toSimpleFunc (-f)) a✝ = ↑(-↑↑f) a✝
h : (toSimpleFunc f) a✝ = ↑↑↑f a✝
⊢ ↑(-↑↑f) a✝ = -↑↑↑f a✝ → ↑(-↑↑f) a✝ = -↑↑↑f a✝

Tactic:
intro h

Result:
case h
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
a✝ : α
h✝¹ : (toSimpleFunc (-f)) a✝ = ↑(-↑↑f) a✝
h✝ : (toSimpleFunc f) a✝ = ↑↑↑f a✝
h : ↑(-↑↑f) a✝ = -↑↑↑f a✝
⊢ ↑(-↑↑f) a✝ = -↑↑↑f a✝