harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma mem_orbit_iff [IsGalois k K] {w w' : InfinitePlace K} :
    w' ∈ MulAction.orbit (K ≃ₐ[k] K) w ↔ w.comap (algebraMap k K) = w'.comap (algebraMap k K)

Proof state:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w w' : InfinitePlace K
⊢ w' ∈ MulAction.orbit (K ≃ₐ[k] K) w → w.comap (algebraMap k K) = w'.comap (algebraMap k K)

Tactic:
rintro ⟨σ, rfl : σ • w = w'⟩

Result:
case intro
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w : InfinitePlace K
σ : K ≃ₐ[k] K
⊢ w.comap (algebraMap k K) = (σ • w).comap (algebraMap k K)

Proof state:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w w' : InfinitePlace K
⊢ w' ∈ MulAction.orbit (K ≃ₐ[k] K) w ↔ w.comap (algebraMap k K) = w'.comap (algebraMap k K)

Tactic:
refine ⟨?_, exists_smul_eq_of_comap_eq⟩

Result:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w w' : InfinitePlace K
⊢ w' ∈ MulAction.orbit (K ≃ₐ[k] K) w → w.comap (algebraMap k K) = w'.comap (algebraMap k K)

Proof state:
case intro
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w : InfinitePlace K
σ : K ≃ₐ[k] K
⊢ mk (w.embedding.comp (algebraMap k K)) = mk ((w.embedding.comp ↑σ.symm).comp (algebraMap k K))

Tactic:
congr 1

Result:
case intro.e_φ
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w : InfinitePlace K
σ : K ≃ₐ[k] K
⊢ w.embedding.comp (algebraMap k K) = (w.embedding.comp ↑σ.symm).comp (algebraMap k K)

Proof state:
case intro.e_φ
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w : InfinitePlace K
σ : K ≃ₐ[k] K
⊢ w.embedding.comp (algebraMap k K) = (w.embedding.comp ↑σ.symm).comp (algebraMap k K)

Tactic:
ext1

Result:
case intro.e_φ.a
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w : InfinitePlace K
σ : K ≃ₐ[k] K
x✝ : k
⊢ (w.embedding.comp (algebraMap k K)) x✝ = ((w.embedding.comp ↑σ.symm).comp (algebraMap k K)) x✝

Proof state:
case intro.e_φ.a
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w : InfinitePlace K
σ : K ≃ₐ[k] K
x✝ : k
⊢ (w.embedding.comp (algebraMap k K)) x✝ = ((w.embedding.comp ↑σ.symm).comp (algebraMap k K)) x✝

Tactic:
simp

Result:
no goals

Proof state:
case intro
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w : InfinitePlace K
σ : K ≃ₐ[k] K
⊢ w.comap (algebraMap k K) = (σ • w).comap (algebraMap k K)

Tactic:
rw [← mk_embedding w, comap_mk, smul_mk, comap_mk]

Result:
case intro
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
w : InfinitePlace K
σ : K ≃ₐ[k] K
⊢ mk (w.embedding.comp (algebraMap k K)) = mk ((w.embedding.comp ↑σ.symm).comp (algebraMap k K))
-- Mathlib/Analysis/Calculus/LogDeriv.lean
theorem logDeriv_const (a : 𝕜') : logDeriv (fun _ : 𝕜 ↦ a) = 0

Proof state:
case h
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
a : 𝕜'
x✝ : 𝕜
⊢ logDeriv (fun x => a) x✝ = 0 x✝

Tactic:
simp [logDeriv_apply]

Result:
no goals

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
a : 𝕜'
⊢ (logDeriv fun x => a) = 0

Tactic:
ext

Result:
case h
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
a : 𝕜'
x✝ : 𝕜
⊢ logDeriv (fun x => a) x✝ = 0 x✝
-- Mathlib/Logic/Basic.lean
theorem not_xor (P Q : Prop) : ¬Xor' P Q ↔ (P ↔ Q)

Proof state:
P Q : Prop
⊢ ¬Xor' P Q ↔ (P ↔ Q)

Tactic:
simp only [not_and, Xor', not_or, not_not, ← iff_iff_implies_and_implies]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_rotateRightAux_of_lt {x : BitVec w} {r : Nat} {i : Nat} (hi : i < r) :
    (x.rotateRightAux r).getMsbD i = x.getMsbD (i + (w - r))

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i < r
⊢ (decide (i < w) && (!decide (i < r) && x.getMsbD (i - r)) || (x <<< (w - r)).getMsbD i) = x.getMsbD (i + (w - r))

Tactic:
simp [show i < r by omega]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i < r
⊢ (x.rotateRightAux r).getMsbD i = x.getMsbD (i + (w - r))

Tactic:
rw [rotateRightAux, getMsbD_or, getMsbD_ushiftRight]

Result:
w : Nat
x : BitVec w
r i : Nat
hi : i < r
⊢ (decide (i < w) && (!decide (i < r) && x.getMsbD (i - r)) || (x <<< (w - r)).getMsbD i) = x.getMsbD (i + (w - r))

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i < r
⊢ i < r

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem fract_eq_self {x : E} : fract b x = x ↔ x ∈ fundamentalDomain b

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
x : E
⊢ fract b x = x ↔ x ∈ fundamentalDomain b

Tactic:
simp only [Basis.ext_elem_iff b, repr_fract_apply, Int.fract_eq_self,
mem_fundamentalDomain, Set.mem_Ico]

Result:
no goals

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
x : E
⊢ fract b x = x ↔ x ∈ fundamentalDomain b

Tactic:
classical simp only [Basis.ext_elem_iff b, repr_fract_apply, Int.fract_eq_self,
  mem_fundamentalDomain, Set.mem_Ico]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem nnnorm_eq_zero_iff {f : Lp E p μ} (hp : 0 < p) : ‖f‖₊ = 0 ↔ f = 0

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ↥(Lp E p μ)
hp : 0 < p
hf : eLpNorm (↑↑f) p μ = 0 ∨ eLpNorm (↑↑f) p μ = ⊤
⊢ f = 0

Tactic:
cases hf with
| inl hf =>
  rw [eLpNorm_eq_zero_iff (Lp.aestronglyMeasurable f) hp.ne.symm] at hf
  exact Subtype.eq (AEEqFun.ext (hf.trans AEEqFun.coeFn_zero.symm))
| inr hf =>
  exact absurd hf (eLpNorm_ne_top f)

Result:
no goals

Proof state:
case inl
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ↥(Lp E p μ)
hp : 0 < p
hf : ↑↑f =ᶠ[ae μ] 0
⊢ f = 0

Tactic:
exact Subtype.eq (AEEqFun.ext (hf.trans AEEqFun.coeFn_zero.symm))

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ↥(Lp E p μ)
hp : 0 < p
hf : ‖f‖₊ = 0
⊢ f = 0

Tactic:
rw [nnnorm_def, ENNReal.toNNReal_eq_zero_iff] at hf

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ↥(Lp E p μ)
hp : 0 < p
hf : eLpNorm (↑↑f) p μ = 0 ∨ eLpNorm (↑↑f) p μ = ⊤
⊢ f = 0

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ↥(Lp E p μ)
hp : 0 < p
⊢ ‖f‖₊ = 0 ↔ f = 0

Tactic:
refine ⟨fun hf => ?_, fun hf => by simp [hf]⟩

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ↥(Lp E p μ)
hp : 0 < p
hf : ‖f‖₊ = 0
⊢ f = 0

Proof state:
case inr
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ↥(Lp E p μ)
hp : 0 < p
hf : eLpNorm (↑↑f) p μ = ⊤
⊢ f = 0

Tactic:
exact absurd hf (eLpNorm_ne_top f)

Result:
no goals

Proof state:
case inl
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ↥(Lp E p μ)
hp : 0 < p
hf : eLpNorm (↑↑f) p μ = 0
⊢ f = 0

Tactic:
rw [eLpNorm_eq_zero_iff (Lp.aestronglyMeasurable f) hp.ne.symm] at hf

Result:
case inl
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ↥(Lp E p μ)
hp : 0 < p
hf : ↑↑f =ᶠ[ae μ] 0
⊢ f = 0

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ↥(Lp E p μ)
hp : 0 < p
hf : f = 0
⊢ ‖f‖₊ = 0

Tactic:
simp [hf]

Result:
no goals
-- Mathlib/NumberTheory/DirichletCharacter/Basic.lean
lemma changeLevel_trans {m d : ℕ} (hm : n ∣ m) (hd : m ∣ d) :
    changeLevel (dvd_trans hm hd) χ = changeLevel hd (changeLevel hm χ)

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m d : ℕ
hm : n ∣ m
hd : m ∣ d
⊢ (changeLevel ⋯) χ = (changeLevel hd) ((changeLevel hm) χ)

Tactic:
simp [changeLevel_def, MonoidHom.comp_assoc, ZMod.unitsMap_comp]

Result:
no goals
-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem fourierCoeff_liftIco_eq {a : ℝ} (f : ℝ → ℂ) (n : ℤ) :
    fourierCoeff (AddCircle.liftIco T a f) n =
    fourierCoeffOn (lt_add_of_pos_right a hT.out) f n

Proof state:
case e_a
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ ∫ (t : ℝ) in Ioo a (a + T), (fourier (-n)) ↑t • liftIco T a f ↑t ∂volume =
    ∫ (x : ℝ) in Ioc a (a + T), (fourier (-n)) ↑x • f x ∂volume

Tactic:
rw [integral_Ioc_eq_integral_Ioo]

Result:
case e_a
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ ∫ (t : ℝ) in Ioo a (a + T), (fourier (-n)) ↑t • liftIco T a f ↑t ∂volume =
    ∫ (t : ℝ) in Ioo a (a + T), (fourier (-n)) ↑t • f t ∂volume

Proof state:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ (1 / T) • ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • liftIco T a f ↑x =
    (1 / T) • ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • f x

Tactic:
congr 1

Result:
case e_a
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • liftIco T a f ↑x = ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • f x

Proof state:
case e_a
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
x : ℝ
hx : x ∈ Ioo a (a + T)
⊢ (fourier (-n)) ↑x • liftIco T a f ↑x = (fourier (-n)) ↑x • f x

Tactic:
rw [liftIco_coe_apply (Ioo_subset_Ico_self hx)]

Result:
no goals

Proof state:
case e_a
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ ∫ (x : ℝ) in Ioc a (a + T), (fourier (-n)) ↑x • liftIco T a f ↑x ∂volume =
    ∫ (x : ℝ) in Ioc a (a + T), (fourier (-n)) ↑x • f x ∂volume

Tactic:
iterate 2 rw [integral_Ioc_eq_integral_Ioo]

Result:
case e_a
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ ∫ (t : ℝ) in Ioo a (a + T), (fourier (-n)) ↑t • liftIco T a f ↑t ∂volume =
    ∫ (t : ℝ) in Ioo a (a + T), (fourier (-n)) ↑t • f t ∂volume

Proof state:
case e_a
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • liftIco T a f ↑x = ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • f x

Tactic:
simp_rw [intervalIntegral.integral_of_le (lt_add_of_pos_right a hT.out).le]

Result:
case e_a
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ ∫ (x : ℝ) in Ioc a (a + T), (fourier (-n)) ↑x • liftIco T a f ↑x ∂volume =
    ∫ (x : ℝ) in Ioc a (a + T), (fourier (-n)) ↑x • f x ∂volume

Proof state:
case e_a
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ ∫ (t : ℝ) in Ioo a (a + T), (fourier (-n)) ↑t • liftIco T a f ↑t ∂volume =
    ∫ (t : ℝ) in Ioo a (a + T), (fourier (-n)) ↑t • f t ∂volume

Tactic:
refine setIntegral_congr_fun measurableSet_Ioo fun x hx => ?_

Result:
case e_a
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
x : ℝ
hx : x ∈ Ioo a (a + T)
⊢ (fourier (-n)) ↑x • liftIco T a f ↑x = (fourier (-n)) ↑x • f x

Proof state:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ fourierCoeff (liftIco T a f) n = fourierCoeffOn ⋯ f n

Tactic:
rw [fourierCoeffOn_eq_integral, fourierCoeff_eq_intervalIntegral _ _ a, add_sub_cancel_left a T]

Result:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ (1 / T) • ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • liftIco T a f ↑x =
    (1 / T) • ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • f x
-- Mathlib/Combinatorics/Digraph/Orientation.lean
@[simp]
lemma toSimpleGraphInclusive_bot : (⊥ : Digraph V).toSimpleGraphInclusive = ⊥

Proof state:
V : Type u_1
⊢ ⊥.toSimpleGraphInclusive = ⊥

Tactic:
ext

Result:
case Adj.h.h.a
V : Type u_1
x✝¹ x✝ : V
⊢ ⊥.toSimpleGraphInclusive.Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝

Proof state:
V : Type u_1
x✝² x✝¹ : V
x✝ : ⊥.toSimpleGraphInclusive.Adj x✝² x✝¹
left✝ : x✝² ≠ x✝¹
h : ⊥.Adj x✝² x✝¹ ∨ ⊥.Adj x✝¹ x✝²
⊢ ⊥.Adj x✝² x✝¹

Tactic:
tauto

Result:
no goals

Proof state:
case Adj.h.h.a
V : Type u_1
x✝¹ x✝ : V
⊢ ⊥.toSimpleGraphInclusive.Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝

Tactic:
exact ⟨fun ⟨_, h⟩ ↦ by tauto, False.elim⟩

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem ext_of_generateFrom_of_iUnion (C : Set (Set α)) (B : ℕ → Set α) (hA : ‹_› = generateFrom C)
    (hC : IsPiSystem C) (h1B : ⋃ i, B i = univ) (h2B : ∀ i, B i ∈ C) (hμB : ∀ i, μ (B i) ≠ ∞)
    (h_eq : ∀ s ∈ C, μ s = ν s) : μ = ν

Proof state:
case refine_2
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
C : Set (Set α)
B : ℕ → Set α
hA : m0 = generateFrom C
hC : IsPiSystem C
h1B : ⋃ i, B i = univ
h2B : ∀ (i : ℕ), B i ∈ C
hμB : ∀ (i : ℕ), μ (B i) ≠ ⊤
h_eq : ∀ s ∈ C, μ s = ν s
⊢ ∀ s ∈ range B, μ s ≠ ⊤

Tactic:
rintro _ ⟨i, rfl⟩

Result:
case refine_2.intro
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
C : Set (Set α)
B : ℕ → Set α
hA : m0 = generateFrom C
hC : IsPiSystem C
h1B : ⋃ i, B i = univ
h2B : ∀ (i : ℕ), B i ∈ C
hμB : ∀ (i : ℕ), μ (B i) ≠ ⊤
h_eq : ∀ s ∈ C, μ s = ν s
i : ℕ
⊢ μ (B i) ≠ ⊤

Proof state:
case refine_1
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
C : Set (Set α)
B : ℕ → Set α
hA : m0 = generateFrom C
hC : IsPiSystem C
h1B : ⋃ i, B i = univ
h2B : ∀ (i : ℕ), B i ∈ C
hμB : ∀ (i : ℕ), μ (B i) ≠ ⊤
h_eq : ∀ s ∈ C, μ s = ν s
⊢ range B ⊆ C

Tactic:
rintro _ ⟨i, rfl⟩

Result:
case refine_1.intro
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
C : Set (Set α)
B : ℕ → Set α
hA : m0 = generateFrom C
hC : IsPiSystem C
h1B : ⋃ i, B i = univ
h2B : ∀ (i : ℕ), B i ∈ C
hμB : ∀ (i : ℕ), μ (B i) ≠ ⊤
h_eq : ∀ s ∈ C, μ s = ν s
i : ℕ
⊢ B i ∈ C

Proof state:
case refine_1.intro
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
C : Set (Set α)
B : ℕ → Set α
hA : m0 = generateFrom C
hC : IsPiSystem C
h1B : ⋃ i, B i = univ
h2B : ∀ (i : ℕ), B i ∈ C
hμB : ∀ (i : ℕ), μ (B i) ≠ ⊤
h_eq : ∀ s ∈ C, μ s = ν s
i : ℕ
⊢ B i ∈ C

Tactic:
apply h2B

Result:
no goals

Proof state:
case refine_2.intro
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
C : Set (Set α)
B : ℕ → Set α
hA : m0 = generateFrom C
hC : IsPiSystem C
h1B : ⋃ i, B i = univ
h2B : ∀ (i : ℕ), B i ∈ C
hμB : ∀ (i : ℕ), μ (B i) ≠ ⊤
h_eq : ∀ s ∈ C, μ s = ν s
i : ℕ
⊢ μ (B i) ≠ ⊤

Tactic:
apply hμB

Result:
no goals

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
C : Set (Set α)
B : ℕ → Set α
hA : m0 = generateFrom C
hC : IsPiSystem C
h1B : ⋃ i, B i = univ
h2B : ∀ (i : ℕ), B i ∈ C
hμB : ∀ (i : ℕ), μ (B i) ≠ ⊤
h_eq : ∀ s ∈ C, μ s = ν s
⊢ μ = ν

Tactic:
refine ext_of_generateFrom_of_cover_subset hA hC ?_ (countable_range B) h1B ?_ h_eq

Result:
case refine_1
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
C : Set (Set α)
B : ℕ → Set α
hA : m0 = generateFrom C
hC : IsPiSystem C
h1B : ⋃ i, B i = univ
h2B : ∀ (i : ℕ), B i ∈ C
hμB : ∀ (i : ℕ), μ (B i) ≠ ⊤
h_eq : ∀ s ∈ C, μ s = ν s
⊢ range B ⊆ C

case refine_2
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
C : Set (Set α)
B : ℕ → Set α
hA : m0 = generateFrom C
hC : IsPiSystem C
h1B : ⋃ i, B i = univ
h2B : ∀ (i : ℕ), B i ∈ C
hμB : ∀ (i : ℕ), μ (B i) ≠ ⊤
h_eq : ∀ s ∈ C, μ s = ν s
⊢ ∀ s ∈ range B, μ s ≠ ⊤
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem infDist_le_dist_of_mem (h : y ∈ s) : infDist x s ≤ dist x y

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s
⊢ (infEdist x s).toReal ≤ (edist x y).toReal

Tactic:
exact ENNReal.toReal_mono (edist_ne_top _ _) (infEdist_le_edist_of_mem h)

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s
⊢ infDist x s ≤ dist x y

Tactic:
rw [dist_edist, infDist]

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
h : y ∈ s
⊢ (infEdist x s).toReal ≤ (edist x y).toReal
-- Mathlib/Probability/Kernel/Composition/CompProd.lean
lemma compProd_sum_left {ι : Type*} [Countable ι]
    {κ : ι → Kernel α β} {η : Kernel (α × β) γ} [∀ i, IsSFiniteKernel (κ i)] :
    Kernel.sum κ ⊗ₖ η = Kernel.sum (fun i ↦ (κ i) ⊗ₖ η)

Proof state:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝¹ : Countable ι
κ : ι → Kernel α β
η : Kernel (α × β) γ
inst✝ : ∀ (i : ι), IsSFiniteKernel (κ i)
hη : ¬IsSFiniteKernel η
⊢ Kernel.sum κ ⊗ₖ η = Kernel.sum fun i => κ i ⊗ₖ η

Tactic:
simp [hη]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝¹ : Countable ι
κ : ι → Kernel α β
η : Kernel (α × β) γ
inst✝ : ∀ (i : ι), IsSFiniteKernel (κ i)
⊢ Kernel.sum κ ⊗ₖ η = Kernel.sum fun i => κ i ⊗ₖ η

Tactic:
by_cases hη : IsSFiniteKernel η

Result:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝¹ : Countable ι
κ : ι → Kernel α β
η : Kernel (α × β) γ
inst✝ : ∀ (i : ι), IsSFiniteKernel (κ i)
hη : IsSFiniteKernel η
⊢ Kernel.sum κ ⊗ₖ η = Kernel.sum fun i => κ i ⊗ₖ η

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝¹ : Countable ι
κ : ι → Kernel α β
η : Kernel (α × β) γ
inst✝ : ∀ (i : ι), IsSFiniteKernel (κ i)
hη : ¬IsSFiniteKernel η
⊢ Kernel.sum κ ⊗ₖ η = Kernel.sum fun i => κ i ⊗ₖ η

Proof state:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝¹ : Countable ι
κ : ι → Kernel α β
η : Kernel (α × β) γ
inst✝ : ∀ (i : ι), IsSFiniteKernel (κ i)
hη : IsSFiniteKernel η
⊢ Kernel.sum κ ⊗ₖ η = Kernel.sum fun i => κ i ⊗ₖ η

Tactic:
ext a s hs

Result:
case pos.h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝¹ : Countable ι
κ : ι → Kernel α β
η : Kernel (α × β) γ
inst✝ : ∀ (i : ι), IsSFiniteKernel (κ i)
hη : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((Kernel.sum κ ⊗ₖ η) a) s = ((Kernel.sum fun i => κ i ⊗ₖ η) a) s

Proof state:
case pos.h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝¹ : Countable ι
κ : ι → Kernel α β
η : Kernel (α × β) γ
inst✝ : ∀ (i : ι), IsSFiniteKernel (κ i)
hη : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((Kernel.sum κ ⊗ₖ η) a) s = ((Kernel.sum fun i => κ i ⊗ₖ η) a) s

Tactic:
simp_rw [sum_apply, compProd_apply hs, sum_apply, lintegral_sum_measure, Measure.sum_apply _ hs,
compProd_apply hs]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/BigOperators.lean
theorem image_multiset_prod (f : F) :
    ∀ m : Multiset (Set α), (f : α → β) '' m.prod = (m.map fun s => f '' s).prod :=
  Quotient.ind <| by
    simpa only [Multiset.quot_mk_to_coe, Multiset.prod_coe, Multiset.map_coe] using
      image_list_prod f

Proof state:
α : Type u_2
β : Type u_3
F : Type u_4
inst✝³ : FunLike F α β
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : MonoidHomClass F α β
f : F
⊢ ∀ (a : List (Set α)), ⇑f '' Multiset.prod ⟦a⟧ = (Multiset.map (fun s => ⇑f '' s) ⟦a⟧).prod

Tactic:
simpa only [Multiset.quot_mk_to_coe, Multiset.prod_coe, Multiset.map_coe] using
  image_list_prod f

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem norm_sq_eq_of_L2 (β : ι → Type*) [∀ i, SeminormedAddCommGroup (β i)] (x : PiLp 2 β) :
    ‖x‖ ^ 2 = ∑ i : ι, ‖x i‖ ^ 2

Proof state:
ι : Type u_2
inst✝¹ : Fintype ι
β : ι → Type u_5
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ ‖x‖₊ ^ 2 = ∑ i : ι, ‖x i‖₊ ^ 2

Tactic:
rw [nnnorm_eq_of_L2, NNReal.sq_sqrt]

Result:
no goals

Proof state:
ι : Type u_2
inst✝¹ : Fintype ι
β : ι → Type u_5
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ ‖x‖ ^ 2 = ∑ i : ι, ‖x i‖ ^ 2

Tactic:
suffices ‖x‖₊ ^ 2 = ∑ i : ι, ‖x i‖₊ ^ 2 by
  simpa only [NNReal.coe_sum] using congr_arg ((↑) : ℝ≥0 → ℝ) this

Result:
ι : Type u_2
inst✝¹ : Fintype ι
β : ι → Type u_5
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ ‖x‖₊ ^ 2 = ∑ i : ι, ‖x i‖₊ ^ 2

Proof state:
ι : Type u_2
inst✝¹ : Fintype ι
β : ι → Type u_5
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
this : ‖x‖₊ ^ 2 = ∑ i : ι, ‖x i‖₊ ^ 2
⊢ ‖x‖ ^ 2 = ∑ i : ι, ‖x i‖ ^ 2

Tactic:
simpa only [NNReal.coe_sum] using congr_arg ((↑) : ℝ≥0 → ℝ) this

Result:
no goals
-- Mathlib/Data/List/Chain.lean
theorem chain'_iff_get {R} : ∀ {l : List α}, Chain' R l ↔
    ∀ (i : ℕ) (h : i < length l - 1),
      R (get l ⟨i, by omega⟩) (get l ⟨i + 1, by omega⟩)
  | [] => iff_of_true (by simp) (fun _ h => by simp at h)
  | [a] => iff_of_true (by simp) (fun _ h => by simp at h)
  | a :: b :: t => by
    rw [← and_forall_add_one, chain'_cons, chain'_iff_get]
    simp

Proof state:
α : Type u
R : α → α → Prop
x✝ : ℕ
h : x✝ < [].length - 1
⊢ R ([].get ⟨x✝, ⋯⟩) ([].get ⟨x✝ + 1, ⋯⟩)

Tactic:
simp at h

Result:
no goals

Proof state:
α : Type u
R : α → α → Prop
a : α
x✝ : ℕ
h : x✝ < [a].length - 1
⊢ R ([a].get ⟨x✝, ⋯⟩) ([a].get ⟨x✝ + 1, ⋯⟩)

Tactic:
simp at h

Result:
no goals

Proof state:
α : Type u
R : α → α → Prop
a : α
⊢ Chain' R [a]

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
R : α → α → Prop
a b : α
t : List α
⊢ Chain' R (a :: b :: t) ↔
    ∀ (i : ℕ) (h : i < (a :: b :: t).length - 1), R ((a :: b :: t).get ⟨i, ⋯⟩) ((a :: b :: t).get ⟨i + 1, ⋯⟩)

Tactic:
rw [← and_forall_add_one, chain'_cons, chain'_iff_get]

Result:
α : Type u
R : α → α → Prop
a b : α
t : List α
⊢ (R a b ∧ ∀ (i : ℕ) (h : i < (b :: t).length - 1), R ((b :: t).get ⟨i, ⋯⟩) ((b :: t).get ⟨i + 1, ⋯⟩)) ↔
    (∀ (h : 0 < (a :: b :: t).length - 1), R ((a :: b :: t).get ⟨0, ⋯⟩) ((a :: b :: t).get ⟨0 + 1, ⋯⟩)) ∧
      ∀ (n : ℕ) (h : n + 1 < (a :: b :: t).length - 1),
        R ((a :: b :: t).get ⟨n + 1, ⋯⟩) ((a :: b :: t).get ⟨n + 1 + 1, ⋯⟩)

Proof state:
α : Type u
β : Type v
R✝ r : α → α → Prop
l✝ l₁ l₂ : List α
a b : α
R : α → α → Prop
l : List α
i : ℕ
h : i < l.length - 1
⊢ i < l.length

Tactic:
omega

Result:
no goals

Proof state:
α : Type u
R : α → α → Prop
a b : α
t : List α
⊢ (R a b ∧ ∀ (i : ℕ) (h : i < (b :: t).length - 1), R ((b :: t).get ⟨i, ⋯⟩) ((b :: t).get ⟨i + 1, ⋯⟩)) ↔
    (∀ (h : 0 < (a :: b :: t).length - 1), R ((a :: b :: t).get ⟨0, ⋯⟩) ((a :: b :: t).get ⟨0 + 1, ⋯⟩)) ∧
      ∀ (n : ℕ) (h : n + 1 < (a :: b :: t).length - 1),
        R ((a :: b :: t).get ⟨n + 1, ⋯⟩) ((a :: b :: t).get ⟨n + 1 + 1, ⋯⟩)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : Type v
R✝ r : α → α → Prop
l✝ l₁ l₂ : List α
a b : α
R : α → α → Prop
l : List α
i : ℕ
h : i < l.length - 1
⊢ i + 1 < l.length

Tactic:
omega

Result:
no goals

Proof state:
α : Type u
R : α → α → Prop
⊢ Chain' R []

Tactic:
simp

Result:
no goals