harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem concat_ne_nil (a : α) (l : List α) : l ++ [a] ≠ []

Proof state:
α : Type u_1
a : α
l : List α
⊢ l ++ [a] ≠ []

Tactic:
cases l <;> simp

Result:
no goals
-- Mathlib/RingTheory/Unramified/Basic.lean
theorem localization_map [FormallyUnramified R S] :
    FormallyUnramified Rₘ Sₘ

Proof state:
R : Type u_1
S : Type u_2
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₘ
inst✝⁹ : CommRing Sₘ
M : Submonoid R
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : Algebra Rₘ Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝ : FormallyUnramified R S
⊢ FormallyUnramified Rₘ Sₘ

Tactic:
haveI : FormallyUnramified S Sₘ :=
  FormallyUnramified.of_isLocalization (M.map (algebraMap R S))

Result:
R : Type u_1
S : Type u_2
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₘ
inst✝⁹ : CommRing Sₘ
M : Submonoid R
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : Algebra Rₘ Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝ : FormallyUnramified R S
this : FormallyUnramified S Sₘ
⊢ FormallyUnramified Rₘ Sₘ

Proof state:
R : Type u_1
S : Type u_2
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₘ
inst✝⁹ : CommRing Sₘ
M : Submonoid R
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : Algebra Rₘ Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝ : FormallyUnramified R S
this : FormallyUnramified S Sₘ
⊢ FormallyUnramified Rₘ Sₘ

Tactic:
haveI : FormallyUnramified R Sₘ := FormallyUnramified.comp R S Sₘ

Result:
R : Type u_1
S : Type u_2
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₘ
inst✝⁹ : CommRing Sₘ
M : Submonoid R
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : Algebra Rₘ Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝ : FormallyUnramified R S
this✝ : FormallyUnramified S Sₘ
this : FormallyUnramified R Sₘ
⊢ FormallyUnramified Rₘ Sₘ

Proof state:
R : Type u_1
S : Type u_2
Rₘ : Type u_3
Sₘ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing Rₘ
inst✝⁹ : CommRing Sₘ
M : Submonoid R
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra R Rₘ
inst✝⁴ : Algebra Rₘ Sₘ
inst✝³ : IsScalarTower R Rₘ Sₘ
inst✝² : IsScalarTower R S Sₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ
inst✝ : FormallyUnramified R S
this✝ : FormallyUnramified S Sₘ
this : FormallyUnramified R Sₘ
⊢ FormallyUnramified Rₘ Sₘ

Tactic:
exact FormallyUnramified.localization_base M

Result:
no goals
-- Mathlib/Geometry/Manifold/PartitionOfUnity.lean
theorem exists_smooth_zero_one_of_isClosed [T2Space M] [SigmaCompactSpace M] {s t : Set M}
    (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) :
    ∃ f : C^∞⟮I, M; 𝓘(ℝ), ℝ⟯, EqOn f 0 s ∧ EqOn f 1 t ∧ ∀ x, f x ∈ Icc 0 1

Proof state:
case intro.intro
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
this : ∀ x ∈ t, sᶜ ∈ 𝓝 x
ι : Type uM
f : SmoothBumpCovering ι I M t
hf : f.IsSubordinate fun x => sᶜ
⊢ ∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : M), f x ∈ Icc 0 1

Tactic:
set g := f.toSmoothPartitionOfUnity

Result:
case intro.intro
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
this : ∀ x ∈ t, sᶜ ∈ 𝓝 x
ι : Type uM
f : SmoothBumpCovering ι I M t
hf : f.IsSubordinate fun x => sᶜ
g : SmoothPartitionOfUnity ι I M t := f.toSmoothPartitionOfUnity
⊢ ∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : M), f x ∈ Icc 0 1

Proof state:
case intro.intro
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
this : ∀ x ∈ t, sᶜ ∈ 𝓝 x
ι : Type uM
f : SmoothBumpCovering ι I M t
hf : f.IsSubordinate fun x => sᶜ
g : SmoothPartitionOfUnity ι I M t := f.toSmoothPartitionOfUnity
x : M
hx : x ∈ s
i : ι
⊢ ↑(f.toFun i) x = 0

Tactic:
exact nmem_support.1 (subset_compl_comm.1 (hf.support_subset i) hx)

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean
theorem support_dropUntil_subset {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) :
    (p.dropUntil u h).support ⊆ p.support := fun x hx => by
  rw [← take_spec p h, mem_support_append_iff]
  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 : V
hx : x ∈ (p.dropUntil u h).support
⊢ x ∈ p.support

Tactic:
rw [← take_spec p h, mem_support_append_iff]

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

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 : V
hx : x ∈ (p.dropUntil u h).support
⊢ x ∈ (p.takeUntil u h).support ∨ x ∈ (p.dropUntil u h).support

Tactic:
exact Or.inr hx

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem nil_beq_iff [BEq α] {l : List α} : ([] == l) = l.isEmpty

Proof state:
α : Type u_1
inst✝ : BEq α
l : List α
⊢ ([] == l) = l.isEmpty

Tactic:
cases l <;> rfl

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem disjoint_closedBall_closedBall_iff (hδ : 0 ≤ δ) (hε : 0 ≤ ε) :
    Disjoint (closedBall x δ) (closedBall y ε) ↔ δ + ε < dist x y

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : Disjoint (closedBall x δ) (closedBall y ε)
hxy : δ + ε ≥ dist x y
⊢ False

Tactic:
rw [add_comm] at hxy

Result:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : Disjoint (closedBall x δ) (closedBall y ε)
hxy : ε + δ ≥ dist x y
⊢ False

Proof state:
case intro.intro
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : Disjoint (closedBall x δ) (closedBall y ε)
hxy : ε + δ ≥ dist x y
z : E
hxz : dist z x ≤ δ
hzy : dist z y ≤ ε
⊢ False

Tactic:
exact h.le_bot ⟨hxz, hzy⟩

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
⊢ Disjoint (closedBall x δ) (closedBall y ε) ↔ δ + ε < dist x y

Tactic:
refine ⟨fun h => lt_of_not_ge fun hxy => ?_, closedBall_disjoint_closedBall⟩

Result:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : Disjoint (closedBall x δ) (closedBall y ε)
hxy : δ + ε ≥ dist x y
⊢ False

Proof state:
case intro.intro
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : Disjoint (closedBall x δ) (closedBall y ε)
hxy : ε + δ ≥ dist x y
z : E
hxz : dist x z ≤ δ
hzy : dist z y ≤ ε
⊢ False

Tactic:
rw [dist_comm] at hxz

Result:
case intro.intro
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : Disjoint (closedBall x δ) (closedBall y ε)
hxy : ε + δ ≥ dist x y
z : E
hxz : dist z x ≤ δ
hzy : dist z y ≤ ε
⊢ False

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : Disjoint (closedBall x δ) (closedBall y ε)
hxy : ε + δ ≥ dist x y
⊢ False

Tactic:
obtain ⟨z, hxz, hzy⟩ := exists_dist_le_le hδ hε hxy

Result:
case intro.intro
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : Disjoint (closedBall x δ) (closedBall y ε)
hxy : ε + δ ≥ dist x y
z : E
hxz : dist x z ≤ δ
hzy : dist z y ≤ ε
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem and_twoPow (x : BitVec w) (i : Nat) :
    x &&& (twoPow w i) = if x.getLsbD i then twoPow w i else 0#w

Proof state:
w : Nat
x : BitVec w
i : Nat
⊢ x &&& twoPow w i = if x.getLsbD i = true then twoPow w i else 0#w

Tactic:
ext j

Result:
case pred
w : Nat
x : BitVec w
i j : Nat
a✝ : j < w
⊢ (x &&& twoPow w i).getLsbD j = (if x.getLsbD i = true then twoPow w i else 0#w).getLsbD j

Proof state:
case pred
w : Nat
x : BitVec w
i j : Nat
a✝ : j < w
⊢ (x.getLsbD j && (decide (i < w) && decide (i = j))) = (if x.getLsbD i = true then twoPow w i else 0#w).getLsbD j

Tactic:
by_cases hj : i = j <;> by_cases hx : x.getLsbD i <;> simp_all

Result:
no goals

Proof state:
case pred
w : Nat
x : BitVec w
i j : Nat
a✝ : j < w
⊢ (x &&& twoPow w i).getLsbD j = (if x.getLsbD i = true then twoPow w i else 0#w).getLsbD j

Tactic:
simp only [getLsbD_and, getLsbD_twoPow]

Result:
case pred
w : Nat
x : BitVec w
i j : Nat
a✝ : j < w
⊢ (x.getLsbD j && (decide (i < w) && decide (i = j))) = (if x.getLsbD i = true then twoPow w i else 0#w).getLsbD j
-- Mathlib/Data/Set/Card.lean
lemma odd_card_insert_iff {a : α} (ha : a ∉ s) (hs : s.Finite

Proof state:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
hs : autoParam s.Finite _auto✝
⊢ Odd (insert a s).ncard ↔ Even s.ncard

Tactic:
rw [ncard_insert_of_not_mem ha hs, Nat.odd_add]

Result:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
hs : autoParam s.Finite _auto✝
⊢ (Odd s.ncard ↔ Even 1) ↔ Even s.ncard

Proof state:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
hs : autoParam s.Finite _auto✝
⊢ (Odd s.ncard ↔ Even 1) ↔ Even s.ncard

Tactic:
simp only [Nat.odd_add, ← Nat.not_even_iff_odd, Nat.not_even_one, iff_false, Decidable.not_not]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
theorem hexagon_reverse_inv (X Y Z : C) :
    (α_ Z X Y).hom ≫ (β_ (X ⊗ Y) Z).inv ≫ (α_ X Y Z).hom =
      (β_ X Z).inv ▷ Y ≫ (α_ X Z Y).hom ≫ X ◁ (β_ Y Z).inv

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ (α_ Z X Y).hom ≫ (β_ (X ⊗ Y) Z).inv ≫ (α_ X Y Z).hom = (β_ X Z).inv ▷ Y ≫ (α_ X Z Y).hom ≫ X ◁ (β_ Y Z).inv

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Basic.lean
theorem pretransitive_iff_subsingleton_quotient :
    IsPretransitive G α ↔ Subsingleton (orbitRel.Quotient G α)

Proof state:
case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : Subsingleton (orbitRel.Quotient G α)
a b : α
h : ⟦b⟧ = ⟦a⟧
⊢ ∃ g, g • a = b

Tactic:
exact Quotient.eq''.mp h

Result:
no goals

Proof state:
case refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : IsPretransitive G α
a b : orbitRel.Quotient G α
x : α
⊢ Quot.mk (⇑(orbitRel G α)) x = b

Tactic:
exact Quot.inductionOn b (fun y ↦ Quot.sound <| exists_smul_eq G y x)

Result:
no goals

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
⊢ IsPretransitive G α ↔ Subsingleton (orbitRel.Quotient G α)

Tactic:
refine ⟨fun _ ↦ ⟨fun a b ↦ ?_⟩, fun _ ↦ ⟨fun a b ↦ ?_⟩⟩

Result:
case refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : IsPretransitive G α
a b : orbitRel.Quotient G α
⊢ a = b

case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : Subsingleton (orbitRel.Quotient G α)
a b : α
⊢ ∃ g, g • a = b

Proof state:
case refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : IsPretransitive G α
a b : orbitRel.Quotient G α
⊢ a = b

Tactic:
refine Quot.inductionOn a (fun x ↦ ?_)

Result:
case refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : IsPretransitive G α
a b : orbitRel.Quotient G α
x : α
⊢ Quot.mk (⇑(orbitRel G α)) x = b

Proof state:
case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : Subsingleton (orbitRel.Quotient G α)
a b : α
⊢ ∃ g, g • a = b

Tactic:
have h : Quotient.mk (orbitRel G α) b = ⟦a⟧ := Subsingleton.elim _ _

Result:
case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : Subsingleton (orbitRel.Quotient G α)
a b : α
h : ⟦b⟧ = ⟦a⟧
⊢ ∃ g, g • a = b
-- Mathlib/Topology/MetricSpace/Dilation.lean
theorem ratio_mul (f g : α →ᵈ α) : ratio (f * g) = ratio f * ratio g

Proof state:
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
f g : α →ᵈ α
h : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ ratio (f * g) = ratio f * ratio g

Tactic:
push_neg at h

Result:
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
f g : α →ᵈ α
h : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ⊤
⊢ ratio (f * g) = ratio f * ratio g

Proof state:
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
f g : α →ᵈ α
h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ ratio (f * g) = ratio f * ratio g

Tactic:
simp [ratio_of_trivial, h]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f g : α →ᵈ α
⊢ ratio (f * g) = ratio f * ratio g

Tactic:
by_cases h : ∀ x y : α, edist x y = 0 ∨ edist x y = ∞

Result:
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
f g : α →ᵈ α
h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ ratio (f * g) = ratio f * ratio g

case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
f g : α →ᵈ α
h : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ ratio (f * g) = ratio f * ratio g

Proof state:
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
f g : α →ᵈ α
h : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ⊤
⊢ ratio (f * g) = ratio f * ratio g

Tactic:
exact ratio_comp' h

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extend_image_nhd_mem_nhds_of_boundaryless [I.Boundaryless] {x} (hx : x ∈ f.source)
    {s : Set M} (h : s ∈ 𝓝 x) : (f.extend I) '' s ∈ 𝓝 ((f.extend I) x)

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
inst✝ : I.Boundaryless
x : M
hx : x ∈ f.source
s : Set M
h : s ∈ 𝓝 x
⊢ ↑(f.extend I) ⁻¹' (↑(f.extend I) '' s) ∈ 𝓝 x

Tactic:
filter_upwards [h] using subset_preimage_image (f.extend I) s

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
inst✝ : I.Boundaryless
x : M
hx : x ∈ f.source
s : Set M
h : s ∈ 𝓝 x
⊢ ↑(f.extend I) '' s ∈ 𝓝 (↑(f.extend I) x)

Tactic:
rw [← f.map_extend_nhds_of_boundaryless hx, Filter.mem_map]

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
inst✝ : I.Boundaryless
x : M
hx : x ∈ f.source
s : Set M
h : s ∈ 𝓝 x
⊢ ↑(f.extend I) ⁻¹' (↑(f.extend I) '' s) ∈ 𝓝 x
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem iSup₂_lintegral_le {ι : Sort*} {ι' : ι → Sort*} (f : ∀ i, ι' i → α → ℝ≥0∞) :
    ⨆ (i) (j), ∫⁻ a, f i j a ∂μ ≤ ∫⁻ a, ⨆ (i) (j), f i j a ∂μ

Proof state:
case h.e'_4.h.e'_4.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_5
ι' : ι → Sort u_6
f : (i : ι) → ι' i → α → ℝ≥0∞
a : α
⊢ ⨆ i, ⨆ j, f i j a = (⨆ i, ⨆ j, f i j) a

Tactic:
simp only [iSup_apply]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_5
ι' : ι → Sort u_6
f : (i : ι) → ι' i → α → ℝ≥0∞
⊢ ⨆ i, ⨆ j, ∫⁻ (a : α), f i j a ∂μ ≤ ∫⁻ (a : α), ⨆ i, ⨆ j, f i j a ∂μ

Tactic:
convert (monotone_lintegral μ).le_map_iSup₂ f with a

Result:
case h.e'_4.h.e'_4.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_5
ι' : ι → Sort u_6
f : (i : ι) → ι' i → α → ℝ≥0∞
a : α
⊢ ⨆ i, ⨆ j, f i j a = (⨆ i, ⨆ j, f i j) a
-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
theorem measure_univ {l u : ℝ} (hfl : Tendsto f atBot (𝓝 l)) (hfu : Tendsto f atTop (𝓝 u)) :
    f.measure univ = ofReal (u - l)

Proof state:
f : StieltjesFunction
l u : ℝ
hfl : Tendsto (↑f) atBot (𝓝 l)
hfu : Tendsto (↑f) atTop (𝓝 u)
⊢ Tendsto (fun x => ofReal (↑f x - l)) atTop (𝓝 (ofReal (u - l)))

Tactic:
exact ENNReal.tendsto_ofReal (Tendsto.sub_const hfu _)

Result:
no goals

Proof state:
f : StieltjesFunction
l u : ℝ
hfl : Tendsto (↑f) atBot (𝓝 l)
hfu : Tendsto (↑f) atTop (𝓝 u)
⊢ Tendsto (fun x => f.measure (Iic x)) atTop (𝓝 (ofReal (u - l)))

Tactic:
simp_rw [measure_Iic f hfl]

Result:
f : StieltjesFunction
l u : ℝ
hfl : Tendsto (↑f) atBot (𝓝 l)
hfu : Tendsto (↑f) atTop (𝓝 u)
⊢ Tendsto (fun x => ofReal (↑f x - l)) atTop (𝓝 (ofReal (u - l)))

Proof state:
f : StieltjesFunction
l u : ℝ
hfl : Tendsto (↑f) atBot (𝓝 l)
hfu : Tendsto (↑f) atTop (𝓝 u)
⊢ f.measure univ = ofReal (u - l)

Tactic:
refine tendsto_nhds_unique (tendsto_measure_Iic_atTop _) ?_

Result:
f : StieltjesFunction
l u : ℝ
hfl : Tendsto (↑f) atBot (𝓝 l)
hfu : Tendsto (↑f) atTop (𝓝 u)
⊢ Tendsto (fun x => f.measure (Iic x)) atTop (𝓝 (ofReal (u - l)))
-- Mathlib/Topology/MetricSpace/Gluing.lean
theorem one_le_dist_of_ne {i j : ι} (h : i ≠ j) (x : E i) (y : E j) :
    1 ≤ dist (⟨i, x⟩ : Σk, E k) ⟨j, y⟩

Proof state:
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i j : ι
h : i ≠ j
x : E i
y : E j
⊢ 1 ≤ dist x ⋯.some + 1 + dist ⋯.some y

Tactic:
linarith [@dist_nonneg _ _ x (Nonempty.some ⟨x⟩), @dist_nonneg _ _ (Nonempty.some ⟨y⟩) y]

Result:
no goals

Proof state:
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i j : ι
h : i ≠ j
x : E i
y : E j
⊢ 1 ≤ dist ⟨i, x⟩ ⟨j, y⟩

Tactic:
rw [Sigma.dist_ne h x y]

Result:
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i j : ι
h : i ≠ j
x : E i
y : E j
⊢ 1 ≤ dist x ⋯.some + 1 + dist ⋯.some y
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem angle_pos_of_angle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = π / 2)
    (h0 : p₁ ≠ p₂ ∨ p₃ = p₂) : 0 < ∠ p₂ p₃ p₁

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ = 0 ∨ p₁ -ᵥ p₂ ≠ 0
⊢ 0 < InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂))

Tactic:
exact angle_add_pos_of_inner_eq_zero h h0

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ = 0 ∨ p₁ -ᵥ p₂ ≠ 0
⊢ 0 < ∠ p₂ p₃ p₁

Tactic:
rw [angle, ← vsub_add_vsub_cancel p₁ p₂ p₃, add_comm]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ = 0 ∨ p₁ -ᵥ p₂ ≠ 0
⊢ 0 < InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂))

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₁ ≠ p₂ ∨ p₃ = p₂
⊢ 0 < ∠ p₂ p₃ p₁

Tactic:
rw [← @vsub_ne_zero V, eq_comm, ← @vsub_eq_zero_iff_eq V, or_comm] at h0

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ = 0 ∨ p₁ -ᵥ p₂ ≠ 0
⊢ 0 < ∠ p₂ p₃ p₁

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
h0 : p₁ ≠ p₂ ∨ p₃ = p₂
⊢ 0 < ∠ p₂ p₃ p₁

Tactic:
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ←
  inner_neg_left, neg_vsub_eq_vsub_rev] at h

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₁ ≠ p₂ ∨ p₃ = p₂
⊢ 0 < ∠ p₂ p₃ p₁
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem Bool.not_true  : (!true) = false

Proof state:
⊢ (!true) = false

Tactic:
decide

Result:
no goals
-- Mathlib/RingTheory/Polynomial/ScaleRoots.lean
lemma scaleRoots_dvd_iff (p q : R[X]) {r : R} (hr : IsUnit r) :
    p.scaleRoots r ∣ q.scaleRoots r ↔ p ∣ q

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
⊢ (p.scaleRoots r).scaleRoots ↑hr.unit⁻¹ ∣ (q.scaleRoots r).scaleRoots ↑hr.unit⁻¹ → p ∣ q

Tactic:
simp [← scaleRoots_mul, scaleRoots_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
⊢ p.scaleRoots r ∣ q.scaleRoots r ↔ p ∣ q

Tactic:
refine ⟨?_ ∘ scaleRoots_dvd' _ _ (hr.unit⁻¹).isUnit, scaleRoots_dvd' p q hr⟩

Result:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
hr : IsUnit r
⊢ (p.scaleRoots r).scaleRoots ↑hr.unit⁻¹ ∣ (q.scaleRoots r).scaleRoots ↑hr.unit⁻¹ → p ∣ q
-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem out_mul (a b : Associates α) : (a * b).out = a.out * b.out :=
  Quotient.inductionOn₂ a b fun _ _ => by
    simp only [Associates.quotient_mk_eq_mk, out_mk, mk_mul_mk, normalize.map_mul]

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a b : Associates α
x✝¹ x✝ : α
⊢ (⟦x✝¹⟧ * ⟦x✝⟧).out = Associates.out ⟦x✝¹⟧ * Associates.out ⟦x✝⟧

Tactic:
simp only [Associates.quotient_mk_eq_mk, out_mk, mk_mul_mk, normalize.map_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mem_of_getElem {l : Vector α n} {i : Nat} {h} {a : α} (e : l[i] = a) : a ∈ l

Proof state:
α : Type u_1
n : Nat
l : Vector α n
i : Nat
h : i < n
⊢ l[i] ∈ l

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : Vector α n
i : Nat
h : i < n
a : α
e : l[i] = a
⊢ a ∈ l

Tactic:
subst e

Result:
α : Type u_1
n : Nat
l : Vector α n
i : Nat
h : i < n
⊢ l[i] ∈ l
-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
@[simp]
protected lemma map_one [MonoidWithZero R] [MonoidWithZero S] (f : R →*₀ S) :
    (1 : HahnSeries Γ R).map f = (1 : HahnSeries Γ S)

Proof state:
case coeff.h
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝³ : Zero Γ
inst✝² : PartialOrder Γ
inst✝¹ : MonoidWithZero R
inst✝ : MonoidWithZero S
f : R →*₀ S
g : Γ
⊢ (map 1 f).coeff g = coeff 1 g

Tactic:
by_cases h : g = 0 <;> simp [h]

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝³ : Zero Γ
inst✝² : PartialOrder Γ
inst✝¹ : MonoidWithZero R
inst✝ : MonoidWithZero S
f : R →*₀ S
⊢ map 1 f = 1

Tactic:
ext g

Result:
case coeff.h
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝³ : Zero Γ
inst✝² : PartialOrder Γ
inst✝¹ : MonoidWithZero R
inst✝ : MonoidWithZero S
f : R →*₀ S
g : Γ
⊢ (map 1 f).coeff g = coeff 1 g
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma coe_inv_map_Δ' : (W.map φ).Δ'⁻¹ = φ ↑W.Δ'⁻¹

Proof state:
R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ ↑(W.map φ).Δ'⁻¹ = φ ↑W.Δ'⁻¹

Tactic:
simp

Result:
no goals