harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Coprime/Lemmas.lean
theorem exists_sum_eq_one_iff_pairwise_coprime [DecidableEq I] (h : t.Nonempty) :
    (∃ μ : I → R, (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) = 1) ↔
      Pairwise (IsCoprime on fun i : t ↦ s i)

Proof state:
case cons.mp.intro.refine_2.refine_1.e_a.e_a.e_s
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ : μ a * ∏ j ∈ t, s j + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
x : I
hx : x ∈ t
⊢ t \ {x} = (insert a t \ {x}) \ {a}

Tactic:
rw [sdiff_sdiff_comm, sdiff_singleton_eq_erase a, erase_insert hat]

Result:
no goals

Proof state:
case h.e_a.e_a.e_a.e_s
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i => s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
hs : Pairwise (IsCoprime on fun a => s ↑a)
Hb : ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1
u v : R
huv : u * ∏ i ∈ t, s i + v * s a = 1
hμ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
x : I
hx : x ∈ t
⊢ (insert a t \ {x}) \ {a} = t \ {x}

Tactic:
rw [sdiff_sdiff_comm, sdiff_singleton_eq_erase a, erase_insert hat]

Result:
no goals
-- Mathlib/Analysis/Complex/OpenMapping.lean
theorem AnalyticAt.eventually_constant_or_nhds_le_map_nhds {z₀ : E} (hg : AnalyticAt ℂ g z₀) :
    (∀ᶠ z in 𝓝 z₀, g z = g z₀) ∨ 𝓝 (g z₀) ≤ map g (𝓝 z₀)

Proof state:
case intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun z t => z₀ + t • z
gray : E → ℂ → ℂ := fun z => g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x | AnalyticAt ℂ g x}
h1 : ∀ z ∈ sphere 0 1, AnalyticOnNhd ℂ (gray z) (ball 0 r)
⊢ (∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀) ∨ 𝓝 (g z₀) ≤ map g (𝓝 z₀)

Tactic:
by_cases h : ∀ z ∈ sphere (0 : E) 1, ∀ᶠ t in 𝓝 0, gray z t = gray z 0

Result:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun z t => z₀ + t • z
gray : E → ℂ → ℂ := fun z => g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x | AnalyticAt ℂ g x}
h1 : ∀ z ∈ sphere 0 1, AnalyticOnNhd ℂ (gray z) (ball 0 r)
h : ∀ z ∈ sphere 0 1, ∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
⊢ (∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀) ∨ 𝓝 (g z₀) ≤ map g (𝓝 z₀)

case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun z t => z₀ + t • z
gray : E → ℂ → ℂ := fun z => g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x | AnalyticAt ℂ g x}
h1 : ∀ z ∈ sphere 0 1, AnalyticOnNhd ℂ (gray z) (ball 0 r)
h : ¬∀ z ∈ sphere 0 1, ∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
⊢ (∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀) ∨ 𝓝 (g z₀) ≤ map g (𝓝 z₀)

Proof state:
case pos.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun z t => z₀ + t • z
gray : E → ℂ → ℂ := fun z => g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x | AnalyticAt ℂ g x}
h1 : ∀ z ∈ sphere 0 1, AnalyticOnNhd ℂ (gray z) (ball 0 r)
h : ∀ z ∈ sphere 0 1, ∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
z : E
hz : z ∈ ball z₀ r
h' : ‖z - z₀‖ ≠ 0
w : E := ‖z - z₀‖⁻¹ • (z - z₀)
h3 : ∀ t ∈ ball 0 r, gray w t = g z₀
⊢ g z = g z₀

Tactic:
have h4 : ‖z - z₀‖ < r := by simpa [dist_eq_norm] using mem_ball.mp hz

Result:
case pos.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
g : E → ℂ
z₀ : E
hg : AnalyticAt ℂ g z₀
ray : E → ℂ → E := fun z t => z₀ + t • z
gray : E → ℂ → ℂ := fun z => g ∘ ray z
r : ℝ
hr : r > 0
hgr : ball z₀ r ⊆ {x | AnalyticAt ℂ g x}
h1 : ∀ z ∈ sphere 0 1, AnalyticOnNhd ℂ (gray z) (ball 0 r)
h : ∀ z ∈ sphere 0 1, ∀ᶠ (t : ℂ) in 𝓝 0, gray z t = gray z 0
z : E
hz : z ∈ ball z₀ r
h' : ‖z - z₀‖ ≠ 0
w : E := ‖z - z₀‖⁻¹ • (z - z₀)
h3 : ∀ t ∈ ball 0 r, gray w t = g z₀
h4 : ‖z - z₀‖ < r
⊢ g z = g z₀
-- Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean
protected lemma GrowsPolynomially.add {f g : ℝ → ℝ} (hf : GrowsPolynomially f)
    (hg : GrowsPolynomially g) (hf' : 0 ≤ᶠ[atTop] f) (hg' : 0 ≤ᶠ[atTop] g) :
    GrowsPolynomially fun x => f x + g x

Proof state:
case h
f g : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hg✝¹ : GrowsPolynomially g
hf'✝ : 0 ≤ᶠ[atTop] f
hg'✝ : 0 ≤ᶠ[atTop] g
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf✝ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
left✝ : c₄ > 0
hg✝ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hg : ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)
hf' : ∀ (y : ℝ), b * id x ≤ y → 0 y ≤ f y
hg' : ∀ (y : ℝ), b * id x ≤ y → 0 y ≤ g y
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ f u + g u ∈ Set.Icc ((c₁ ⊓ c₃) * (f x + g x)) ((c₂ ⊔ c₄) * (f x + g x))

Tactic:
have hbx : b * x ≤ x := calc
  b * x ≤ 1 * x := by gcongr; exact le_of_lt hb.2
      _ = x := by ring

Result:
case h
f g : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hg✝¹ : GrowsPolynomially g
hf'✝ : 0 ≤ᶠ[atTop] f
hg'✝ : 0 ≤ᶠ[atTop] g
b : ℝ
hb : b ∈ Set.Ioo 0 1
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf✝ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
c₃ : ℝ
hc₃_mem : c₃ > 0
c₄ : ℝ
left✝ : c₄ > 0
hg✝ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)
x : ℝ
hf : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
hg : ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)
hf' : ∀ (y : ℝ), b * id x ≤ y → 0 y ≤ f y
hg' : ∀ (y : ℝ), b * id x ≤ y → 0 y ≤ g y
hx_pos : 0 ≤ x
u : ℝ
hu : u ∈ Set.Icc (b * x) x
hbx : b * x ≤ x
⊢ f u + g u ∈ Set.Icc ((c₁ ⊓ c₃) * (f x + g x)) ((c₂ ⊔ c₄) * (f x + g x))
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem integral_smul (c : 𝕜) (f : α →₁[μ] E) : integral (c • f) = c • integral f

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝⁵ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : CompleteSpace E
c : 𝕜
f : ↥(Lp E 1 μ)
⊢ integralCLM (c • f) = c • integralCLM f

Tactic:
show (integralCLM' 𝕜) (c • f) = c • (integralCLM' 𝕜) f

Result:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝⁵ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : CompleteSpace E
c : 𝕜
f : ↥(Lp E 1 μ)
⊢ (integralCLM' 𝕜) (c • f) = c • (integralCLM' 𝕜) f

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝⁵ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : CompleteSpace E
c : 𝕜
f : ↥(Lp E 1 μ)
⊢ (integralCLM' 𝕜) (c • f) = c • (integralCLM' 𝕜) f

Tactic:
exact _root_.map_smul (integralCLM' 𝕜) c f

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝⁵ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : CompleteSpace E
c : 𝕜
f : ↥(Lp E 1 μ)
⊢ integral (c • f) = c • integral f

Tactic:
simp only [integral]

Result:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝⁵ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : CompleteSpace E
c : 𝕜
f : ↥(Lp E 1 μ)
⊢ integralCLM (c • f) = c • integralCLM f
-- Mathlib/Analysis/Convex/Gauge.lean
theorem one_le_gauge_of_not_mem (hs₁ : StarConvex ℝ 0 s) (hs₂ : Absorbs ℝ s {x}) (hx : x ∉ s) :
    1 ≤ gauge s x :=
  le_gauge_of_not_mem hs₁ hs₂ <| by rwa [one_smul]

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x : E
hs₁ : StarConvex ℝ 0 s
hs₂ : Absorbs ℝ s {x}
hx : x ∉ s
⊢ x ∉ 1 • s

Tactic:
rwa [one_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_two_pow_sub_succ (h₂ : x < 2 ^ n) (i : Nat) :
    testBit (2^n - (x + 1)) i = (decide (i < n) && ! testBit x i)

Proof state:
case succ
i : Nat
ih : ∀ {x n : Nat}, x < 2 ^ n → (2 ^ n - (x + 1)).testBit i = (decide (i < n) && !x.testBit i)
x n : Nat
h₂ : x < 2 ^ n
⊢ (2 ^ n - (x + 1)).testBit (i + 1) = (decide (i + 1 < n) && !x.testBit (i + 1))

Tactic:
simp only [testBit_succ]

Result:
case succ
i : Nat
ih : ∀ {x n : Nat}, x < 2 ^ n → (2 ^ n - (x + 1)).testBit i = (decide (i < n) && !x.testBit i)
x n : Nat
h₂ : x < 2 ^ n
⊢ ((2 ^ n - (x + 1)) / 2).testBit i = (decide (i + 1 < n) && !(x / 2).testBit i)

Proof state:
x n : Nat
h₂ : x < 2 ^ 0
⊢ (2 ^ 0 - (x + 1)).testBit 0 = (decide (0 < 0) && !x.testBit 0)

Tactic:
simp [succ_sub_succ_eq_sub]

Result:
no goals

Proof state:
i : Nat
ih : ∀ {x n : Nat}, x < 2 ^ n → (2 ^ n - (x + 1)).testBit i = (decide (i < n) && !x.testBit i)
x n✝ n : Nat
h₂ : x < 2 ^ (n + 1)
⊢ x / 2 < 2 ^ n

Tactic:
omega

Result:
no goals

Proof state:
case zero
x n : Nat
h₂ : x < 2 ^ n
⊢ (2 ^ n - (x + 1)).testBit 0 = (decide (0 < n) && !x.testBit 0)

Tactic:
match n with
| 0 => simp [succ_sub_succ_eq_sub]
| n+1 =>
  simp [not_decide_mod_two_eq_one]
  omega

Result:
no goals

Proof state:
x n✝ n : Nat
h₂ : x < 2 ^ (n + 1)
⊢ (2 ^ (n + 1) - (x + 1)) % 2 = 1 ↔ x % 2 = 0

Tactic:
omega

Result:
no goals

Proof state:
i : Nat
ih : ∀ {x n : Nat}, x < 2 ^ n → (2 ^ n - (x + 1)).testBit i = (decide (i < n) && !x.testBit i)
x n : Nat
h₂ : x < 2 ^ 0
⊢ ((2 ^ 0 - (x + 1)) / 2).testBit i = (decide (i + 1 < 0) && !(x / 2).testBit i)

Tactic:
simp [decide_eq_false, succ_sub_succ_eq_sub]

Result:
no goals

Proof state:
i : Nat
ih : ∀ {x n : Nat}, x < 2 ^ n → (2 ^ n - (x + 1)).testBit i = (decide (i < n) && !x.testBit i)
x n✝ n : Nat
h₂ : x < 2 ^ (n + 1)
⊢ (decide (i < n) && !(x / 2).testBit i) = (decide (i + 1 < n + 1) && !(x / 2).testBit i)

Tactic:
simp [Nat.succ_lt_succ_iff]

Result:
no goals

Proof state:
x n✝ n : Nat
h₂ : x < 2 ^ (n + 1)
⊢ (2 ^ (n + 1) - (x + 1)).testBit 0 = (decide (0 < n + 1) && !x.testBit 0)

Tactic:
simp [not_decide_mod_two_eq_one]

Result:
x n✝ n : Nat
h₂ : x < 2 ^ (n + 1)
⊢ (2 ^ (n + 1) - (x + 1)) % 2 = 1 ↔ x % 2 = 0

Proof state:
i : Nat
ih : ∀ {x n : Nat}, x < 2 ^ n → (2 ^ n - (x + 1)).testBit i = (decide (i < n) && !x.testBit i)
x n✝ n : Nat
h₂ : x < 2 ^ (n + 1)
⊢ ((2 ^ (n + 1) - (x + 1)) / 2).testBit i = (decide (i + 1 < n + 1) && !(x / 2).testBit i)

Tactic:
rw [Nat.two_pow_succ_sub_succ_div_two, ih]

Result:
i : Nat
ih : ∀ {x n : Nat}, x < 2 ^ n → (2 ^ n - (x + 1)).testBit i = (decide (i < n) && !x.testBit i)
x n✝ n : Nat
h₂ : x < 2 ^ (n + 1)
⊢ (decide (i < n) && !(x / 2).testBit i) = (decide (i + 1 < n + 1) && !(x / 2).testBit i)

i : Nat
ih : ∀ {x n : Nat}, x < 2 ^ n → (2 ^ n - (x + 1)).testBit i = (decide (i < n) && !x.testBit i)
x n✝ n : Nat
h₂ : x < 2 ^ (n + 1)
⊢ x / 2 < 2 ^ n
-- Mathlib/Geometry/Manifold/MFDeriv/Defs.lean
theorem differentiableWithinAt_localInvariantProp :
    (contDiffGroupoid 1 I).LocalInvariantProp (contDiffGroupoid 1 I')
      (DifferentiableWithinAtProp I I') :=
  { is_local

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
f : H → H'
e' : PartialHomeomorph H' H'
he' : e' ∈ contDiffGroupoid 1 I'
hs : s ⊆ f ⁻¹' e'.source
hx : f x ∈ e'.source
h : DifferentiableWithinAt 𝕜 (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)
A : (↑I' ∘ f ∘ ↑I.symm) (↑I x) ∈ ↑I'.symm ⁻¹' e'.source ∩ range ↑I'
this : ContDiffWithinAt 𝕜 1 (↑I' ∘ ↑e' ∘ ↑I'.symm) (↑I'.symm ⁻¹' e'.source ∩ range ↑I') ((↑I' ∘ f ∘ ↑I.symm) (↑I x))
⊢ DifferentiableWithinAt 𝕜 (↑I' ∘ (↑e' ∘ f) ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)

Tactic:
convert (this.differentiableWithinAt le_rfl).comp _ h _

Result:
case h.e'_11
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
f : H → H'
e' : PartialHomeomorph H' H'
he' : e' ∈ contDiffGroupoid 1 I'
hs : s ⊆ f ⁻¹' e'.source
hx : f x ∈ e'.source
h : DifferentiableWithinAt 𝕜 (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)
A : (↑I' ∘ f ∘ ↑I.symm) (↑I x) ∈ ↑I'.symm ⁻¹' e'.source ∩ range ↑I'
this : ContDiffWithinAt 𝕜 1 (↑I' ∘ ↑e' ∘ ↑I'.symm) (↑I'.symm ⁻¹' e'.source ∩ range ↑I') ((↑I' ∘ f ∘ ↑I.symm) (↑I x))
⊢ ↑I' ∘ (↑e' ∘ f) ∘ ↑I.symm = (↑I' ∘ ↑e' ∘ ↑I'.symm) ∘ ↑I' ∘ f ∘ ↑I.symm

𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
E' : Type u_5
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
s : Set H
x : H
f : H → H'
e' : PartialHomeomorph H' H'
he' : e' ∈ contDiffGroupoid 1 I'
hs : s ⊆ f ⁻¹' e'.source
hx : f x ∈ e'.source
h : DifferentiableWithinAt 𝕜 (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I x)
A : (↑I' ∘ f ∘ ↑I.symm) (↑I x) ∈ ↑I'.symm ⁻¹' e'.source ∩ range ↑I'
this : ContDiffWithinAt 𝕜 1 (↑I' ∘ ↑e' ∘ ↑I'.symm) (↑I'.symm ⁻¹' e'.source ∩ range ↑I') ((↑I' ∘ f ∘ ↑I.symm) (↑I x))
⊢ MapsTo (↑I' ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ range ↑I) (↑I'.symm ⁻¹' e'.source ∩ range ↑I')
-- Mathlib/.lake/packages/lean4/src/lean/Init/Core.lean
theorem Subsingleton.helim {α β : Sort u} [h₁ : Subsingleton α] (h₂ : α = β) (a : α) (b : β) : HEq a b

Proof state:
α : Sort u
h₁ : Subsingleton α
a b : α
⊢ HEq a b

Tactic:
apply heq_of_eq

Result:
case h
α : Sort u
h₁ : Subsingleton α
a b : α
⊢ a = b

Proof state:
case h
α : Sort u
h₁ : Subsingleton α
a b : α
⊢ a = b

Tactic:
apply Subsingleton.elim

Result:
no goals

Proof state:
α β : Sort u
h₁ : Subsingleton α
h₂ : α = β
a : α
b : β
⊢ HEq a b

Tactic:
subst h₂

Result:
α : Sort u
h₁ : Subsingleton α
a b : α
⊢ HEq a b
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem Perm.sizeOf_eq_sizeOf [SizeOf α] {l₁ l₂ : List α} (h : l₁ ~ l₂) :
    sizeOf l₁ = sizeOf l₂

Proof state:
case nil
α : Type u_1
inst✝ : SizeOf α
l₁ l₂ : List α
⊢ sizeOf [] = sizeOf []

Tactic:
rfl

Result:
no goals

Proof state:
case trans
α : Type u_1
inst✝ : SizeOf α
l₁ l₂ l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
h_sz₁₂ : sizeOf l₁✝ = sizeOf l₂✝
h_sz₂₃ : sizeOf l₂✝ = sizeOf l₃✝
⊢ sizeOf l₁✝ = sizeOf l₃✝

Tactic:
simp [h_sz₁₂, h_sz₂₃]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : SizeOf α
l₁ l₂ : List α
h : l₁ ~ l₂
⊢ sizeOf l₁ = sizeOf l₂

Tactic:
induction h with
| nil => rfl
| cons _ _ h_sz₁₂ => simp [h_sz₁₂]
| swap => simp [Nat.add_left_comm]
| trans _ _ h_sz₁₂ h_sz₂₃ => simp [h_sz₁₂, h_sz₂₃]

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : SizeOf α
l₁ l₂ : List α
x✝ : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
h_sz₁₂ : sizeOf l₁✝ = sizeOf l₂✝
⊢ sizeOf (x✝ :: l₁✝) = sizeOf (x✝ :: l₂✝)

Tactic:
simp [h_sz₁₂]

Result:
no goals

Proof state:
case swap
α : Type u_1
inst✝ : SizeOf α
l₁ l₂ : List α
x✝ y✝ : α
l✝ : List α
⊢ sizeOf (y✝ :: x✝ :: l✝) = sizeOf (x✝ :: y✝ :: l✝)

Tactic:
simp [Nat.add_left_comm]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/SpecialFunctions/PosPart.lean
/-- A C⋆-algebra is spanned by nonnegative elements of norm less than `r`. -/
lemma span_nonneg_inter_ball {r : ℝ} (hr : 0 < r) :
    span ℂ ({x : A | 0 ≤ x} ∩ Metric.ball 0 r) = ⊤

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
r : ℝ
hr : 0 < r
⊢ span ℂ ({x | 0 ≤ x} ∩ Metric.ball 0 r) = ⊤

Tactic:
rw [eq_top_iff, ← span_nonneg_inter_closedBall (half_pos hr)]

Result:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
r : ℝ
hr : 0 < r
⊢ span ℂ ({x | 0 ≤ x} ∩ Metric.closedBall 0 (r / 2)) ≤ span ℂ ({x | 0 ≤ x} ∩ Metric.ball 0 r)

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
r : ℝ
hr : 0 < r
⊢ span ℂ ({x | 0 ≤ x} ∩ Metric.closedBall 0 (r / 2)) ≤ span ℂ ({x | 0 ≤ x} ∩ Metric.ball 0 r)

Tactic:
gcongr

Result:
case h.H
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
r : ℝ
hr : 0 < r
⊢ Metric.closedBall 0 (r / 2) ⊆ Metric.ball 0 r

Proof state:
case h.H
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
r : ℝ
hr : 0 < r
⊢ Metric.closedBall 0 (r / 2) ⊆ Metric.ball 0 r

Tactic:
exact Metric.closedBall_subset_ball <| half_lt_self hr

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem ordProj_pos (n p : ℕ) : 0 < ordProj[p] n

Proof state:
n p : ℕ
pp : Prime p
⊢ 0 < p ^ n.factorization p

Tactic:
simp [pow_pos pp.pos]

Result:
no goals

Proof state:
n p : ℕ
pp : ¬Prime p
⊢ 0 < p ^ n.factorization p

Tactic:
simp [pp]

Result:
no goals

Proof state:
n p : ℕ
⊢ 0 < p ^ n.factorization p

Tactic:
if pp : p.Prime then simp [pow_pos pp.pos] else simp [pp]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean
theorem darts_dropUntil_subset {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) :
    (p.dropUntil u h).darts ⊆ p.darts := fun x hx => by
  rw [← take_spec p h, darts_append, List.mem_append]
  exact Or.inr hx

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
x : G.Dart
hx : x ∈ (p.dropUntil u h).darts
⊢ x ∈ (p.takeUntil u h).darts ∨ x ∈ (p.dropUntil u h).darts

Tactic:
exact Or.inr hx

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
x : G.Dart
hx : x ∈ (p.dropUntil u h).darts
⊢ x ∈ p.darts

Tactic:
rw [← take_spec p h, darts_append, List.mem_append]

Result:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
x : G.Dart
hx : x ∈ (p.dropUntil u h).darts
⊢ x ∈ (p.takeUntil u h).darts ∨ x ∈ (p.dropUntil u h).darts
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem sub_inv_antitoneOn_Icc_left (ha : b < c) :
    AntitoneOn (fun x ↦ (x-c)⁻¹) (Set.Icc a b)

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : b < c
⊢ AntitoneOn (fun x => (x - c)⁻¹) (Set.Icc a b)

Tactic:
by_cases hab : a ≤ b

Result:
case pos
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : b < c
hab : a ≤ b
⊢ AntitoneOn (fun x => (x - c)⁻¹) (Set.Icc a b)

case neg
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : b < c
hab : ¬a ≤ b
⊢ AntitoneOn (fun x => (x - c)⁻¹) (Set.Icc a b)

Proof state:
case pos
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : b < c
hab : a ≤ b
⊢ AntitoneOn (fun x => (x - c)⁻¹) (Set.Icc a b)

Tactic:
exact sub_inv_antitoneOn_Iio.mono <| (Set.Icc_subset_Iio_iff hab).mpr ha

Result:
no goals

Proof state:
case neg
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : b < c
hab : ¬a ≤ b
⊢ AntitoneOn (fun x => (x - c)⁻¹) (Set.Icc a b)

Tactic:
simp [hab, Set.Subsingleton.antitoneOn]

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem quotDualCoannihilatorToDual_nondegenerate (W : Submodule R (Dual R M)) :
    W.quotDualCoannihilatorToDual.Nondegenerate

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R (Dual R M)
⊢ ker W.quotDualCoannihilatorToDual = ⊥ ∧ ker W.quotDualCoannihilatorToDual.flip = ⊥

Tactic:
letI : AddCommGroup W := inferInstance

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R (Dual R M)
this : AddCommGroup ↥W := inferInstance
⊢ ker W.quotDualCoannihilatorToDual = ⊥ ∧ ker W.quotDualCoannihilatorToDual.flip = ⊥

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R (Dual R M)
this : AddCommGroup ↥W := inferInstance
⊢ ker W.quotDualCoannihilatorToDual = ⊥ ∧ ker W.quotDualCoannihilatorToDual.flip = ⊥

Tactic:
simp_rw [ker_eq_bot]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R (Dual R M)
this : AddCommGroup ↥W := inferInstance
⊢ Function.Injective ⇑W.quotDualCoannihilatorToDual ∧ Function.Injective ⇑W.quotDualCoannihilatorToDual.flip

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R (Dual R M)
⊢ W.quotDualCoannihilatorToDual.Nondegenerate

Tactic:
rw [Nondegenerate, separatingLeft_iff_ker_eq_bot, separatingRight_iff_flip_ker_eq_bot]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R (Dual R M)
⊢ ker W.quotDualCoannihilatorToDual = ⊥ ∧ ker W.quotDualCoannihilatorToDual.flip = ⊥

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R (Dual R M)
this : AddCommGroup ↥W := inferInstance
⊢ Function.Injective ⇑W.quotDualCoannihilatorToDual ∧ Function.Injective ⇑W.quotDualCoannihilatorToDual.flip

Tactic:
exact ⟨W.quotDualCoannihilatorToDual_injective, W.flip_quotDualCoannihilatorToDual_injective⟩

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/FunctionsBoundedAtInfty.lean
lemma tendsto_coe_atImInfty :
    Tendsto UpperHalfPlane.coe atImInfty (comap Complex.im atTop)

Proof state:
⊢ Tendsto UpperHalfPlane.coe atImInfty (comap Complex.im atTop)

Tactic:
simpa only [atImInfty, tendsto_comap_iff, Function.comp_def,
  funext UpperHalfPlane.coe_im] using tendsto_comap

Result:
no goals