harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
    {l : List α} {k k' fallback : α} (k_beq : k == k')
    (not_mem : ¬ k ∈ m)
    (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) :
    getKeyD (insertManyIfNewUnit m l) k' fallback = k

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k k' fallback : α
k_beq : (k == k') = true
not_mem : ¬k ∈ m
distinct : List.Pairwise (fun a b => (a == b) = false) l
mem : k ∈ l
⊢ (insertManyIfNewUnit m l).getKeyD k' fallback = k

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true] at not_mem

Result:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k k' fallback : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a == b) = false) l
mem : k ∈ l
not_mem : m.contains k = false
⊢ (insertManyIfNewUnit m l).getKeyD k' fallback = k

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k k' fallback : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a == b) = false) l
mem : k ∈ l
not_mem : m.contains k = false
⊢ (insertManyIfNewUnit m l).getKeyD k' fallback = k

Tactic:
exact Raw₀.Const.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_mem ⟨m.1, _⟩ m.2 k_beq
  not_mem distinct mem

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_le_size_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List α} :
    m.1.size ≤ (insertManyIfNewUnit m l).1.1.size

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw₀ α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List α
⊢ m.val.size ≤ (insertManyIfNewUnit m l).val.val.size

Tactic:
simp_to_model [Const.insertManyIfNewUnit] using List.length_le_length_insertListIfNewUnit

Result:
no goals
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem isSeparable_algebraMap (x : F) : IsSeparable F ((algebraMap F E) x)

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : F
⊢ (minpoly F x).Separable

Tactic:
exact Algebra.IsSeparable.isSeparable F x

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : F
⊢ IsSeparable F ((algebraMap F E) x)

Tactic:
rw [IsSeparable, minpoly.algebraMap_eq (algebraMap F E).injective]

Result:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : F
⊢ (minpoly F x).Separable
-- Mathlib/Data/List/ToFinsupp.lean
theorem toFinsupp_singleton (x : M) [DecidablePred (getD [x] · 0 ≠ 0)] :
    toFinsupp [x] = Finsupp.single 0 x

Proof state:
M : Type u_1
inst✝¹ : Zero M
x : M
inst✝ : DecidablePred fun x_1 => [x].getD x_1 0 ≠ 0
⊢ [x].toFinsupp = Finsupp.single 0 x

Tactic:
ext ⟨_ | i⟩ <;> simp [Finsupp.single_apply, (Nat.zero_lt_succ _).ne]

Result:
no goals
-- Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean
theorem deriv_sqrt_mul_log (x : ℝ) :
    deriv (fun x => √x * log x) x = (2 + log x) / (2 * √x)

Proof state:
x : ℝ
⊢ deriv (fun x => √x * log x) x = (2 + log x) / (2 * √x)

Tactic:
rcases lt_or_le 0 x with hx | hx

Result:
case inl
x : ℝ
hx : 0 < x
⊢ deriv (fun x => √x * log x) x = (2 + log x) / (2 * √x)

case inr
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x => √x * log x) x = (2 + log x) / (2 * √x)

Proof state:
case inl
x : ℝ
hx : 0 < x
⊢ deriv (fun x => √x * log x) x = (2 + log x) / (2 * √x)

Tactic:
exact (hasDerivAt_sqrt_mul_log hx.ne').deriv

Result:
no goals

Proof state:
case inr
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x => √x * log x) x = (2 + log x) / (2 * √x)

Tactic:
rw [sqrt_eq_zero_of_nonpos hx, mul_zero, div_zero]

Result:
case inr
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x => √x * log x) x = 0

Proof state:
case inr
x : ℝ
hx : x ≤ 0
⊢ HasDerivWithinAt (fun x => √x * log x) 0 (Iic 0) x

Tactic:
refine (hasDerivWithinAt_const x _ 0).congr_of_mem (fun x hx => ?_) hx

Result:
case inr
x✝ : ℝ
hx✝ : x✝ ≤ 0
x : ℝ
hx : x ∈ Iic 0
⊢ √x * log x = 0

Proof state:
case inr
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x => √x * log x) x = 0

Tactic:
refine HasDerivWithinAt.deriv_eq_zero ?_ (uniqueDiffOn_Iic 0 x hx)

Result:
case inr
x : ℝ
hx : x ≤ 0
⊢ HasDerivWithinAt (fun x => √x * log x) 0 (Iic 0) x

Proof state:
case inr
x✝ : ℝ
hx✝ : x✝ ≤ 0
x : ℝ
hx : x ∈ Iic 0
⊢ √x * log x = 0

Tactic:
rw [sqrt_eq_zero_of_nonpos hx, zero_mul]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
theorem exists_mem_subalgebra_near_continuousMap_of_separatesPoints (A : Subalgebra ℝ C(X, ℝ))
    (w : A.SeparatesPoints) (f : C(X, ℝ)) (ε : ℝ) (pos : 0 < ε) :
    ∃ g : A, ‖(g : C(X, ℝ)) - f‖ < ε

Proof state:
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w✝ : A.SeparatesPoints
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x ∈ Metric.ball f i, x ∈ ↑A.toSubsemiring
g : C(X, ℝ)
H : ‖g - f‖ < ε
m : g ∈ ↑A.toSubsemiring
⊢ ∃ g, ‖↑g - f‖ < ε

Tactic:
exact ⟨⟨g, m⟩, H⟩

Result:
no goals

Proof state:
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w✝ : A.SeparatesPoints
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x ∈ Metric.ball f i, x ∈ ↑A.toSubsemiring
g : C(X, ℝ)
H : g ∈ Metric.ball f ε
m : g ∈ ↑A.toSubsemiring
⊢ ∃ g, ‖↑g - f‖ < ε

Tactic:
rw [Metric.mem_ball, dist_eq_norm] at H

Result:
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w✝ : A.SeparatesPoints
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x ∈ Metric.ball f i, x ∈ ↑A.toSubsemiring
g : C(X, ℝ)
H : ‖g - f‖ < ε
m : g ∈ ↑A.toSubsemiring
⊢ ∃ g, ‖↑g - f‖ < ε

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w✝ : A.SeparatesPoints
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
w : ∃ᶠ (x : C(X, ℝ)) in 𝓝 f, x ∈ ↑A.toSubsemiring
⊢ ∃ g, ‖↑g - f‖ < ε

Tactic:
rw [Metric.nhds_basis_ball.frequently_iff] at w

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w✝ : A.SeparatesPoints
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x ∈ Metric.ball f i, x ∈ ↑A.toSubsemiring
⊢ ∃ g, ‖↑g - f‖ < ε

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
⊢ ∃ g, ‖↑g - f‖ < ε

Tactic:
have w :=
  mem_closure_iff_frequently.mp (continuousMap_mem_subalgebra_closure_of_separatesPoints A w f)

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w✝ : A.SeparatesPoints
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
w : ∃ᶠ (x : C(X, ℝ)) in 𝓝 f, x ∈ ↑A.toSubsemiring
⊢ ∃ g, ‖↑g - f‖ < ε

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w✝ : A.SeparatesPoints
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x ∈ Metric.ball f i, x ∈ ↑A.toSubsemiring
⊢ ∃ g, ‖↑g - f‖ < ε

Tactic:
obtain ⟨g, H, m⟩ := w ε pos

Result:
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w✝ : A.SeparatesPoints
f : C(X, ℝ)
ε : ℝ
pos : 0 < ε
w : ∀ (i : ℝ), 0 < i → ∃ x ∈ Metric.ball f i, x ∈ ↑A.toSubsemiring
g : C(X, ℝ)
H : g ∈ Metric.ball f ε
m : g ∈ ↑A.toSubsemiring
⊢ ∃ g, ‖↑g - f‖ < ε
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem attachWith_map_coe {p : α → Prop} (f : α → β) (o : Option α) (H : ∀ a ∈ o, p a) :
    ((o.attachWith p H).map fun (i : { i // p i}) => f i.val) = o.map f

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
f : α → β
o : Option α
H : ∀ (a : α), a ∈ o → p a
⊢ Option.map (fun i => f i.val) (o.attachWith p H) = Option.map f o

Tactic:
cases o <;> simp [H]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Prod.lean
lemma measure_prod_compl_eq_zero {s : Set α} {t : Set β}
    (s_ae_univ : μ sᶜ = 0) (t_ae_univ : ν tᶜ = 0) :
    μ.prod ν (s ×ˢ t)ᶜ = 0

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
s_ae_univ : μ sᶜ = 0
t_ae_univ : ν tᶜ = 0
⊢ (μ.prod ν) (sᶜ ×ˢ univ) = 0 ∧ (μ.prod ν) (univ ×ˢ tᶜ) = 0

Tactic:
simp [s_ae_univ, t_ae_univ]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
s_ae_univ : μ sᶜ = 0
t_ae_univ : ν tᶜ = 0
⊢ (μ.prod ν) (s ×ˢ t)ᶜ = 0

Tactic:
rw [Set.compl_prod_eq_union, measure_union_null_iff]

Result:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
s_ae_univ : μ sᶜ = 0
t_ae_univ : ν tᶜ = 0
⊢ (μ.prod ν) (sᶜ ×ˢ univ) = 0 ∧ (μ.prod ν) (univ ×ˢ tᶜ) = 0
-- Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
theorem restrict_ofFunction (s : Set α) (hm : Monotone m) :
    restrict s (OuterMeasure.ofFunction m m_empty) =
      OuterMeasure.ofFunction (fun t => m (t ∩ s)) (by simp; simp [m_empty])

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ (map Subtype.val ∘ₗ comap Subtype.val) (OuterMeasure.ofFunction m m_empty) =
    OuterMeasure.ofFunction (fun t => m (t ∩ s)) ⋯

Tactic:
simp only [inter_comm _ s, LinearMap.comp_apply]

Result:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ (map Subtype.val) ((comap Subtype.val) (OuterMeasure.ofFunction m m_empty)) =
    OuterMeasure.ofFunction (fun t => m (s ∩ t)) ⋯

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ m ∅ = 0

Tactic:
simp [m_empty]

Result:
no goals

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ (fun t => m (t ∩ s)) ∅ = 0

Tactic:
simp

Result:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ m ∅ = 0

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ (map Subtype.val) ((comap Subtype.val) (OuterMeasure.ofFunction m m_empty)) =
    OuterMeasure.ofFunction (fun t => m (s ∩ t)) ⋯

Tactic:
rw [comap_ofFunction _ (Or.inl hm)]

Result:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ (map Subtype.val) (OuterMeasure.ofFunction (fun s_1 => m (Subtype.val '' s_1)) ⋯) =
    OuterMeasure.ofFunction (fun t => m (s ∩ t)) ⋯

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ (restrict s) (OuterMeasure.ofFunction m m_empty) = OuterMeasure.ofFunction (fun t => m (t ∩ s)) ⋯

Tactic:
rw [restrict]

Result:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ (map Subtype.val ∘ₗ comap Subtype.val) (OuterMeasure.ofFunction m m_empty) =
    OuterMeasure.ofFunction (fun t => m (t ∩ s)) ⋯

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ (map Subtype.val) (OuterMeasure.ofFunction (fun s_1 => m (Subtype.val '' s_1)) ⋯) =
    OuterMeasure.ofFunction (fun t => m (s ∩ t)) ⋯

Tactic:
simp only [map_ofFunction Subtype.coe_injective, Subtype.image_preimage_coe]

Result:
no goals
-- Mathlib/Algebra/Polynomial/PartialFractions.lean
theorem div_eq_quo_add_rem_div_add_rem_div (f : R[X]) {g₁ g₂ : R[X]} (hg₁ : g₁.Monic)
    (hg₂ : g₂.Monic) (hcoprime : IsCoprime g₁ g₂) :
    ∃ q r₁ r₂ : R[X],
      r₁.degree < g₁.degree ∧
        r₂.degree < g₂.degree ∧ (f : K) / (↑g₁ * ↑g₂) = ↑q + ↑r₁ / ↑g₁ + ↑r₂ / ↑g₂

Proof state:
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
c d : R[X]
hcd : c * g₁ + d * g₂ = 1
hg₁' : ↑g₁ ≠ 0
⊢ ¬g₂ = 0

Tactic:
exact hg₂.ne_zero

Result:
no goals

Proof state:
case intro.intro
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
c d : R[X]
hcd : c * g₁ + d * g₂ = 1
hg₁' : ↑g₁ ≠ 0
hg₂' : ↑g₂ ≠ 0
hfc : f * c %ₘ g₂ + g₂ * (f * c /ₘ g₂) = f * c
hfd : f * d %ₘ g₁ + g₁ * (f * d /ₘ g₁) = f * d
⊢ ↑f / (↑g₁ * ↑g₂) = ↑(f * d /ₘ g₁ + f * c /ₘ g₂) + ↑(f * d %ₘ g₁) / ↑g₁ + ↑(f * c %ₘ g₂) / ↑g₂

Tactic:
field_simp

Result:
case intro.intro
R : Type
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g₁ g₂ : R[X]
hg₁ : g₁.Monic
hg₂ : g₂.Monic
c d : R[X]
hcd : c * g₁ + d * g₂ = 1
hg₁' : ↑g₁ ≠ 0
hg₂' : ↑g₂ ≠ 0
hfc : f * c %ₘ g₂ + g₂ * (f * c /ₘ g₂) = f * c
hfd : f * d %ₘ g₁ + g₁ * (f * d /ₘ g₁) = f * d
⊢ ↑f =
    (((algebraMap R[X] K) (f * d /ₘ g₁) + (algebraMap R[X] K) (f * c /ₘ g₂)) * ↑g₁ + ↑(f * d %ₘ g₁)) * ↑g₂ +
      ↑(f * c %ₘ g₂) * ↑g₁
-- Mathlib/NumberTheory/DiophantineApproximation/Basic.lean
theorem convergent_of_zero (n : ℕ) : convergent 0 n = 0

Proof state:
n : ℕ
⊢ convergent 0 n = 0

Tactic:
induction n with
| zero => simp only [convergent_zero, floor_zero, cast_zero]
| succ n ih =>
  simp only [ih, convergent_succ, floor_zero, cast_zero, fract_zero, add_zero, inv_zero]

Result:
no goals

Proof state:
case succ
n : ℕ
ih : convergent 0 n = 0
⊢ convergent 0 (n + 1) = 0

Tactic:
simp only [ih, convergent_succ, floor_zero, cast_zero, fract_zero, add_zero, inv_zero]

Result:
no goals

Proof state:
case zero

⊢ convergent 0 0 = 0

Tactic:
simp only [convergent_zero, floor_zero, cast_zero]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Unique.lean
lemma condKernel_compProd (μ : Measure α) [IsFiniteMeasure μ] (κ : Kernel α Ω) [IsMarkovKernel κ] :
    (μ ⊗ₘ κ).condKernel =ᵐ[μ] κ

Proof state:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
κ : Kernel α Ω
inst✝ : IsMarkovKernel κ
this : ⇑κ =ᶠ[ae (μ ⊗ₘ κ).fst] ⇑(μ ⊗ₘ κ).condKernel
⊢ ⇑(μ ⊗ₘ κ).condKernel =ᶠ[ae μ] ⇑κ

Tactic:
symm

Result:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
κ : Kernel α Ω
inst✝ : IsMarkovKernel κ
this : ⇑κ =ᶠ[ae (μ ⊗ₘ κ).fst] ⇑(μ ⊗ₘ κ).condKernel
⊢ ⇑κ =ᶠ[ae μ] ⇑(μ ⊗ₘ κ).condKernel

Proof state:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
κ : Kernel α Ω
inst✝ : IsMarkovKernel κ
⊢ ⇑κ =ᶠ[ae (μ ⊗ₘ κ).fst] ⇑(μ ⊗ₘ κ).condKernel

Tactic:
refine eq_condKernel_of_measure_eq_compProd _ ?_

Result:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
κ : Kernel α Ω
inst✝ : IsMarkovKernel κ
⊢ μ ⊗ₘ κ = (μ ⊗ₘ κ).fst ⊗ₘ κ

Proof state:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
κ : Kernel α Ω
inst✝ : IsMarkovKernel κ
⊢ ⇑(μ ⊗ₘ κ).condKernel =ᶠ[ae μ] ⇑κ

Tactic:
suffices κ =ᵐ[(μ ⊗ₘ κ).fst] (μ ⊗ₘ κ).condKernel by symm; rwa [Measure.fst_compProd] at this

Result:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
κ : Kernel α Ω
inst✝ : IsMarkovKernel κ
⊢ ⇑κ =ᶠ[ae (μ ⊗ₘ κ).fst] ⇑(μ ⊗ₘ κ).condKernel

Proof state:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
κ : Kernel α Ω
inst✝ : IsMarkovKernel κ
⊢ μ ⊗ₘ κ = (μ ⊗ₘ κ).fst ⊗ₘ κ

Tactic:
rw [Measure.fst_compProd]

Result:
no goals

Proof state:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
κ : Kernel α Ω
inst✝ : IsMarkovKernel κ
this : ⇑κ =ᶠ[ae (μ ⊗ₘ κ).fst] ⇑(μ ⊗ₘ κ).condKernel
⊢ ⇑κ =ᶠ[ae μ] ⇑(μ ⊗ₘ κ).condKernel

Tactic:
rwa [Measure.fst_compProd] at this

Result:
no goals
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem repr_ceil_apply (m : E) (i : ι) : b.repr (ceil b m) i = ⌈b.repr m i⌉

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 ι
m : E
i : ι
⊢ (b.repr ↑(ceil b m)) i = ↑⌈(b.repr m) i⌉

Tactic:
classical simp only [ceil, ← Int.cast_smul_eq_zsmul K, b.repr.map_smul, Finsupp.single_apply,
  Finset.sum_apply', Basis.repr_self, Finsupp.smul_single', mul_one, Finset.sum_ite_eq', coe_sum,
  Finset.mem_univ, if_true, coe_smul_of_tower, Basis.restrictScalars_apply, map_sum]

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 ι
m : E
i : ι
⊢ (b.repr ↑(ceil b m)) i = ↑⌈(b.repr m) i⌉

Tactic:
simp only [ceil, ← Int.cast_smul_eq_zsmul K, b.repr.map_smul, Finsupp.single_apply,
Finset.sum_apply', Basis.repr_self, Finsupp.smul_single', mul_one, Finset.sum_ite_eq', coe_sum,
Finset.mem_univ, if_true, coe_smul_of_tower, Basis.restrictScalars_apply, map_sum]

Result:
no goals
-- Mathlib/Algebra/Ring/CharZero.lean
theorem add_self_eq_zero {a : R} : a + a = 0 ↔ a = 0

Proof state:
R : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
a : R
⊢ a + a = 0 ↔ a = 0

Tactic:
simp only [(two_mul a).symm, mul_eq_zero, two_ne_zero, false_or]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean
theorem exists_one_lt_mul_of_lt (h : a < b) : ∃ (c : _) (_ : 1 < c), a * c = b

Proof state:
α : Type u
inst✝² : MulOneClass α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedMul α
a b : α
h : a < b
⊢ ∃ c x, a * c = b

Tactic:
obtain ⟨c, hc⟩ := le_iff_exists_mul.1 h.le

Result:
case intro
α : Type u
inst✝² : MulOneClass α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedMul α
a b : α
h : a < b
c : α
hc : b = a * c
⊢ ∃ c x, a * c = b

Proof state:
case intro
α : Type u
inst✝² : MulOneClass α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedMul α
a b : α
h : a < b
hc : b = a * 1
⊢ False

Tactic:
simp [hc, lt_irrefl] at h

Result:
no goals

Proof state:
case intro
α : Type u
inst✝² : MulOneClass α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedMul α
a b : α
h : a < b
c : α
hc : b = a * c
⊢ ∃ c x, a * c = b

Tactic:
refine ⟨c, one_lt_iff_ne_one.2 ?_, hc.symm⟩

Result:
case intro
α : Type u
inst✝² : MulOneClass α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedMul α
a b : α
h : a < b
c : α
hc : b = a * c
⊢ c ≠ 1

Proof state:
case intro
α : Type u
inst✝² : MulOneClass α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedMul α
a b : α
h : a < b
c : α
hc : b = a * c
⊢ c ≠ 1

Tactic:
rintro rfl

Result:
case intro
α : Type u
inst✝² : MulOneClass α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedMul α
a b : α
h : a < b
hc : b = a * 1
⊢ False
-- Mathlib/Algebra/BigOperators/Expect.lean
@[simp] lemma expect_const (hs : s.Nonempty) (a : M) : 𝔼 _i ∈ s, a = a

Proof state:
case ha
ι : Type u_1
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
hs : s.Nonempty
a : M
⊢ ↑(#s) ≠ 0

Tactic:
exact mod_cast hs.card_ne_zero

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
hs : s.Nonempty
a : M
⊢ 𝔼 _i ∈ s, a = a

Tactic:
rw [expect, sum_const, ← Nat.cast_smul_eq_nsmul ℚ≥0, inv_smul_smul₀]

Result:
case ha
ι : Type u_1
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
hs : s.Nonempty
a : M
⊢ ↑(#s) ≠ 0
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem toSpanNonzeroSingleton_apply (t : R) :
    toSpanNonzeroSingleton R M x h t =
      (⟨t • x, Submodule.smul_mem _ _ (Submodule.mem_span_singleton_self x)⟩ : R ∙ x)

Proof state:
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x : M
h : x ≠ 0
t : R
⊢ (toSpanNonzeroSingleton R M x h) t = ⟨t • x, ⋯⟩

Tactic:
rfl

Result:
no goals
-- Mathlib/ModelTheory/Fraisse.lean
theorem IsUltrahomogeneous.amalgamation_age (h : L.IsUltrahomogeneous M) :
    Amalgamation (L.age M)

Proof state:
case intro.intro.intro.intro.intro.intro.intro
L : Language
M : Type w
inst✝ : L.Structure M
h : L.IsUltrahomogeneous M
N P Q : Bundled L.Structure
NP : ↑N ↪[L] ↑P
NQ : ↑N ↪[L] ↑Q
Nfg : Structure.FG L ↑N
Pfg : Structure.FG L ↑P
PM : ↑P ↪[L] M
Qfg : Structure.FG L ↑Q
QM : ↑Q ↪[L] M
g : M ≃[L] M
hg : (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype
s : L.Substructure M := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range
⊢ ((Substructure.inclusion ⋯).comp (g.toEmbedding.comp PM).equivRange.toEmbedding).comp NP =
    ((Substructure.inclusion ⋯).comp QM.equivRange.toEmbedding).comp NQ

Tactic:
ext n

Result:
case intro.intro.intro.intro.intro.intro.intro.h
L : Language
M : Type w
inst✝ : L.Structure M
h : L.IsUltrahomogeneous M
N P Q : Bundled L.Structure
NP : ↑N ↪[L] ↑P
NQ : ↑N ↪[L] ↑Q
Nfg : Structure.FG L ↑N
Pfg : Structure.FG L ↑P
PM : ↑P ↪[L] M
Qfg : Structure.FG L ↑Q
QM : ↑Q ↪[L] M
g : M ≃[L] M
hg : (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype
s : L.Substructure M := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range
n : ↑N
⊢ (((Substructure.inclusion ⋯).comp (g.toEmbedding.comp PM).equivRange.toEmbedding).comp NP) n =
    (((Substructure.inclusion ⋯).comp QM.equivRange.toEmbedding).comp NQ) n

Proof state:
case intro.intro.intro.intro.intro.intro.intro.h.a
L : Language
M : Type w
inst✝ : L.Structure M
h : L.IsUltrahomogeneous M
N P Q : Bundled L.Structure
NP : ↑N ↪[L] ↑P
NQ : ↑N ↪[L] ↑Q
Nfg : Structure.FG L ↑N
Pfg : Structure.FG L ↑P
PM : ↑P ↪[L] M
Qfg : Structure.FG L ↑Q
QM : ↑Q ↪[L] M
g : M ≃[L] M
hg : (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype
s : L.Substructure M := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range
n : ↑N
hgn : QM (NQ n) = g (PM (NP n))
⊢ ↑((Substructure.inclusion ⋯) ((g.toEmbedding.comp PM).equivRange.toEmbedding (NP n))) =
    ↑((Substructure.inclusion ⋯) (QM.equivRange (NQ n)))

Tactic:
erw [Substructure.coe_inclusion, Substructure.coe_inclusion]

Result:
case intro.intro.intro.intro.intro.intro.intro.h.a
L : Language
M : Type w
inst✝ : L.Structure M
h : L.IsUltrahomogeneous M
N P Q : Bundled L.Structure
NP : ↑N ↪[L] ↑P
NQ : ↑N ↪[L] ↑Q
Nfg : Structure.FG L ↑N
Pfg : Structure.FG L ↑P
PM : ↑P ↪[L] M
Qfg : Structure.FG L ↑Q
QM : ↑Q ↪[L] M
g : M ≃[L] M
hg : (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype
s : L.Substructure M := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range
n : ↑N
hgn : QM (NQ n) = g (PM (NP n))
⊢ ↑(Set.inclusion ⋯ ((g.toEmbedding.comp PM).equivRange.toEmbedding (NP n))) = ↑(Set.inclusion ⋯ (QM.equivRange (NQ n)))