harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Filter/Basic.lean
theorem eq_top_of_neBot [Subsingleton α] (l : Filter α) [NeBot l] : l = ⊤

Proof state:
α : Type u
inst✝¹ : Subsingleton α
l : Filter α
inst✝ : l.NeBot
s : Set α
hs : s ∈ l
⊢ s ∈ ⊤

Tactic:
obtain rfl : s = univ := Subsingleton.eq_univ_of_nonempty (nonempty_of_mem hs)

Result:
α : Type u
inst✝¹ : Subsingleton α
l : Filter α
inst✝ : l.NeBot
hs : univ ∈ l
⊢ univ ∈ ⊤

Proof state:
α : Type u
inst✝¹ : Subsingleton α
l : Filter α
inst✝ : l.NeBot
hs : univ ∈ l
⊢ univ ∈ ⊤

Tactic:
exact univ_mem

Result:
no goals

Proof state:
α : Type u
inst✝¹ : Subsingleton α
l : Filter α
inst✝ : l.NeBot
⊢ l = ⊤

Tactic:
refine top_unique fun s hs => ?_

Result:
α : Type u
inst✝¹ : Subsingleton α
l : Filter α
inst✝ : l.NeBot
s : Set α
hs : s ∈ l
⊢ s ∈ ⊤
-- Mathlib/SetTheory/Cardinal/Finite.lean
theorem card_lt_top_of_finite [Finite α] : card α < ⊤

Proof state:
α : Type u_1
inst✝ : Finite α
⊢ card α < ⊤

Tactic:
simp [card]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
theorem singularPart_smul (s : SignedMeasure α) (μ : Measure α) (r : ℝ) :
    (r • s).singularPart μ = r • s.singularPart μ

Proof state:
case inl.intro
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
⊢ (↑r • s).singularPart μ = ↑r • s.singularPart μ

Tactic:
exact singularPart_smul_nnreal s μ r

Result:
no goals

Proof state:
case inr
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
⊢ (r • s).singularPart μ = r • s.singularPart μ

Tactic:
rw [singularPart, singularPart]

Result:
case inr
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
⊢ ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)

Proof state:
case inr
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
⊢ ((-r).toNNReal • s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure -
      ((-r).toNNReal • s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)

Tactic:
rw [toSignedMeasure_smul, toSignedMeasure_smul, ← neg_sub, ← smul_sub, NNReal.smul_def,
  ← neg_smul, Real.coe_toNNReal _ (le_of_lt (neg_pos.mpr hr)), neg_neg]

Result:
no goals

Proof state:
case inl
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : 0 ≤ r
⊢ (r • s).singularPart μ = r • s.singularPart μ

Tactic:
lift r to ℝ≥0 using hr

Result:
case inl.intro
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
⊢ (↑r • s).singularPart μ = ↑r • s.singularPart μ
-- Mathlib/Data/Finset/BooleanAlgebra.lean
lemma univ_val_map_subtype_restrict [Fintype α] (f : α → β)
    (p : α → Prop) [DecidablePred p] [Fintype {a // p a}] :
    univ.val.map (Subtype.restrict p f) = (univ.filter p).val.map f

Proof state:
α : Type u_1
β : Type u_2
inst✝² : Fintype α
f : α → β
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ Multiset.map (Subtype.restrict p f) univ.val = Multiset.map f (filter p univ).val

Tactic:
rw [← univ_val_map_subtype_val, Multiset.map_map, Subtype.restrict_def]

Result:
no goals
-- Mathlib/RingTheory/Kaehler/CotangentComplex.lean
lemma subsingleton_h1Cotangent (P : Extension R S) :
    Subsingleton P.H1Cotangent ↔ Function.Injective P.cotangentComplex

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ Subsingleton ↥(LinearMap.ker P.cotangentComplex) ↔ Function.Injective ⇑P.cotangentComplex

Tactic:
rw [← LinearMap.ker_eq_bot, Submodule.eq_bot_iff, subsingleton_iff_forall_eq 0, Subtype.forall']

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (∀ (y : ↥(LinearMap.ker P.cotangentComplex)), y = 0) ↔ ∀ (x : ↥(LinearMap.ker P.cotangentComplex)), ↑x = 0

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (∀ (y : ↥(LinearMap.ker P.cotangentComplex)), y = 0) ↔ ∀ (x : ↥(LinearMap.ker P.cotangentComplex)), ↑x = 0

Tactic:
simp only [Subtype.ext_iff, Submodule.coe_zero]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ Subsingleton P.H1Cotangent ↔ Function.Injective ⇑P.cotangentComplex

Tactic:
delta Extension.H1Cotangent

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ Subsingleton ↥(LinearMap.ker P.cotangentComplex) ↔ Function.Injective ⇑P.cotangentComplex
-- Mathlib/Algebra/Lie/Weights/Basic.lean
lemma lie_mem_maxGenEigenspace_toEnd
    {χ₁ χ₂ : R} {x y : L} {m : M} (hy : y ∈ 𝕎(L, χ₁, x)) (hm : m ∈ 𝕎(M, χ₂, x)) :
    ⁅y, m⁆ ∈ 𝕎(M, χ₁ + χ₂, x)

Proof state:
case h
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
χ₁ χ₂ : R
x y : L
m : M
hy : y ∈ 𝕎(L, χ₁, x)
hm : m ∈ 𝕎(M, χ₂, x)
⊢ (toModuleHom R L M) ((TensorProduct.map 𝕎(L, χ₁, x).subtype 𝕎(M, χ₂, x).subtype) (⟨y, hy⟩ ⊗ₜ[R] ⟨m, hm⟩)) = ⁅y, m⁆

Tactic:
simp only [Submodule.subtype_apply, toModuleHom_apply, TensorProduct.map_tmul]

Result:
no goals

Proof state:
case a
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
χ₁ χ₂ : R
x y : L
m : M
hy : y ∈ 𝕎(L, χ₁, x)
hm : m ∈ 𝕎(M, χ₂, x)
⊢ ⁅y, m⁆ ∈ LinearMap.range (↑(toModuleHom R L M) ∘ₗ TensorProduct.mapIncl 𝕎(L, χ₁, x) 𝕎(M, χ₂, x))

Tactic:
simp only [LieModuleHom.coe_toLinearMap, Function.comp_apply, LinearMap.coe_comp,
  TensorProduct.mapIncl, LinearMap.mem_range]

Result:
case a
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
χ₁ χ₂ : R
x y : L
m : M
hy : y ∈ 𝕎(L, χ₁, x)
hm : m ∈ 𝕎(M, χ₂, x)
⊢ ∃ y_1, (toModuleHom R L M) ((TensorProduct.map 𝕎(L, χ₁, x).subtype 𝕎(M, χ₂, x).subtype) y_1) = ⁅y, m⁆

Proof state:
case a
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
χ₁ χ₂ : R
x y : L
m : M
hy : y ∈ 𝕎(L, χ₁, x)
hm : m ∈ 𝕎(M, χ₂, x)
⊢ ∃ y_1, (toModuleHom R L M) ((TensorProduct.map 𝕎(L, χ₁, x).subtype 𝕎(M, χ₂, x).subtype) y_1) = ⁅y, m⁆

Tactic:
use ⟨y, hy⟩ ⊗ₜ ⟨m, hm⟩

Result:
case h
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
χ₁ χ₂ : R
x y : L
m : M
hy : y ∈ 𝕎(L, χ₁, x)
hm : m ∈ 𝕎(M, χ₂, x)
⊢ (toModuleHom R L M) ((TensorProduct.map 𝕎(L, χ₁, x).subtype 𝕎(M, χ₂, x).subtype) (⟨y, hy⟩ ⊗ₜ[R] ⟨m, hm⟩)) = ⁅y, m⁆

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
χ₁ χ₂ : R
x y : L
m : M
hy : y ∈ 𝕎(L, χ₁, x)
hm : m ∈ 𝕎(M, χ₂, x)
⊢ ⁅y, m⁆ ∈ 𝕎(M, χ₁ + χ₂, x)

Tactic:
apply LieModule.weight_vector_multiplication L M M (toModuleHom R L M) χ₁ χ₂

Result:
case a
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
χ₁ χ₂ : R
x y : L
m : M
hy : y ∈ 𝕎(L, χ₁, x)
hm : m ∈ 𝕎(M, χ₂, x)
⊢ ⁅y, m⁆ ∈ LinearMap.range (↑(toModuleHom R L M) ∘ₗ TensorProduct.mapIncl 𝕎(L, χ₁, x) 𝕎(M, χ₂, x))
-- Mathlib/MeasureTheory/Function/UniformIntegrable.lean
theorem UniformIntegrable.ae_eq {g : ι → α → β} (hf : UniformIntegrable f p μ)
    (hfg : ∀ n, f n =ᵐ[μ] g n) : UniformIntegrable g p μ

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f g : ι → α → β
hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n
hfm : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hunif : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑C
⊢ UniformIntegrable g p μ

Tactic:
refine ⟨fun i => (hfm i).congr (hfg i), (unifIntegrable_congr_ae hfg).1 hunif, C, fun i => ?_⟩

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f g : ι → α → β
hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n
hfm : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hunif : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑C
i : ι
⊢ eLpNorm (g i) p μ ≤ ↑C

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f g : ι → α → β
hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n
hfm : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hunif : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑C
i : ι
⊢ eLpNorm (f i) p μ ≤ ↑C

Tactic:
exact hC i

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f g : ι → α → β
hf : UniformIntegrable f p μ
hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n
⊢ UniformIntegrable g p μ

Tactic:
obtain ⟨hfm, hunif, C, hC⟩ := hf

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f g : ι → α → β
hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n
hfm : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hunif : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑C
⊢ UniformIntegrable g p μ

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f g : ι → α → β
hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n
hfm : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hunif : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑C
i : ι
⊢ eLpNorm (g i) p μ ≤ ↑C

Tactic:
rw [← eLpNorm_congr_ae (hfg i)]

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
f g : ι → α → β
hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n
hfm : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hunif : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (f i) p μ ≤ ↑C
i : ι
⊢ eLpNorm (f i) p μ ≤ ↑C
-- Mathlib/Data/Fintype/Basic.lean
theorem Fin.univ_succ (n : ℕ) :
    (univ : Finset (Fin (n + 1))) =
      Finset.cons 0 (univ.map ⟨Fin.succ, Fin.succ_injective _⟩) (by simp [map_eq_image])

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
⊢ 0 ∉ map { toFun := succ, inj' := ⋯ } univ

Tactic:
simp [map_eq_image]

Result:
no goals

Proof state:
n : ℕ
⊢ univ = Finset.cons 0 (map { toFun := succ, inj' := ⋯ } univ) ⋯

Tactic:
simp [map_eq_image]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma smul_equiv_smul (P Q : Fin 3 → R) {u v : R} (hu : IsUnit u) (hv : IsUnit v) :
    u • P ≈ v • Q ↔ P ≈ Q

Proof state:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ ⟦P⟧ = ⟦Q⟧ ↔ ⟦P⟧ = ⟦Q⟧

Tactic:
rfl

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ u • P ≈ v • Q ↔ P ≈ Q

Tactic:
erw [← Quotient.eq_iff_equiv, ← Quotient.eq_iff_equiv, smul_eq P hu, smul_eq Q hv]

Result:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ ⟦P⟧ = ⟦Q⟧ ↔ ⟦P⟧ = ⟦Q⟧
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast_alterKey_self (k : α) (f : Option (β k) → Option (β k))
    (l : List ((a : α) × β a)) (hl : DistinctKeys l) (hc : containsKey k (alterKey k f l)) :
    haveI hc' : (f (getValueCast? k l)).isSome

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
hl : DistinctKeys l
hc : containsKey k (alterKey k f l) = true
⊢ (if h : (k == k) = true then cast ⋯ ((f (getValueCast? k l)).get ⋯) else getValueCast k l ⋯) =
    (f (getValueCast? k l)).get ⋯

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
hl : DistinctKeys l
hc : containsKey k (alterKey k f l) = true
⊢ getValueCast k (alterKey k f l) hc = (f (getValueCast? k l)).get ⋯

Tactic:
rw [getValueCast_alterKey _ _ _ _ hl]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
hl : DistinctKeys l
hc : containsKey k (alterKey k f l) = true
⊢ (if h : (k == k) = true then cast ⋯ ((f (getValueCast? k l)).get ⋯) else getValueCast k l ⋯) =
    (f (getValueCast? k l)).get ⋯

Proof state:
α : Type u
β : α → Type v
γ : α → Type w
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
hl : DistinctKeys l
hc : containsKey k (alterKey k f l) = true
⊢ (f (getValueCast? k l)).isSome = true

Tactic:
rwa [containsKey_alterKey hl, beq_self_eq_true] at hc

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem mul_zero (a : Rat) : a * 0 = 0

Proof state:
a : Rat
⊢ a * 0 = 0

Tactic:
simp [mul_def]

Result:
no goals
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
@[simp]
lemma uIcc_of_ge (h : b ≤ a) : [[a, b]] = Icc b a

Proof state:
α : Type u_1
inst✝ : Lattice α
a b : α
h : b ≤ a
⊢ [[a, b]] = Icc b a

Tactic:
rw [uIcc, inf_eq_right.2 h, sup_eq_left.2 h]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Basic.lean
theorem zipWithLeft_eq_zipWithLeftTR : @zipWithLeft = @zipWithLeftTR

Proof state:
case h.h.h.h.h.h
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → Option β → γ
as : List α
bs : List β
⊢ zipWithLeft f as bs = zipWithLeftTR.go f as bs #[]

Tactic:
simp [zipWithLeftTR, go]

Result:
no goals

Proof state:
⊢ @zipWithLeft = @zipWithLeftTR

Tactic:
funext α β γ f as bs

Result:
case h.h.h.h.h.h
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → Option β → γ
as : List α
bs : List β
⊢ zipWithLeft f as bs = zipWithLeftTR f as bs

Proof state:
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → Option β → γ
as : List α
bs✝ : List β
acc : Array γ
bs : List β
⊢ zipWithLeftTR.go f [] bs acc = acc.toList ++ zipWithLeft f [] bs

Tactic:
simp [zipWithLeftTR.go]

Result:
no goals

Proof state:
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → Option β → γ
as✝ : List α
bs✝ : List β
acc : Array γ
a : α
as : List α
b : β
bs : List β
⊢ zipWithLeftTR.go f (a :: as) (b :: bs) acc = acc.toList ++ zipWithLeft f (a :: as) (b :: bs)

Tactic:
simp [zipWithLeftTR.go, go _ as bs]

Result:
no goals

Proof state:
case h.h.h.h.h.h
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → Option β → γ
as : List α
bs : List β
⊢ zipWithLeft f as bs = zipWithLeftTR f as bs

Tactic:
simp [zipWithLeftTR]

Result:
case h.h.h.h.h.h
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → Option β → γ
as : List α
bs : List β
⊢ zipWithLeft f as bs = zipWithLeftTR.go f as bs #[]

Proof state:
α : Type u_3
β : Type u_2
γ : Type u_1
f : α → Option β → γ
as : List α
bs : List β
acc : Array γ
head✝ : α
tail✝ : List α
⊢ zipWithLeftTR.go f (head✝ :: tail✝) [] acc = acc.toList ++ zipWithLeft f (head✝ :: tail✝) []

Tactic:
simp [zipWithLeftTR.go, Array.foldl_toList_eq_map]

Result:
no goals
-- Mathlib/Data/TypeVec.lean
theorem append_prod_appendFun {n} {α α' β β' : TypeVec.{u} n} {φ φ' ψ ψ' : Type u}
    {f₀ : α ⟹ α'} {g₀ : β ⟹ β'} {f₁ : φ → φ'} {g₁ : ψ → ψ'} :
    ((f₀ ⊗' g₀) ::: (_root_.Prod.map f₁ g₁)) = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁))

Proof state:
case a.h.fz
n : ℕ
α α' β β' : TypeVec.{u} n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
a : ((α ⊗ β) ::: (φ × ψ)) Fin2.fz
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) Fin2.fz a = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) Fin2.fz a

Tactic:
cases a

Result:
case a.h.fz.mk
n : ℕ
α α' β β' : TypeVec.{u} n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
fst✝ : φ
snd✝ : ψ
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) Fin2.fz (fst✝, snd✝) = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) Fin2.fz (fst✝, snd✝)

Proof state:
case a.h
n : ℕ
α α' β β' : TypeVec.{u} n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
i : Fin2 (n + 1)
a : ((α ⊗ β) ::: (φ × ψ)) i
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) i a = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) i a

Tactic:
cases i

Result:
case a.h.fz
n : ℕ
α α' β β' : TypeVec.{u} n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
a : ((α ⊗ β) ::: (φ × ψ)) Fin2.fz
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) Fin2.fz a = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) Fin2.fz a

case a.h.fs
n : ℕ
α α' β β' : TypeVec.{u} n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
a✝ : Fin2 n
a : ((α ⊗ β) ::: (φ × ψ)) a✝.fs
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) a✝.fs a = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) a✝.fs a

Proof state:
case a.h.fs
n : ℕ
α α' β β' : TypeVec.{u} n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
a✝ : Fin2 n
a : ((α ⊗ β) ::: (φ × ψ)) a✝.fs
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) a✝.fs a = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) a✝.fs a

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
α α' β β' : TypeVec.{u} n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁))

Tactic:
ext i a

Result:
case a.h
n : ℕ
α α' β β' : TypeVec.{u} n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
i : Fin2 (n + 1)
a : ((α ⊗ β) ::: (φ × ψ)) i
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) i a = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) i a

Proof state:
case a.h.fz.mk
n : ℕ
α α' β β' : TypeVec.{u} n
φ φ' ψ ψ' : Type u
f₀ : α ⟹ α'
g₀ : β ⟹ β'
f₁ : φ → φ'
g₁ : ψ → ψ'
fst✝ : φ
snd✝ : ψ
⊢ (f₀ ⊗' g₀ ::: Prod.map f₁ g₁) Fin2.fz (fst✝, snd✝) = ((f₀ ::: f₁) ⊗' (g₀ ::: g₁)) Fin2.fz (fst✝, snd✝)

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem LinearMap.toMatrix'_algebraMap (x : R) :
    LinearMap.toMatrix' (algebraMap R (Module.End R (n → R)) x) = scalar n x

Proof state:
R : Type u_1
inst✝² : CommSemiring R
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
x : R
⊢ toMatrix' ((algebraMap R (Module.End R (n → R))) x) = (scalar n) x

Tactic:
simp [Module.algebraMap_end_eq_smul_id, smul_eq_diagonal_mul]

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
lemma sdiff_sdiff_sdiff_cancel_right (hcb : z ≤ y) : (x \ z) \ (y \ z) = x \ y

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hcb : z ≤ y
⊢ (x \ z) \ (y \ z) = x \ y

Tactic:
rw [le_antisymm_iff, sdiff_le_comm]

Result:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hcb : z ≤ y
⊢ (x \ z) \ (x \ y) ≤ y \ z ∧ x \ y ≤ (x \ z) \ (y \ z)

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hcb : z ≤ y
⊢ (x \ z) \ (x \ y) ≤ y \ z ∧ x \ y ≤ (x \ z) \ (y \ z)

Tactic:
exact ⟨sdiff_sdiff_sdiff_le_sdiff,
  (disjoint_sdiff_self_left.mono_right sdiff_le).le_sdiff_of_le_left <| sdiff_le_sdiff_left hcb⟩

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_univ : μ.restrict univ = μ :=
  ext fun s hs => by simp [hs]

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ (μ.restrict univ) s = μ s

Tactic:
simp [hs]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem tan_oangle_add_left_smul_rotation_pi_div_two {x : V} (h : x ≠ 0) (r : ℝ) :
    Real.Angle.tan (o.oangle (x + r • o.rotation (π / 2 : ℝ) x) (r • o.rotation (π / 2 : ℝ) x)) =
      r⁻¹

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
⊢ (o.oangle (x + r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x)).tan = r⁻¹

Tactic:
rw [o.oangle_add_left_smul_rotation_pi_div_two h, Real.Angle.tan_coe, Real.tan_arctan]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/PairingHeap.lean
theorem Heap.size_tail (le) {s : Heap α} (h : s.NoSibling) : (s.tail le).size = s.size - 1

Proof state:
α : Type u_1
le : α → α → Bool
s : Heap α
h : s.NoSibling
⊢ ((tail? le s).getD nil).size = s.size - 1

Tactic:
match eq : s.tail? le with
| none => cases s with cases eq | nil => rfl
| some tl => simp [Heap.size_tail? h eq]

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
s : Heap α
h : s.NoSibling
eq : tail? le s = none
⊢ (none.getD nil).size = s.size - 1

Tactic:
cases s with cases eq | nil => rfl

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
s : Heap α
h : s.NoSibling
⊢ (tail le s).size = s.size - 1

Tactic:
simp only [Heap.tail]

Result:
α : Type u_1
le : α → α → Bool
s : Heap α
h : s.NoSibling
⊢ ((tail? le s).getD nil).size = s.size - 1

Proof state:
case nil.refl
α : Type u_1
le : α → α → Bool
h : nil.NoSibling
⊢ (none.getD nil).size = nil.size - 1

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
s : Heap α
h : s.NoSibling
tl : Heap α
eq : tail? le s = some tl
⊢ ((some tl).getD nil).size = s.size - 1

Tactic:
simp [Heap.size_tail? h eq]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Hermite/Basic.lean
theorem coeff_hermite_succ_succ (n k : ℕ) : coeff (hermite (n + 1)) (k + 1) =
    coeff (hermite n) k - (k + 2) * coeff (hermite n) (k + 2)

Proof state:
n k : ℕ
⊢ (hermite (n + 1)).coeff (k + 1) = (hermite n).coeff k - (↑k + 2) * (hermite n).coeff (k + 2)

Tactic:
rw [hermite_succ, coeff_sub, coeff_X_mul, coeff_derivative, mul_comm]

Result:
n k : ℕ
⊢ (hermite n).coeff k - (↑(k + 1) + 1) * (hermite n).coeff (k + 1 + 1) =
    (hermite n).coeff k - (↑k + 2) * (hermite n).coeff (k + 2)

Proof state:
n k : ℕ
⊢ (hermite n).coeff k - (↑(k + 1) + 1) * (hermite n).coeff (k + 1 + 1) =
    (hermite n).coeff k - (↑k + 2) * (hermite n).coeff (k + 2)

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Topology/Algebra/StarSubalgebra.lean
theorem _root_.Subalgebra.topologicalClosure_star_comm (s : Subalgebra R A) :
    (star s).topologicalClosure = star s.topologicalClosure

Proof state:
R : Type u_1
A : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : StarRing A
inst✝² : StarModule R A
inst✝¹ : IsTopologicalSemiring A
inst✝ : ContinuousStar A
s : Subalgebra R A
⊢ ∀ (t : Subalgebra R A), (star t).topologicalClosure ≤ star t.topologicalClosure

Tactic:
exact fun t => (star t).topologicalClosure_minimal (Subalgebra.star_mono subset_closure)
  (isClosed_closure.preimage continuous_star)

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : StarRing A
inst✝² : StarModule R A
inst✝¹ : IsTopologicalSemiring A
inst✝ : ContinuousStar A
s : Subalgebra R A
⊢ (star s).topologicalClosure = star s.topologicalClosure

Tactic:
suffices ∀ t : Subalgebra R A, (star t).topologicalClosure ≤ star t.topologicalClosure from
  le_antisymm (this s) (by simpa only [star_star] using Subalgebra.star_mono (this (star s)))

Result:
R : Type u_1
A : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : StarRing A
inst✝² : StarModule R A
inst✝¹ : IsTopologicalSemiring A
inst✝ : ContinuousStar A
s : Subalgebra R A
⊢ ∀ (t : Subalgebra R A), (star t).topologicalClosure ≤ star t.topologicalClosure

Proof state:
R : Type u_1
A : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : StarRing A
inst✝² : StarModule R A
inst✝¹ : IsTopologicalSemiring A
inst✝ : ContinuousStar A
s : Subalgebra R A
this : ∀ (t : Subalgebra R A), (star t).topologicalClosure ≤ star t.topologicalClosure
⊢ star s.topologicalClosure ≤ (star s).topologicalClosure

Tactic:
simpa only [star_star] using Subalgebra.star_mono (this (star s))

Result:
no goals