harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Convex/Topology.lean
theorem JoinedIn.of_segment_subset {E : Type*} [AddCommGroup E] [Module ℝ E]
    [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E]
    {x y : E} {s : Set E} (h : [x -[ℝ] y] ⊆ s) : JoinedIn s x y

Proof state:
E : Type u_4
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
x y : E
s : Set E
h : [x-[ℝ]y] ⊆ s
A : Continuous fun t => (1 - t) • x + t • y
⊢ (1 - 0) • x + 0 • y = x

Tactic:
simp

Result:
no goals

Proof state:
E : Type u_4
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
x y : E
s : Set E
h : [x-[ℝ]y] ⊆ s
A : Continuous fun t => (1 - t) • x + t • y
⊢ (1 - 1) • x + 1 • y = y

Tactic:
simp

Result:
no goals

Proof state:
E : Type u_4
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
x y : E
s : Set E
h : [x-[ℝ]y] ⊆ s
A : Continuous fun t => (1 - t) • x + t • y
⊢ JoinedIn s x y

Tactic:
apply JoinedIn.ofLine A.continuousOn (by simp) (by simp)

Result:
E : Type u_4
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
x y : E
s : Set E
h : [x-[ℝ]y] ⊆ s
A : Continuous fun t => (1 - t) • x + t • y
⊢ (fun t => (1 - t) • x + t • y) '' unitInterval ⊆ s

Proof state:
E : Type u_4
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
x y : E
s : Set E
h : [x-[ℝ]y] ⊆ s
⊢ JoinedIn s x y

Tactic:
have A : Continuous (fun t ↦ (1 - t) • x + t • y : ℝ → E) := by fun_prop

Result:
E : Type u_4
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
x y : E
s : Set E
h : [x-[ℝ]y] ⊆ s
A : Continuous fun t => (1 - t) • x + t • y
⊢ JoinedIn s x y

Proof state:
E : Type u_4
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
x y : E
s : Set E
h : [x-[ℝ]y] ⊆ s
⊢ Continuous fun t => (1 - t) • x + t • y

Tactic:
fun_prop

Result:
no goals

Proof state:
case h.e'_3
E : Type u_4
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
x y : E
s : Set E
h : [x-[ℝ]y] ⊆ s
A : Continuous fun t => (1 - t) • x + t • y
⊢ (fun t => (1 - t) • x + t • y) '' unitInterval = [x-[ℝ]y]

Tactic:
rw [segment_eq_image ℝ x y]

Result:
no goals

Proof state:
E : Type u_4
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
x y : E
s : Set E
h : [x-[ℝ]y] ⊆ s
A : Continuous fun t => (1 - t) • x + t • y
⊢ (fun t => (1 - t) • x + t • y) '' unitInterval ⊆ s

Tactic:
convert h

Result:
case h.e'_3
E : Type u_4
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul ℝ E
x y : E
s : Set E
h : [x-[ℝ]y] ⊆ s
A : Continuous fun t => (1 - t) • x + t • y
⊢ (fun t => (1 - t) • x + t • y) '' unitInterval = [x-[ℝ]y]
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem indicator_ae_eq_of_restrict_compl_ae_eq_zero (hs : MeasurableSet s)
    (hf : f =ᵐ[μ.restrict sᶜ] 0) : s.indicator f =ᵐ[μ] f

Proof state:
case h
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → f x = 0 x
x : α
hx : x ∈ sᶜ → f x = 0 x
⊢ s.indicator f x = f x

Tactic:
by_cases hxs : x ∈ s

Result:
case pos
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → f x = 0 x
x : α
hx : x ∈ sᶜ → f x = 0 x
hxs : x ∈ s
⊢ s.indicator f x = f x

case neg
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → f x = 0 x
x : α
hx : x ∈ sᶜ → f x = 0 x
hxs : x ∉ s
⊢ s.indicator f x = f x

Proof state:
case pos
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → f x = 0 x
x : α
hx : x ∈ sᶜ → f x = 0 x
hxs : x ∈ s
⊢ s.indicator f x = f x

Tactic:
simp only [hxs, Set.indicator_of_mem]

Result:
no goals

Proof state:
case neg
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → f x = 0 x
x : α
hx : x ∈ sᶜ → f x = 0 x
hxs : x ∉ s
⊢ s.indicator f x = f x

Tactic:
simp only [hx hxs, Pi.zero_apply, Set.indicator_apply_eq_zero, eq_self_iff_true, imp_true_iff]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict sᶜ)] 0
⊢ s.indicator f =ᶠ[ae μ] f

Tactic:
rw [Filter.EventuallyEq, ae_restrict_iff' hs.compl] at hf

Result:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → f x = 0 x
⊢ s.indicator f =ᶠ[ae μ] f

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → f x = 0 x
⊢ s.indicator f =ᶠ[ae μ] f

Tactic:
filter_upwards [hf] with x hx

Result:
case h
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → f x = 0 x
x : α
hx : x ∈ sᶜ → f x = 0 x
⊢ s.indicator f x = f x
-- Mathlib/RingTheory/ReesAlgebra.lean
theorem reesAlgebra.monomial_mem {I : Ideal R} {i : ℕ} {r : R} :
    monomial i r ∈ reesAlgebra I ↔ r ∈ I ^ i

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
i : ℕ
r : R
⊢ (monomial i) r ∈ reesAlgebra I ↔ r ∈ I ^ i

Tactic:
simp +contextual [mem_reesAlgebra_iff_support, coeff_monomial, ←
  imp_iff_not_or]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
lemma isSFiniteKernel_prodMkLeft_unit {κ : Kernel α β} :
    IsSFiniteKernel (prodMkLeft Unit κ) ↔ IsSFiniteKernel κ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
x✝ : IsSFiniteKernel (prodMkLeft Unit κ)
⊢ Measurable fun a => ((), a)

Tactic:
fun_prop

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
x✝ : IsSFiniteKernel (prodMkLeft Unit κ)
⊢ IsSFiniteKernel κ

Tactic:
change IsSFiniteKernel ((prodMkLeft Unit κ).comap (fun a ↦ ((), a)) (by fun_prop))

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
x✝ : IsSFiniteKernel (prodMkLeft Unit κ)
⊢ IsSFiniteKernel ((prodMkLeft Unit κ).comap (fun a => ((), a)) ⋯)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ IsSFiniteKernel (prodMkLeft Unit κ) ↔ IsSFiniteKernel κ

Tactic:
refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
x✝ : IsSFiniteKernel (prodMkLeft Unit κ)
⊢ IsSFiniteKernel κ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
x✝ : IsSFiniteKernel (prodMkLeft Unit κ)
⊢ IsSFiniteKernel ((prodMkLeft Unit κ).comap (fun a => ((), a)) ⋯)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem Indep.isBasis_of_maximal_subset (hI : M.Indep I) (hIX : I ⊆ X)
    (hmax : ∀ ⦃J⦄, M.Indep J → I ⊆ J → J ⊆ X → J ⊆ I) (hX : X ⊆ M.E

Proof state:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
hmax : ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → J ⊆ I
hX : autoParam (X ⊆ M.E) _auto✝
⊢ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J

Tactic:
exact fun J hJ hIJ hJX ↦ hIJ.antisymm (hmax hJ hIJ hJX)

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
hmax : ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → J ⊆ I
hX : autoParam (X ⊆ M.E) _auto✝
⊢ X ⊆ M.E

Tactic:
aesop_mat

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
hmax : ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → J ⊆ I
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.IsBasis I X

Tactic:
rw [isBasis_iff (by aesop_mat : X ⊆ M.E), and_iff_right hI, and_iff_right hIX]

Result:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
hmax : ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → J ⊆ I
hX : autoParam (X ⊆ M.E) _auto✝
⊢ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J
-- Mathlib/NumberTheory/NumberField/House.lean
theorem house_eq_sup' (α : K) :
    house α = univ.sup' univ_nonempty (fun φ : K →+* ℂ ↦ ‖φ α‖₊)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
⊢ house α = ↑(univ.sup' ⋯ fun φ => ‖φ α‖₊)

Tactic:
rw [house, ← coe_nnnorm, nnnorm_eq, ← sup'_eq_sup univ_nonempty]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem norm_ne_zero_iff {x : mixedSpace K} :
    mixedEmbedding.norm x ≠ 0 ↔ ∀ w, normAtPlace w x ≠ 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ ¬mixedEmbedding.norm x ≠ 0 ↔ ¬∀ (w : InfinitePlace K), (normAtPlace w) x ≠ 0

Tactic:
simp_rw [ne_eq, mixedEmbedding.norm_eq_zero_iff, not_not, not_forall, not_not]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ mixedEmbedding.norm x ≠ 0 ↔ ∀ (w : InfinitePlace K), (normAtPlace w) x ≠ 0

Tactic:
rw [← not_iff_not]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ ¬mixedEmbedding.norm x ≠ 0 ↔ ¬∀ (w : InfinitePlace K), (normAtPlace w) x ≠ 0
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem cyclotomic.eval_apply {R S : Type*} (q : R) (n : ℕ) [Ring R] [Ring S] (f : R →+* S) :
    eval (f q) (cyclotomic n S) = f (eval q (cyclotomic n R))

Proof state:
R : Type u_1
S : Type u_2
q : R
n : ℕ
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
⊢ eval (f q) (cyclotomic n S) = f (eval q (cyclotomic n R))

Tactic:
rw [← map_cyclotomic n f, eval_map, eval₂_at_apply]

Result:
no goals
-- Mathlib/GroupTheory/Nilpotent.lean
theorem upperCentralSeries.map {H : Type*} [Group H] {f : G →* H} (h : Function.Surjective f)
    (n : ℕ) : Subgroup.map f (upperCentralSeries G n) ≤ upperCentralSeries H n

Proof state:
case zero
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
h : Function.Surjective ⇑f
⊢ Subgroup.map f (upperCentralSeries G 0) ≤ upperCentralSeries H 0

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
h : Function.Surjective ⇑f
n : ℕ
⊢ Subgroup.map f (upperCentralSeries G n) ≤ upperCentralSeries H n

Tactic:
induction' n with d hd

Result:
case zero
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
h : Function.Surjective ⇑f
⊢ Subgroup.map f (upperCentralSeries G 0) ≤ upperCentralSeries H 0

case succ
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
h : Function.Surjective ⇑f
d : ℕ
hd : Subgroup.map f (upperCentralSeries G d) ≤ upperCentralSeries H d
⊢ Subgroup.map f (upperCentralSeries G (d + 1)) ≤ upperCentralSeries H (d + 1)

Proof state:
case succ.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
h : Function.Surjective ⇑f
d : ℕ
hd : Subgroup.map f (upperCentralSeries G d) ≤ upperCentralSeries H d
x : G
hx : x ∈ upperCentralSeries G d.succ
y : G
⊢ f x * f y * (f x)⁻¹ * (f y)⁻¹ ∈ (upperCentralSeriesAux H d).fst

Tactic:
simpa using hd (mem_map_of_mem f (hx y))

Result:
no goals

Proof state:
case succ
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
h : Function.Surjective ⇑f
d : ℕ
hd : Subgroup.map f (upperCentralSeries G d) ≤ upperCentralSeries H d
⊢ Subgroup.map f (upperCentralSeries G (d + 1)) ≤ upperCentralSeries H (d + 1)

Tactic:
rintro _ ⟨x, hx : x ∈ upperCentralSeries G d.succ, rfl⟩ y'

Result:
case succ.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
h : Function.Surjective ⇑f
d : ℕ
hd : Subgroup.map f (upperCentralSeries G d) ≤ upperCentralSeries H d
x : G
hx : x ∈ upperCentralSeries G d.succ
y' : H
⊢ f x * y' * (f x)⁻¹ * y'⁻¹ ∈ (upperCentralSeriesAux H d).fst

Proof state:
case succ.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
h : Function.Surjective ⇑f
d : ℕ
hd : Subgroup.map f (upperCentralSeries G d) ≤ upperCentralSeries H d
x : G
hx : x ∈ upperCentralSeries G d.succ
y' : H
⊢ f x * y' * (f x)⁻¹ * y'⁻¹ ∈ (upperCentralSeriesAux H d).fst

Tactic:
rcases h y' with ⟨y, rfl⟩

Result:
case succ.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
h : Function.Surjective ⇑f
d : ℕ
hd : Subgroup.map f (upperCentralSeries G d) ≤ upperCentralSeries H d
x : G
hx : x ∈ upperCentralSeries G d.succ
y : G
⊢ f x * f y * (f x)⁻¹ * (f y)⁻¹ ∈ (upperCentralSeriesAux H d).fst
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get_alter_self [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)}
    (h : m.WF) {hc : k ∈ m.alter k f} :
    haveI h' : (f (m.get? k)).isSome := mem_alter_self h |>.mp hc
    (m.alter k f).get k hc = (f (m.get? k)).get h'

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
hc : k ∈ m.alter k f
⊢ (m.alter k f).contains k = true → (m.alter k f).get k hc = (f (m.get? k)).get ⋯

Tactic:
simp_to_raw using Raw₀.get_alter_self

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
hc : k ∈ m.alter k f
⊢ (m.alter k f).get k hc = (f (m.get? k)).get ⋯

Tactic:
simp only [mem_iff_contains] at hc

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
hc✝ : k ∈ m.alter k f
hc : (m.alter k f).contains k = true
⊢ (m.alter k f).get k hc✝ = (f (m.get? k)).get ⋯

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
hc✝ : k ∈ m.alter k f
hc : (m.alter k f).contains k = true
⊢ (m.alter k f).get k hc✝ = (f (m.get? k)).get ⋯

Tactic:
revert hc

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
hc : k ∈ m.alter k f
⊢ (m.alter k f).contains k = true → (m.alter k f).get k hc = (f (m.get? k)).get ⋯
-- Mathlib/Algebra/BigOperators/Associated.lean
theorem prod_eq_one_iff {p : Multiset (Associates α)} :
    p.prod = 1 ↔ ∀ a ∈ p, (a : Associates α) = 1 :=
  Multiset.induction_on p (by simp)
    (by simp +contextual [mul_eq_one, or_imp, forall_and])

Proof state:
α : Type u_1
inst✝ : CommMonoid α
p : Multiset (Associates α)
⊢ Multiset.prod 0 = 1 ↔ ∀ a ∈ 0, a = 1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommMonoid α
p : Multiset (Associates α)
⊢ ∀ (a : Associates α) (s : Multiset (Associates α)),
    (s.prod = 1 ↔ ∀ a ∈ s, a = 1) → ((a ::ₘ s).prod = 1 ↔ ∀ a_2 ∈ a ::ₘ s, a_2 = 1)

Tactic:
simp +contextual [mul_eq_one, or_imp, forall_and]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast?_insertEntry_self [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α}
    {v : β k} : getValueCast? k (insertEntry k v l) = some v

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k : α
v : β k
⊢ getValueCast? k (insertEntry k v l) = some v

Tactic:
rw [getValueCast?_insertEntry, dif_pos BEq.refl, cast_eq]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Triangle.lean
theorem sin_angle_add_angle_sub_add_angle_sub_eq_zero {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
    Real.sin (angle x y + angle x (x - y) + angle y (y - x)) = 0

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ Real.sin (angle x y) * -Real.cos (angle x y) + Real.cos (angle x y) * Real.sin (angle x y) = 0

Tactic:
ring

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ Real.sin (angle x y + angle x (x - y) + angle y (y - x)) = 0

Tactic:
rw [add_assoc, Real.sin_add, cos_angle_sub_add_angle_sub_rev_eq_neg_cos_angle hx hy,
  sin_angle_sub_add_angle_sub_rev_eq_sin_angle hx hy]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ Real.sin (angle x y) * -Real.cos (angle x y) + Real.cos (angle x y) * Real.sin (angle x y) = 0
-- Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean
theorem contractLeft_contractLeft (x : CliffordAlgebra Q) : d⌋(d⌋x) = 0

Proof state:
case ι_mul
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
x✝ : CliffordAlgebra Q
m✝ : M
hx : (contractLeft d) ((contractLeft d) x✝) = 0
⊢ (contractLeft d) ((contractLeft d) ((ι Q) m✝ * x✝)) = 0

Tactic:
rw [contractLeft_ι_mul, map_sub, contractLeft_ι_mul, hx, LinearMap.map_smul,
  mul_zero, sub_zero, sub_self]

Result:
no goals

Proof state:
case add
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
x✝ y✝ : CliffordAlgebra Q
hx : (contractLeft d) ((contractLeft d) x✝) = 0
hy : (contractLeft d) ((contractLeft d) y✝) = 0
⊢ (contractLeft d) ((contractLeft d) (x✝ + y✝)) = 0

Tactic:
rw [map_add, map_add, hx, hy, add_zero]

Result:
no goals

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
x : CliffordAlgebra Q
⊢ (contractLeft d) ((contractLeft d) x) = 0

Tactic:
induction x using CliffordAlgebra.left_induction with
| algebraMap => simp_rw [contractLeft_algebraMap, map_zero]
| add _ _ hx hy => rw [map_add, map_add, hx, hy, add_zero]
| ι_mul _ _ hx =>
  rw [contractLeft_ι_mul, map_sub, contractLeft_ι_mul, hx, LinearMap.map_smul,
    mul_zero, sub_zero, sub_self]

Result:
no goals

Proof state:
case algebraMap
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
r✝ : R
⊢ (contractLeft d) ((contractLeft d) ((algebraMap R (CliffordAlgebra Q)) r✝)) = 0

Tactic:
simp_rw [contractLeft_algebraMap, map_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
theorem ae_eq_condExp_of_forall_setIntegral_eq (hm : m ≤ m₀) [SigmaFinite (μ.trim hm)]
    {f g : α → E} (hf : Integrable f μ)
    (hg_int_finite : ∀ s, MeasurableSet[m] s → μ s < ∞ → IntegrableOn g s μ)
    (hg_eq : ∀ s : Set α, MeasurableSet[m] s → μ s < ∞ → ∫ x in s, g x ∂μ = ∫ x in s, f x ∂μ)
    (hgm : AEStronglyMeasurable[m] g μ) : g =ᵐ[μ] μ[f|m]

Proof state:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
hm : m ≤ m₀
inst✝ : SigmaFinite (μ.trim hm)
f g : α → E
hf : Integrable f μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ
hg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, f x ∂μ
hgm : AEStronglyMeasurable g μ
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, (μ[f|m]) x ∂μ

Tactic:
rw [hg_eq s hs hμs, setIntegral_condExp hm hf hs]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
hm : m ≤ m₀
inst✝ : SigmaFinite (μ.trim hm)
f g : α → E
hf : Integrable f μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ
hg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, f x ∂μ
hgm : AEStronglyMeasurable g μ
⊢ g =ᶠ[ae μ] μ[f|m]

Tactic:
refine ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' hm hg_int_finite
  (fun s _ _ => integrable_condExp.integrableOn) (fun s hs hμs => ?_) hgm
  (StronglyMeasurable.aestronglyMeasurable stronglyMeasurable_condExp)

Result:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
hm : m ≤ m₀
inst✝ : SigmaFinite (μ.trim hm)
f g : α → E
hf : Integrable f μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ
hg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, f x ∂μ
hgm : AEStronglyMeasurable g μ
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, (μ[f|m]) x ∂μ
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma shift_units_smul (a : ℤ) (x : Rˣ) :
    (x • γ).shift a = x • (γ.shift a)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a : ℤ
x : Rˣ
⊢ (x • γ).shift a = x • γ.shift a

Tactic:
ext p q hpq

Result:
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a : ℤ
x : Rˣ
p q : ℤ
hpq : p + n = q
⊢ ((x • γ).shift a).v p q hpq = (x • γ.shift a).v p q hpq

Proof state:
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a : ℤ
x : Rˣ
p q : ℤ
hpq : p + n = q
⊢ ((x • γ).shift a).v p q hpq = x • (γ.shift a).v p q hpq

Tactic:
simp only [shift_v', units_smul_v]

Result:
no goals

Proof state:
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a : ℤ
x : Rˣ
p q : ℤ
hpq : p + n = q
⊢ ((x • γ).shift a).v p q hpq = (x • γ.shift a).v p q hpq

Tactic:
dsimp

Result:
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a : ℤ
x : Rˣ
p q : ℤ
hpq : p + n = q
⊢ ((x • γ).shift a).v p q hpq = x • (γ.shift a).v p q hpq
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_alter [LawfulBEq α] {k k' : α} {fallback : β k'} {f : Option (β k) → Option (β k)}
    (h : m.WF) : (m.alter k f).getD k' fallback =
      if heq : k == k' then
        f (m.get? k) |>.map (cast (congrArg β <| eq_of_beq heq)) |>.getD fallback
      else
        m.getD k' fallback

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k k' : α
fallback : β k'
f : Option (β k) → Option (β k)
h : m.WF
⊢ (m.alter k f).getD k' fallback =
    if heq : (k == k') = true then (Option.map (cast ⋯) (f (m.get? k))).getD fallback else m.getD k' fallback

Tactic:
simp_to_raw using Raw₀.getD_alter

Result:
no goals