harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Quaternion.lean
theorem tsum_coe (f : α → ℝ) : (∑' a, (f a : ℍ)) = ↑(∑' a, f a)

Proof state:
case pos
α : Type u_1
f : α → ℝ
hf : Summable f
⊢ ∑' (a : α), ↑(f a) = ↑(∑' (a : α), f a)

Tactic:
exact (hasSum_coe.mpr hf.hasSum).tsum_eq

Result:
no goals

Proof state:
α : Type u_1
f : α → ℝ
⊢ ∑' (a : α), ↑(f a) = ↑(∑' (a : α), f a)

Tactic:
by_cases hf : Summable f

Result:
case pos
α : Type u_1
f : α → ℝ
hf : Summable f
⊢ ∑' (a : α), ↑(f a) = ↑(∑' (a : α), f a)

case neg
α : Type u_1
f : α → ℝ
hf : ¬Summable f
⊢ ∑' (a : α), ↑(f a) = ↑(∑' (a : α), f a)

Proof state:
case neg
α : Type u_1
f : α → ℝ
hf : ¬Summable f
⊢ ∑' (a : α), ↑(f a) = ↑(∑' (a : α), f a)

Tactic:
simp [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable (summable_coe.not.mpr hf)]

Result:
no goals
-- Mathlib/RingTheory/Localization/Defs.lean
theorem isLocalization_iff_of_base_ringEquiv (h : R ≃+* P) :
    IsLocalization M S ↔
      haveI := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
      IsLocalization (M.map h.toMonoidHom) S

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
H : IsLocalization (Submonoid.map h.toMonoidHom M) S
⊢ IsLocalization M S

Tactic:
convert isLocalization_of_base_ringEquiv (Submonoid.map (RingEquiv.toMonoidHom h) M) S h.symm

Result:
case h.e'_3
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
H : IsLocalization (Submonoid.map h.toMonoidHom M) S
⊢ M = Submonoid.map h.symm.toMonoidHom (Submonoid.map h.toMonoidHom M)

case h.e'_6
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommSemiring P
h : R ≃+* P
this : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
H : IsLocalization (Submonoid.map h.toMonoidHom M) S
⊢ inst✝¹ = ((algebraMap P S).comp h.symm.symm.toRingHom).toAlgebra
-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
lemma Set.Iic_ciInf [Nonempty ι] {f : ι → α} (hf : BddBelow (range f)) :
    Iic (⨅ i, f i) = ⋂ i, Iic (f i)

Proof state:
case h₂
α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
hf : BddBelow (range f)
x : α
hx : x ∈ ⋂ i, Iic (f i)
⊢ x ∈ Iic (⨅ i, f i)

Tactic:
apply le_ciInf

Result:
case h₂.H
α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
hf : BddBelow (range f)
x : α
hx : x ∈ ⋂ i, Iic (f i)
⊢ ∀ (x_1 : ι), x ≤ f x_1

Proof state:
case h₂.H
α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
hf : BddBelow (range f)
x : α
hx : x ∈ ⋂ i, Iic (f i)
⊢ ∀ (x_1 : ι), x ≤ f x_1

Tactic:
simpa using hx

Result:
no goals

Proof state:
case h₁
α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
hf : BddBelow (range f)
⊢ Iic (⨅ i, f i) ⊆ ⋂ i, Iic (f i)

Tactic:
rintro x hx - ⟨i, rfl⟩

Result:
case h₁.intro
α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
hf : BddBelow (range f)
x : α
hx : x ∈ Iic (⨅ i, f i)
i : ι
⊢ x ∈ (fun i => Iic (f i)) i

Proof state:
α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
hf : BddBelow (range f)
⊢ Iic (⨅ i, f i) = ⋂ i, Iic (f i)

Tactic:
apply Subset.antisymm

Result:
case h₁
α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
hf : BddBelow (range f)
⊢ Iic (⨅ i, f i) ⊆ ⋂ i, Iic (f i)

case h₂
α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
hf : BddBelow (range f)
⊢ ⋂ i, Iic (f i) ⊆ Iic (⨅ i, f i)

Proof state:
case h₁.intro
α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
hf : BddBelow (range f)
x : α
hx : x ∈ Iic (⨅ i, f i)
i : ι
⊢ x ∈ (fun i => Iic (f i)) i

Tactic:
exact hx.trans (ciInf_le hf _)

Result:
no goals

Proof state:
case h₂
α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
hf : BddBelow (range f)
⊢ ⋂ i, Iic (f i) ⊆ Iic (⨅ i, f i)

Tactic:
rintro x hx

Result:
case h₂
α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : Nonempty ι
f : ι → α
hf : BddBelow (range f)
x : α
hx : x ∈ ⋂ i, Iic (f i)
⊢ x ∈ Iic (⨅ i, f i)
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Kernels.lean
/-- The cokernel of a zero map is preserved by any functor which preserves zero morphisms. -/
lemma preservesCokernel_zero' (f : X ⟶ Y) (hf : f = 0) :
    PreservesColimit (parallelPair f 0) G

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
f : X ⟶ Y
hf : f = 0
⊢ PreservesColimit (parallelPair 0 0) G

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
f : X ⟶ Y
hf : f = 0
⊢ PreservesColimit (parallelPair f 0) G

Tactic:
rw [hf]

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
f : X ⟶ Y
hf : f = 0
⊢ PreservesColimit (parallelPair 0 0) G
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
lemma limsup_add_le (h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤) (h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥) :
    limsup (u + v) f ≤ (limsup u f) + (limsup v f)

Proof state:
case h
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤
h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > limsup v f
c : EReal
c_ab : c > a + b
x : α
a_x : u x < a
b_x : v x < b
⊢ (u + v) x < c

Tactic:
exact (add_lt_add a_x b_x).trans c_ab

Result:
no goals

Proof state:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤
h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥
⊢ limsup (u + v) f ≤ limsup u f + limsup v f

Tactic:
refine le_add_of_forall_gt h h' fun a a_u b b_v ↦ (limsup_le_iff).2 fun c c_ab ↦ ?_

Result:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤
h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > limsup v f
c : EReal
c_ab : c > a + b
⊢ ∀ᶠ (a : α) in f, (u + v) a < c

Proof state:
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤
h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > limsup v f
c : EReal
c_ab : c > a + b
⊢ ∀ᶠ (a : α) in f, (u + v) a < c

Tactic:
filter_upwards [eventually_lt_of_limsup_lt a_u, eventually_lt_of_limsup_lt b_v] with x a_x b_x

Result:
case h
α : Type u_3
f : Filter α
u v : α → EReal
h : limsup u f ≠ ⊥ ∨ limsup v f ≠ ⊤
h' : limsup u f ≠ ⊤ ∨ limsup v f ≠ ⊥
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > limsup v f
c : EReal
c_ab : c > a + b
x : α
a_x : u x < a
b_x : v x < b
⊢ (u + v) x < c
-- Mathlib/Topology/Instances/CantorSet.lean
lemma zero_mem_preCantorSet (n : ℕ) : 0 ∈ preCantorSet n

Proof state:
n : ℕ
⊢ 0 ∈ preCantorSet n

Tactic:
induction n with
| zero =>
  simp [preCantorSet]
| succ n ih =>
  exact Or.inl ⟨0, ih, by simp only [zero_div]⟩

Result:
no goals

Proof state:
case succ
n : ℕ
ih : 0 ∈ preCantorSet n
⊢ 0 ∈ preCantorSet (n + 1)

Tactic:
exact Or.inl ⟨0, ih, by simp only [zero_div]⟩

Result:
no goals

Proof state:
n : ℕ
ih : 0 ∈ preCantorSet n
⊢ (fun x => x / 3) 0 = 0

Tactic:
simp only [zero_div]

Result:
no goals

Proof state:
case zero

⊢ 0 ∈ preCantorSet 0

Tactic:
simp [preCantorSet]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Intervals.lean
theorem prod_eq_prod_Ico_succ_bot {a b : ℕ} (hab : a < b) (f : ℕ → M) :
    ∏ k ∈ Ico a b, f k = f a * ∏ k ∈ Ico (a + 1) b, f k

Proof state:
M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
hab : a < b
f : ℕ → M
⊢ a ∉ Ico (a + 1) b

Tactic:
simp

Result:
no goals

Proof state:
M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
hab : a < b
f : ℕ → M
⊢ ∏ k ∈ Ico a b, f k = f a * ∏ k ∈ Ico (a + 1) b, f k

Tactic:
have ha : a ∉ Ico (a + 1) b := by simp

Result:
M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
hab : a < b
f : ℕ → M
ha : a ∉ Ico (a + 1) b
⊢ ∏ k ∈ Ico a b, f k = f a * ∏ k ∈ Ico (a + 1) b, f k

Proof state:
M : Type u_2
inst✝ : CommMonoid M
a b : ℕ
hab : a < b
f : ℕ → M
ha : a ∉ Ico (a + 1) b
⊢ ∏ k ∈ Ico a b, f k = f a * ∏ k ∈ Ico (a + 1) b, f k

Tactic:
rw [← prod_insert ha, Nat.Ico_insert_succ_left hab]

Result:
no goals
-- Mathlib/FieldTheory/JacobsonNoether.lean
theorem exists_separable_and_not_isCentral (H : k ≠ (⊤ : Subring D)) :
    ∃ x : D, x ∉ k ∧ IsSeparable k x

Proof state:
case intro.intro.intro.intro.intro
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D) a))^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D) a))^[n] b
x✝ : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
hc : a * c = c * a
⊢ False

Tactic:
set d := c⁻¹ * a * (ad k D a)^[n - 1] b with hd_def

Result:
case intro.intro.intro.intro.intro
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D) a))^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D) a))^[n] b
x✝ : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
hc : a * c = c * a
d : D := c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hd_def : d = c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
⊢ False
-- Mathlib/Probability/Independence/Conditional.lean
lemma iCondIndepSets_iff (π : ι → Set (Set Ω)) (hπ : ∀ i s (_hs : s ∈ π i), MeasurableSet s)
    (μ : Measure Ω) [IsFiniteMeasure μ] :
    iCondIndepSets m' hm' π μ ↔ ∀ (s : Finset ι) {f : ι → Set Ω} (_H : ∀ i, i ∈ s → f i ∈ π i),
      μ⟦⋂ i ∈ s, f i | m'⟧ =ᵐ[μ] ∏ i ∈ s, (μ⟦f i | m'⟧)

Proof state:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
π : ι → Set (Set Ω)
hπ : ∀ (i : ι), ∀ s ∈ π i, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_eq' :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ i ∈ s, (fun ω => (((condExpKernel μ m') ω) (f i)).toReal) =ᶠ[ae μ] μ[(f i).indicator fun ω => 1|m']
h_eq :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ᵐ (ω : Ω) ∂μ, ∀ i ∈ s, (((condExpKernel μ m') ω) (f i)).toReal = (μ[(f i).indicator fun ω => 1|m']) ω
⊢ ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      (fun ω => (((condExpKernel μ m') ω) (⋂ i ∈ s, f i)).toReal) =ᶠ[ae μ] μ[(⋂ i ∈ s, f i).indicator fun ω => 1|m']

Tactic:
refine fun s f H ↦ condExpKernel_ae_eq_condExp hm' ?_

Result:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
π : ι → Set (Set Ω)
hπ : ∀ (i : ι), ∀ s ∈ π i, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_eq' :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ i ∈ s, (fun ω => (((condExpKernel μ m') ω) (f i)).toReal) =ᶠ[ae μ] μ[(f i).indicator fun ω => 1|m']
h_eq :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ᵐ (ω : Ω) ∂μ, ∀ i ∈ s, (((condExpKernel μ m') ω) (f i)).toReal = (μ[(f i).indicator fun ω => 1|m']) ω
s : Finset ι
f : ι → Set Ω
H : ∀ i ∈ s, f i ∈ π i
⊢ MeasurableSet (⋂ i ∈ s, f i)
-- Mathlib/AlgebraicGeometry/SpreadingOut.lean
lemma isGermInjectiveAt_iff_of_isOpenImmersion {x : X} [IsOpenImmersion f] :
    Y.IsGermInjectiveAt (f.base x) ↔ X.IsGermInjectiveAt x

Proof state:
case intro.intro.intro.intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
x : ↑↑X.toPresheafedSpace
inst✝ : IsOpenImmersion f
H✝ : Y.IsGermInjectiveAt ((ConcreteCategory.hom f.base) x)
V : ↑X.affineOpens
hU : IsAffineOpen (f ''ᵁ ↑V)
hU' : f ''ᵁ ↑V ≤ Scheme.Hom.opensRange f
hV : (IsOpenImmersion.affineOpensEquiv f) V = ⟨⟨f ''ᵁ ↑V, hU⟩, hU'⟩
y : ↑↑X.toPresheafedSpace
hy : y ∈ ↑↑V
e : (ConcreteCategory.hom f.base) y = (ConcreteCategory.hom f.base) x
H : Function.Injective ⇑(ConcreteCategory.hom (Y.presheaf.germ (f ''ᵁ ↑V) ((ConcreteCategory.hom f.base) x) ⋯))
⊢ X.IsGermInjectiveAt x

Tactic:
obtain rfl := f.isOpenEmbedding.injective e

Result:
case intro.intro.intro.intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
V : ↑X.affineOpens
hU : IsAffineOpen (f ''ᵁ ↑V)
hU' : f ''ᵁ ↑V ≤ Scheme.Hom.opensRange f
hV : (IsOpenImmersion.affineOpensEquiv f) V = ⟨⟨f ''ᵁ ↑V, hU⟩, hU'⟩
y : ↑↑X.toPresheafedSpace
hy : y ∈ ↑↑V
H✝ : Y.IsGermInjectiveAt ((ConcreteCategory.hom f.base) y)
e : (ConcreteCategory.hom f.base) y = (ConcreteCategory.hom f.base) y
H : Function.Injective ⇑(ConcreteCategory.hom (Y.presheaf.germ (f ''ᵁ ↑V) ((ConcreteCategory.hom f.base) y) ⋯))
⊢ X.IsGermInjectiveAt y

Proof state:
case intro.intro.intro.intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
V : ↑X.affineOpens
hU : IsAffineOpen (f ''ᵁ ↑V)
hU' : f ''ᵁ ↑V ≤ Scheme.Hom.opensRange f
hV : (IsOpenImmersion.affineOpensEquiv f) V = ⟨⟨f ''ᵁ ↑V, hU⟩, hU'⟩
y : ↑↑X.toPresheafedSpace
hy : y ∈ ↑↑V
H✝ : Y.IsGermInjectiveAt ((ConcreteCategory.hom f.base) y)
e : (ConcreteCategory.hom f.base) y = (ConcreteCategory.hom f.base) y
H : Function.Injective ⇑(ConcreteCategory.hom (Y.presheaf.germ (f ''ᵁ ↑V) ((ConcreteCategory.hom f.base) y) ⋯))
⊢ Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ (↑V) y hy))

Tactic:
replace H := ((MorphismProperty.injective CommRingCat).cancel_right_of_respectsIso _
  (f.stalkMap y)).mpr H

Result:
case intro.intro.intro.intro.intro.intro.intro
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
V : ↑X.affineOpens
hU : IsAffineOpen (f ''ᵁ ↑V)
hU' : f ''ᵁ ↑V ≤ Scheme.Hom.opensRange f
hV : (IsOpenImmersion.affineOpensEquiv f) V = ⟨⟨f ''ᵁ ↑V, hU⟩, hU'⟩
y : ↑↑X.toPresheafedSpace
hy : y ∈ ↑↑V
H✝ : Y.IsGermInjectiveAt ((ConcreteCategory.hom f.base) y)
e : (ConcreteCategory.hom f.base) y = (ConcreteCategory.hom f.base) y
H :
  MorphismProperty.injective CommRingCat
    (Y.presheaf.germ (f ''ᵁ ↑V) ((ConcreteCategory.hom f.base) y) ⋯ ≫ Scheme.Hom.stalkMap f y)
⊢ Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ (↑V) y hy))
-- Mathlib/MeasureTheory/Decomposition/Exhaustion.lean
/-- Auxiliary lemma for `measure_eq_top_of_subset_compl_sigmaFiniteSetWRT'`. -/
lemma measure_eq_top_of_subset_compl_sigmaFiniteSetWRT'_of_measurableSet [IsFiniteMeasure ν]
    (hs : MeasurableSet s) (hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ) (hνs : ν s ≠ 0) :
    μ s = ∞

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
hsσ : SigmaFinite (μ.restrict s)
h_lt : ν (μ.sigmaFiniteSetWRT' ν) < ν (μ.sigmaFiniteSetWRT' ν ∪ s)
⊢ ν (μ.sigmaFiniteSetWRT' ν ∪ s) ≤ ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s

Tactic:
refine (le_iSup
  (f := fun (_ : SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν ∪ s))) ↦ _) ?_).trans ?_

Result:
case refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
hsσ : SigmaFinite (μ.restrict s)
h_lt : ν (μ.sigmaFiniteSetWRT' ν) < ν (μ.sigmaFiniteSetWRT' ν ∪ s)
⊢ SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν ∪ s))

case refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
hsσ : SigmaFinite (μ.restrict s)
h_lt : ν (μ.sigmaFiniteSetWRT' ν) < ν (μ.sigmaFiniteSetWRT' ν ∪ s)
⊢ ⨆ (_ : SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν ∪ s))), ν (μ.sigmaFiniteSetWRT' ν ∪ s) ≤
    ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s
-- Mathlib/Algebra/Ring/Hom/Basic.lean
theorem codomain_trivial_iff_range_eq_singleton_zero : (0 : β) = 1 ↔ Set.range f = {0} :=
  f.codomain_trivial_iff_range_trivial.trans
    ⟨fun h =>
      Set.ext fun y => ⟨fun ⟨x, hx⟩ => by simp [← hx, h x], fun hy => ⟨0, by simpa using hy.symm⟩⟩,
      fun h x => Set.mem_singleton_iff.mp (h ▸ Set.mem_range_self x)⟩

Proof state:
α : Type u_1
β : Type u_2
x✝² : NonAssocSemiring α
x✝¹ : NonAssocSemiring β
f : α →+* β
h : ∀ (x : α), f x = 0
y : β
x✝ : y ∈ Set.range ⇑f
x : α
hx : f x = y
⊢ y ∈ {0}

Tactic:
simp [← hx, h x]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
h : ∀ (x : α), f x = 0
y : β
hy : y ∈ {0}
⊢ f 0 = y

Tactic:
simpa using hy.symm

Result:
no goals
-- Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean
@[simp]
lemma lTensor_injective_iff_injective [Module.FaithfullyFlat R M] :
    Function.Injective (f.lTensor M) ↔ Function.Injective f

Proof state:
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_4
N' : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R N
inst✝¹ : Module R N'
f : N →ₗ[R] N'
inst✝ : FaithfullyFlat R M
⊢ Function.Exact ⇑0 ⇑(LinearMap.lTensor M f) ↔ Function.Exact ⇑0 ⇑f

Tactic:
conv_rhs => rw [← lTensor_exact_iff_exact R M]

Result:
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_4
N' : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R N
inst✝¹ : Module R N'
f : N →ₗ[R] N'
inst✝ : FaithfullyFlat R M
⊢ Function.Exact ⇑0 ⇑(LinearMap.lTensor M f) ↔ Function.Exact ⇑(LinearMap.lTensor M 0) ⇑(LinearMap.lTensor M f)

Proof state:
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_4
N' : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R N
inst✝¹ : Module R N'
f : N →ₗ[R] N'
inst✝ : FaithfullyFlat R M
⊢ Function.Exact ⇑0 ⇑(LinearMap.lTensor M f) ↔ Function.Exact ⇑(LinearMap.lTensor M 0) ⇑(LinearMap.lTensor M f)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_4
N' : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R N
inst✝¹ : Module R N'
f : N →ₗ[R] N'
inst✝ : FaithfullyFlat R M
⊢ Function.Injective ⇑(LinearMap.lTensor M f) ↔ Function.Injective ⇑f

Tactic:
rw [← LinearMap.exact_zero_iff_injective (M ⊗[R] Unit), ← LinearMap.exact_zero_iff_injective Unit]

Result:
R : Type u
M : Type v
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
N : Type u_4
N' : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R N
inst✝¹ : Module R N'
f : N →ₗ[R] N'
inst✝ : FaithfullyFlat R M
⊢ Function.Exact ⇑0 ⇑(LinearMap.lTensor M f) ↔ Function.Exact ⇑0 ⇑f
-- Mathlib/Topology/Connected/TotallyDisconnected.lean
theorem totallySeparatedSpace_iff_exists_isClopen {α : Type*} [TopologicalSpace α] :
    TotallySeparatedSpace α ↔ ∀ x y : α, x ≠ y → ∃ U : Set α, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ

Proof state:
α : Type u_3
inst✝ : TopologicalSpace α
⊢ TotallySeparatedSpace α ↔ ∀ (x y : α), x ≠ y → ∃ U, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ

Tactic:
simp only [totallySeparatedSpace_iff, IsTotallySeparated, Set.Pairwise, mem_univ, true_implies]

Result:
α : Type u_3
inst✝ : TopologicalSpace α
⊢ (∀ ⦃x y : α⦄, x ≠ y → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v) ↔
    ∀ (x y : α), x ≠ y → ∃ U, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ

Proof state:
α : Type u_3
inst✝ : TopologicalSpace α
⊢ (∀ ⦃x y : α⦄, x ≠ y → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v) ↔
    ∀ (x y : α), x ≠ y → ∃ U, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ

Tactic:
refine forall₃_congr fun x y _ ↦
  ⟨fun ⟨U, V, hU, hV, Ux, Vy, f, disj⟩ ↦ ?_, fun ⟨U, hU, Ux, Ucy⟩ ↦ ?_⟩

Result:
case refine_1
α : Type u_3
inst✝ : TopologicalSpace α
x y : α
x✝¹ : x ≠ y
x✝ : ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
U V : Set α
hU : IsOpen U
hV : IsOpen V
Ux : x ∈ U
Vy : y ∈ V
f : univ ⊆ U ∪ V
disj : Disjoint U V
⊢ ∃ U, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ

case refine_2
α : Type u_3
inst✝ : TopologicalSpace α
x y : α
x✝¹ : x ≠ y
x✝ : ∃ U, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ
U : Set α
hU : IsClopen U
Ux : x ∈ U
Ucy : y ∈ Uᶜ
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

Proof state:
case refine_2
α : Type u_3
inst✝ : TopologicalSpace α
x y : α
x✝¹ : x ≠ y
x✝ : ∃ U, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ
U : Set α
hU : IsClopen U
Ux : x ∈ U
Ucy : y ∈ Uᶜ
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

Tactic:
exact ⟨U, Uᶜ, hU.2, hU.compl.2, Ux, Ucy, (Set.union_compl_self U).ge, disjoint_compl_right⟩

Result:
no goals

Proof state:
case refine_1
α : Type u_3
inst✝ : TopologicalSpace α
x y : α
x✝¹ : x ≠ y
x✝ : ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v
U V : Set α
hU : IsOpen U
hV : IsOpen V
Ux : x ∈ U
Vy : y ∈ V
f : univ ⊆ U ∪ V
disj : Disjoint U V
⊢ ∃ U, IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ

Tactic:
exact ⟨U, isClopen_of_disjoint_cover_open f hU hV disj,
  Ux, fun Uy ↦ Set.disjoint_iff.mp disj ⟨Uy, Vy⟩⟩

Result:
no goals
-- Mathlib/Algebra/Group/Defs.lean
@[to_additive (attr := simp) one_zsmul]
lemma zpow_one (a : G) : a ^ (1 : ℤ) = a

Proof state:
G : Type u_1
inst✝ : DivInvMonoid G
a : G
⊢ a ^ 1 = a

Tactic:
rw [zpow_ofNat, pow_one]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean
theorem Cospherical.affineIndependent {s : Set P} (hs : Cospherical s) {p : Fin 3 → P}
    (hps : Set.range p ⊆ s) (hpi : Function.Injective p) : AffineIndependent ℝ p

Proof state:
case intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv0 : v ≠ 0
c : P
r : ℝ
hs : ∀ p ∈ s, dist p c = r
hs' : ∀ (i : Fin 3), dist (p i) c = r
f : Fin 3 → ℝ
hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0
hf0 : f 0 = 0
hfi : Function.Injective f
hsd : ∀ (i : Fin 3), f i = 0 ∨ f i = -2 * inner v (p 0 -ᵥ c) / inner v v
hfn0 : ∀ (i : Fin 3), i ≠ 0 → f i ≠ 0
hfn0' : ∀ (i : Fin 3), i ≠ 0 → f i = -2 * inner v (p 0 -ᵥ c) / inner v v
⊢ False

Tactic:
have hf12 : f 1 = f 2 := by rw [hfn0' 1 (by decide), hfn0' 2 (by decide)]

Result:
case intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv0 : v ≠ 0
c : P
r : ℝ
hs : ∀ p ∈ s, dist p c = r
hs' : ∀ (i : Fin 3), dist (p i) c = r
f : Fin 3 → ℝ
hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0
hf0 : f 0 = 0
hfi : Function.Injective f
hsd : ∀ (i : Fin 3), f i = 0 ∨ f i = -2 * inner v (p 0 -ᵥ c) / inner v v
hfn0 : ∀ (i : Fin 3), i ≠ 0 → f i ≠ 0
hfn0' : ∀ (i : Fin 3), i ≠ 0 → f i = -2 * inner v (p 0 -ᵥ c) / inner v v
hf12 : f 1 = f 2
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem add_mul_emod_self {a b c : Int} : (a + b * c) % c = a % c :=
  if cz : c = 0 then by
    rw [cz, Int.mul_zero, Int.add_zero]
  else by
    rw [Int.emod_def, Int.emod_def, Int.add_mul_ediv_right _ _ cz, Int.add_comm _ b,
      Int.mul_add, Int.mul_comm, ← Int.sub_sub, Int.add_sub_cancel]

Proof state:
a b c : Int
cz : c = 0
⊢ (a + b * c) % c = a % c

Tactic:
rw [cz, Int.mul_zero, Int.add_zero]

Result:
no goals

Proof state:
a b c : Int
cz : ¬c = 0
⊢ (a + b * c) % c = a % c

Tactic:
rw [Int.emod_def, Int.emod_def, Int.add_mul_ediv_right _ _ cz, Int.add_comm _ b,
  Int.mul_add, Int.mul_comm, ← Int.sub_sub, Int.add_sub_cancel]

Result:
no goals