harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem measure_diff_lt_of_lt_add (hs : NullMeasurableSet s μ) (hst : s ⊆ t) (hs' : μ s ≠ ∞)
    {ε : ℝ≥0∞} (h : μ t < μ s + ε) : μ (t \ s) < ε

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
hst : s ⊆ t
hs' : μ s ≠ ⊤
ε : ℝ≥0∞
h : μ t < μ s + ε
⊢ μ (t \ s) < ε

Tactic:
rw [measure_diff hst hs hs']

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
hst : s ⊆ t
hs' : μ s ≠ ⊤
ε : ℝ≥0∞
h : μ t < μ s + ε
⊢ μ t - μ s < ε

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
hst : s ⊆ t
hs' : μ s ≠ ⊤
ε : ℝ≥0∞
h : μ t < μ s + ε
⊢ μ t - μ s < ε

Tactic:
rw [add_comm] at h

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
hst : s ⊆ t
hs' : μ s ≠ ⊤
ε : ℝ≥0∞
h : μ t < ε + μ s
⊢ μ t - μ s < ε

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
hst : s ⊆ t
hs' : μ s ≠ ⊤
ε : ℝ≥0∞
h : μ t < ε + μ s
⊢ μ t - μ s < ε

Tactic:
exact ENNReal.sub_lt_of_lt_add (measure_mono hst) h

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
@[simp] lemma zero_le' : 0 ≤ a

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommMonoidWithZero α
a : α
⊢ 0 ≤ a

Tactic:
simpa only [mul_zero, mul_one] using mul_le_mul_left' (zero_le_one' α) a

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem isRat_rpow_pos {a b : ℝ} {nb : ℕ}
    {num : ℤ} {den : ℕ}
    (pb : IsNat b nb) (pe' : IsRat (a ^ nb) num den) :
    IsRat (a ^ b) num den

Proof state:
a b : ℝ
nb : ℕ
num : ℤ
den : ℕ
pb : IsNat b nb
pe' : IsRat (a ^ nb) num den
⊢ IsRat (a ^ b) num den

Tactic:
rwa [pb.out, rpow_natCast]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem rotate_perm (l : List α) (n : ℕ) : l.rotate n ~ l

Proof state:
case succ
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
l : List α
⊢ l.rotate' (n + 1) ~ l

Tactic:
rcases l with - | ⟨hd, tl⟩

Result:
case succ.nil
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
⊢ [].rotate' (n + 1) ~ []

case succ.cons
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
hd : α
tl : List α
⊢ (hd :: tl).rotate' (n + 1) ~ hd :: tl

Proof state:
case zero
α : Type u
l : List α
⊢ l.rotate' 0 ~ l

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
l : List α
n : ℕ
⊢ l.rotate' n ~ l

Tactic:
induction' n with n hn generalizing l

Result:
case zero
α : Type u
l : List α
⊢ l.rotate' 0 ~ l

case succ
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
l : List α
⊢ l.rotate' (n + 1) ~ l

Proof state:
case succ.nil
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
⊢ [].rotate' (n + 1) ~ []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
l : List α
n : ℕ
⊢ l.rotate n ~ l

Tactic:
rw [rotate_eq_rotate']

Result:
α : Type u
l : List α
n : ℕ
⊢ l.rotate' n ~ l

Proof state:
case succ.cons
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
hd : α
tl : List α
⊢ (tl ++ [hd]).rotate' n ~ hd :: tl

Tactic:
exact (hn _).trans (perm_append_singleton _ _)

Result:
no goals

Proof state:
case succ.cons
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
hd : α
tl : List α
⊢ (hd :: tl).rotate' (n + 1) ~ hd :: tl

Tactic:
rw [rotate'_cons_succ]

Result:
case succ.cons
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
hd : α
tl : List α
⊢ (tl ++ [hd]).rotate' n ~ hd :: tl
-- Mathlib/Probability/Kernel/Disintegration/Unique.lean
lemma condKernel_const [CountableOrCountablyGenerated α β] (ρ : Measure (β × Ω)) [IsFiniteMeasure ρ]
    (a : α) :
    (fun b ↦ Kernel.condKernel (Kernel.const α ρ) (a, b)) =ᵐ[ρ.fst] ρ.condKernel

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
a : α
⊢ (fun b => (Kernel.const α ρ).condKernel (a, b)) =ᶠ[ae ρ.fst] ⇑ρ.condKernel

Tactic:
have h := Kernel.condKernel_apply_eq_condKernel (Kernel.const α ρ) a

Result:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
a : α
h : (fun b => (Kernel.const α ρ).condKernel (a, b)) =ᶠ[ae ((Kernel.const α ρ).fst a)] ⇑((Kernel.const α ρ) a).condKernel
⊢ (fun b => (Kernel.const α ρ).condKernel (a, b)) =ᶠ[ae ρ.fst] ⇑ρ.condKernel

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
a : α
h : (fun b => (Kernel.const α ρ).condKernel (a, b)) =ᶠ[ae (Measure.map Prod.fst ρ)] ⇑ρ.condKernel
⊢ (fun b => (Kernel.const α ρ).condKernel (a, b)) =ᶠ[ae ρ.fst] ⇑ρ.condKernel

Tactic:
filter_upwards [h] with b hb using hb

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
a : α
h : (fun b => (Kernel.const α ρ).condKernel (a, b)) =ᶠ[ae ((Kernel.const α ρ).fst a)] ⇑((Kernel.const α ρ) a).condKernel
⊢ (fun b => (Kernel.const α ρ).condKernel (a, b)) =ᶠ[ae ρ.fst] ⇑ρ.condKernel

Tactic:
simp_rw [Kernel.fst_apply, Kernel.const_apply] at h

Result:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
a : α
h : (fun b => (Kernel.const α ρ).condKernel (a, b)) =ᶠ[ae (Measure.map Prod.fst ρ)] ⇑ρ.condKernel
⊢ (fun b => (Kernel.const α ρ).condKernel (a, b)) =ᶠ[ae ρ.fst] ⇑ρ.condKernel
-- Mathlib/Algebra/Polynomial/GroupRingAction.lean
theorem prodXSubSMul.coeff (x : R) (g : G) (n : ℕ) :
    g • (prodXSubSMul G R x).coeff n = (prodXSubSMul G R x).coeff n

Proof state:
G : Type u_2
inst✝³ : Group G
inst✝² : Fintype G
R : Type u_3
inst✝¹ : CommRing R
inst✝ : MulSemiringAction G R
x : R
g : G
n : ℕ
⊢ g • (prodXSubSMul G R x).coeff n = (prodXSubSMul G R x).coeff n

Tactic:
rw [← Polynomial.coeff_smul, prodXSubSMul.smul]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/AffineMap.lean
theorem hasStrictDerivAt : HasStrictDerivAt f (f.linear 1) x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
x : 𝕜
⊢ HasStrictDerivAt (⇑f.linear + fun x => f 0) (f.linear 1) x

Tactic:
exact f.linear.hasStrictDerivAt.add_const (f 0)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
x : 𝕜
⊢ HasStrictDerivAt (⇑f) (f.linear 1) x

Tactic:
rw [f.decomp]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
x : 𝕜
⊢ HasStrictDerivAt (⇑f.linear + fun x => f 0) (f.linear 1) x
-- Mathlib/Data/Stream/Init.lean
theorem interleave_tail_tail (s₁ s₂ : Stream' α) : tail s₁ ⋈ tail s₂ = tail (tail (s₁ ⋈ s₂))

Proof state:
α : Type u
s₁ s₂ : Stream' α
⊢ s₁.tail ⋈ s₂.tail = (s₁ ⋈ s₂).tail.tail

Tactic:
rw [interleave_eq s₁ s₂]

Result:
α : Type u
s₁ s₂ : Stream' α
⊢ s₁.tail ⋈ s₂.tail = (s₁.head :: s₂.head :: (s₁.tail ⋈ s₂.tail)).tail.tail

Proof state:
α : Type u
s₁ s₂ : Stream' α
⊢ s₁.tail ⋈ s₂.tail = (s₁.head :: s₂.head :: (s₁.tail ⋈ s₂.tail)).tail.tail

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
theorem toNNReal_pos {r : ℝ} : 0 < Real.toNNReal r ↔ 0 < r

Proof state:
r : ℝ
⊢ 0 < r.toNNReal ↔ 0 < r

Tactic:
simp [← NNReal.coe_lt_coe, lt_irrefl]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean
theorem measurable_comp_iff (hg : MeasurableEmbedding g) : Measurable (g ∘ f) ↔ Measurable f

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
H : Measurable (g ∘ f)
⊢ Measurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f)

Tactic:
exact hg.measurable_rangeSplitting.comp H.subtype_mk

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
H : Measurable (g ∘ f)
this : Measurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f)
⊢ Measurable f

Tactic:
rwa [(rightInverse_rangeSplitting hg.injective).comp_eq_id] at this

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
H : Measurable (g ∘ f)
⊢ Measurable f

Tactic:
suffices Measurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f) by
  rwa [(rightInverse_rangeSplitting hg.injective).comp_eq_id] at this

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
H : Measurable (g ∘ f)
⊢ Measurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
⊢ Measurable (g ∘ f) ↔ Measurable f

Tactic:
refine ⟨fun H => ?_, hg.measurable.comp⟩

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
H : Measurable (g ∘ f)
⊢ Measurable f
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Gcd.lean
theorem Coprime.dvd_of_dvd_mul_left (H1 : Coprime k m) (H2 : k ∣ m * n) : k ∣ n :=
  H1.dvd_of_dvd_mul_right (by rwa [Nat.mul_comm])

Proof state:
k m n : Nat
H1 : k.Coprime m
H2 : k ∣ m * n
⊢ k ∣ n * m

Tactic:
rwa [Nat.mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Impl.lean
theorem modifyTR_go_eq : ∀ l n, modifyTR.go f l n acc = acc.toList ++ modify f n l
  | [], n => by cases n <;> simp [modifyTR.go, modify]
  | a :: l, 0 => by simp [modifyTR.go, modify]
  | a :: l, n+1 => by simp [modifyTR.go, modify, modifyTR_go_eq l]

Proof state:
α✝ : Type u_1
f : α✝ → α✝
acc : Array α✝
a : α✝
l : List α✝
⊢ modifyTR.go f (a :: l) 0 acc = acc.toList ++ modify f 0 (a :: l)

Tactic:
simp [modifyTR.go, modify]

Result:
no goals

Proof state:
α✝ : Type u_1
f : α✝ → α✝
acc : Array α✝
a : α✝
l : List α✝
n : Nat
⊢ modifyTR.go f (a :: l) (n + 1) acc = acc.toList ++ modify f (n + 1) (a :: l)

Tactic:
simp [modifyTR.go, modify, modifyTR_go_eq l]

Result:
no goals

Proof state:
α✝ : Type u_1
f : α✝ → α✝
acc : Array α✝
n : Nat
⊢ modifyTR.go f [] n acc = acc.toList ++ modify f n []

Tactic:
cases n <;> simp [modifyTR.go, modify]

Result:
no goals
-- Mathlib/Probability/CondVar.lean
@[simp] lemma condVar_zero : Var[0; μ | m] = 0

Proof state:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
⊢ Var[0; μ | m] = 0

Tactic:
simp [condVar]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Module/Defs.lean
lemma norm_zero_iff (x : E) : ‖x‖ = 0 ↔ x = 0 :=
  ⟨fun h => by simpa [norm_eq_sqrt_norm_inner_self, inner_self] using h,
    fun h => by simp [norm, h, norm_eq_sqrt_norm_inner_self]⟩

Proof state:
A : Type u_1
E : Type u_2
inst✝⁶ : NonUnitalCStarAlgebra A
inst✝⁵ : PartialOrder A
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℂ E
inst✝² : SMul Aᵐᵒᵖ E
inst✝¹ : Norm E
inst✝ : CStarModule A E
x : E
h : x = 0
⊢ ‖x‖ = 0

Tactic:
simp [norm, h, norm_eq_sqrt_norm_inner_self]

Result:
no goals

Proof state:
A : Type u_1
E : Type u_2
inst✝⁶ : NonUnitalCStarAlgebra A
inst✝⁵ : PartialOrder A
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℂ E
inst✝² : SMul Aᵐᵒᵖ E
inst✝¹ : Norm E
inst✝ : CStarModule A E
x : E
h : ‖x‖ = 0
⊢ x = 0

Tactic:
simpa [norm_eq_sqrt_norm_inner_self, inner_self] using h

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem coe_le_iff (n : ℕ) (x : PartENat) : (n : PartENat) ≤ x ↔ ∀ h : x.Dom, n ≤ x.get h

Proof state:
n : ℕ
x : PartENat
⊢ ↑n ≤ x ↔ ∀ (h : x.Dom), n ≤ x.get h

Tactic:
simp only [le_def, exists_prop_of_true, dom_some, forall_true_iff]

Result:
n : ℕ
x : PartENat
⊢ (∀ (hy : x.Dom), (↑n).get ⋯ ≤ x.get hy) ↔ ∀ (h : x.Dom), n ≤ x.get h

Proof state:
n : ℕ
x : PartENat
⊢ (∀ (hy : x.Dom), (↑n).get ⋯ ≤ x.get hy) ↔ ∀ (h : x.Dom), n ≤ x.get h

Tactic:
rfl

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem sInter_empty : ⋂₀ (∅ : ZFSet) = ∅

Proof state:
⊢ ⋂₀ ∅ = ∅

Tactic:
simp [sInter]

Result:
no goals
-- Mathlib/Algebra/Category/Ring/Epi.lean
lemma RingHom.surjective_of_epi_of_finite {R S : CommRingCat} (f : R ⟶ S) [Epi f]
    (h₂ : RingHom.Finite f.hom) : Function.Surjective f

Proof state:
case h₁
R S : CommRingCat
f : R ⟶ S
inst✝ : Epi f
h₂ : (CommRingCat.Hom.hom f).Finite
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
algebraizeInst✝ : Module.Finite ↑R ↑S
⊢ ∀ (s : ↑S), s ⊗ₜ[↑R] 1 = 1 ⊗ₜ[↑R] s

Tactic:
rwa [← CommRingCat.epi_iff_tmul_eq_tmul]

Result:
no goals

Proof state:
R S : CommRingCat
f : R ⟶ S
inst✝ : Epi f
h₂ : (CommRingCat.Hom.hom f).Finite
⊢ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
algebraize [f.hom]

Result:
R S : CommRingCat
f : R ⟶ S
inst✝ : Epi f
h₂ : (CommRingCat.Hom.hom f).Finite
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
algebraizeInst✝ : Module.Finite ↑R ↑S
⊢ Function.Surjective ⇑(ConcreteCategory.hom f)

Proof state:
R S : CommRingCat
f : R ⟶ S
inst✝ : Epi f
h₂ : (CommRingCat.Hom.hom f).Finite
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
algebraizeInst✝ : Module.Finite ↑R ↑S
⊢ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
apply RingHom.surjective_of_tmul_eq_tmul_of_finite

Result:
case h₁
R S : CommRingCat
f : R ⟶ S
inst✝ : Epi f
h₂ : (CommRingCat.Hom.hom f).Finite
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
algebraizeInst✝ : Module.Finite ↑R ↑S
⊢ ∀ (s : ↑S), s ⊗ₜ[↑R] 1 = 1 ⊗ₜ[↑R] s
-- Mathlib/Data/Stream/Init.lean
theorem tails_eq (s : Stream' α) : tails s = tail s::tails (tail s)

Proof state:
α : Type u
s : Stream' α
⊢ id s.tail :: corec id tail s.tail.tail = s.tail :: corec id tail s.tail.tail

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
s : Stream' α
⊢ corec id tail s.tail = s.tail :: corec id tail s.tail.tail

Tactic:
rw [corec_eq]

Result:
α : Type u
s : Stream' α
⊢ id s.tail :: corec id tail s.tail.tail = s.tail :: corec id tail s.tail.tail

Proof state:
α : Type u
s : Stream' α
⊢ s.tails = s.tail :: s.tail.tails

Tactic:
unfold tails

Result:
α : Type u
s : Stream' α
⊢ corec id tail s.tail = s.tail :: corec id tail s.tail.tail
-- Mathlib/Order/Filter/EventuallyConst.lean
theorem eventuallyConst_pred' {p : α → Prop} :
    EventuallyConst p l ↔ (p =ᶠ[l] fun _ ↦ False) ∨ (p =ᶠ[l] fun _ ↦ True)

Proof state:
α : Type u_1
l : Filter α
p : α → Prop
⊢ EventuallyConst p l ↔ (p =ᶠ[l] fun x => False) ∨ p =ᶠ[l] fun x => True

Tactic:
simp only [eventuallyConst_iff_exists_eventuallyEq, Prop.exists_iff]

Result:
no goals
-- Mathlib/RingTheory/FiniteType.lean
theorem polynomial : FiniteType R R[X] :=
  ⟨⟨{Polynomial.X}, by
      rw [Finset.coe_singleton]
      exact Polynomial.adjoin_X⟩⟩

Proof state:
R : Type uR
inst✝ : CommSemiring R
⊢ adjoin R {X} = ⊤

Tactic:
exact Polynomial.adjoin_X

Result:
no goals

Proof state:
R : Type uR
inst✝ : CommSemiring R
⊢ adjoin R ↑{X} = ⊤

Tactic:
rw [Finset.coe_singleton]

Result:
R : Type uR
inst✝ : CommSemiring R
⊢ adjoin R {X} = ⊤
-- Mathlib/GroupTheory/OreLocalization/Basic.lean
theorem universalMulHom_commutes {r : R} : universalMulHom f fS hf (numeratorHom r) = f r

Proof state:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r : R
⊢ (universalMulHom f fS hf) (numeratorHom r) = f r

Tactic:
simp [numeratorHom_apply, universalMulHom_apply]

Result:
no goals
-- Mathlib/Algebra/Ring/Center.lean
theorem neg_mem_center [NonUnitalNonAssocRing M] {a : M} (ha : a ∈ Set.center M) :
    -a ∈ Set.center M where
  comm _

Proof state:
M : Type u_1
inst✝ : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x✝¹ x✝ : M
⊢ x✝¹ * -a * x✝ = x✝¹ * (-a * x✝)

Tactic:
rw [← neg_mul_comm, ha.mid_assoc, neg_mul_comm, neg_mul]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x✝ : M
⊢ -a * x✝ = x✝ * -a

Tactic:
rw [← neg_mul_comm, ← ha.comm, neg_mul_comm]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x✝¹ x✝ : M
⊢ x✝¹ * x✝ * -a = x✝¹ * (x✝ * -a)

Tactic:
rw [mul_neg, ha.right_assoc, mul_neg, mul_neg]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : NonUnitalNonAssocRing M
a : M
ha : a ∈ center M
x✝¹ x✝ : M
⊢ -a * (x✝¹ * x✝) = -a * x✝¹ * x✝

Tactic:
rw [neg_mul, ha.left_assoc, neg_mul, neg_mul]

Result:
no goals
-- Mathlib/Combinatorics/Colex.lean
lemma mem_initSeg_self : s ∈ initSeg s

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
⊢ s ∈ initSeg s

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma equation_zero : W'.Equation ![1, 1, 0]

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
⊢ W'.Equation ![1, 1, 0]

Tactic:
simp only [equation_of_Z_eq_zero, fin3_def_ext, one_pow]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem eq_univ_of_subsingleton_span_eq_top {s : Set P} (h₁ : s.Subsingleton)
    (h₂ : affineSpan k s = ⊤) : s = (univ : Set P)

Proof state:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
this : s = {p}
⊢ Subsingleton P

Tactic:
exact subsingleton_of_subsingleton_span_eq_top h₁ h₂

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
⊢ {p} ⊆ s

Tactic:
simp [hp]

Result:
no goals

Proof state:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
⊢ s = univ

Tactic:
have : s = {p} := Subset.antisymm (fun q hq => h₁ hq hp) (by simp [hp])

Result:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
this : s = {p}
⊢ s = univ

Proof state:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
this : s = {p}
⊢ s = univ

Tactic:
rw [this, eq_comm, ← subsingleton_iff_singleton (mem_univ p), subsingleton_univ_iff]

Result:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
this : s = {p}
⊢ Subsingleton P

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
h₂ : affineSpan k s = ⊤
⊢ s = univ

Tactic:
obtain ⟨p, hp⟩ := AffineSubspace.nonempty_of_affineSpan_eq_top k V P h₂

Result:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : Set P
h₁ : s.Subsingleton
h₂ : affineSpan k s = ⊤
p : P
hp : p ∈ s
⊢ s = univ
-- Mathlib/Data/Finset/Sort.lean
theorem orderEmbOfFin_eq_orderEmbOfFin_iff {k l : ℕ} {s : Finset α} {i : Fin k} {j : Fin l}
    {h : s.card = k} {h' : s.card = l} :
    s.orderEmbOfFin h i = s.orderEmbOfFin h' j ↔ (i : ℕ) = (j : ℕ)

Proof state:
α : Type u_1
inst✝ : LinearOrder α
k l : ℕ
s : Finset α
i : Fin k
j : Fin l
h : #s = k
h' : #s = l
⊢ (s.orderEmbOfFin h) i = (s.orderEmbOfFin h') j ↔ ↑i = ↑j

Tactic:
substs k l

Result:
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
i j : Fin #s
⊢ (s.orderEmbOfFin ⋯) i = (s.orderEmbOfFin ⋯) j ↔ ↑i = ↑j

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
i j : Fin #s
⊢ (s.orderEmbOfFin ⋯) i = (s.orderEmbOfFin ⋯) j ↔ ↑i = ↑j

Tactic:
exact (s.orderEmbOfFin rfl).eq_iff_eq.trans Fin.ext_iff

Result:
no goals
-- Mathlib/Data/Finset/Interval.lean
theorem card_Icc_finset (h : s ⊆ t) : (Icc s t).card = 2 ^ (t.card - s.card)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
hu : u ∈ ↑(t \ s).powerset
v : Finset α
hv : v ∈ ↑(t \ s).powerset
huv : s ⊔ u = s ⊔ v
⊢ u = v

Tactic:
rw [mem_coe, mem_powerset] at hu hv

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
hu : u ⊆ t \ s
v : Finset α
hv : v ⊆ t \ s
huv : s ⊔ u = s ⊔ v
⊢ u = v

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ Set.InjOn (fun x => s ∪ x) ↑(t \ s).powerset

Tactic:
rintro u hu v hv (huv : s ⊔ u = s ⊔ v)

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
hu : u ∈ ↑(t \ s).powerset
v : Finset α
hv : v ∈ ↑(t \ s).powerset
huv : s ⊔ u = s ⊔ v
⊢ u = v

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ #(Icc s t) = 2 ^ (#t - #s)

Tactic:
rw [← card_sdiff h, ← card_powerset, Icc_eq_image_powerset h, Finset.card_image_iff]

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ Set.InjOn (fun x => s ∪ x) ↑(t \ s).powerset

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
hu : u ⊆ t \ s
v : Finset α
hv : v ⊆ t \ s
huv : s ⊔ u = s ⊔ v
⊢ u = v

Tactic:
rw [← (disjoint_sdiff.mono_right hu : Disjoint s u).sup_sdiff_cancel_left, ←
  (disjoint_sdiff.mono_right hv : Disjoint s v).sup_sdiff_cancel_left, huv]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem collinear_singleton (p : P) : Collinear k ({p} : Set P)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
⊢ Module.rank k ↥⊥ ≤ 1

Tactic:
simp

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
⊢ Collinear k {p}

Tactic:
rw [collinear_iff_rank_le_one, vectorSpan_singleton]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
⊢ Module.rank k ↥⊥ ≤ 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem countP_flatten (l : Vector (Vector α m) n) :
    countP p l.flatten = (l.map (countP p)).sum

Proof state:
α : Type u_1
p : α → Bool
m n : Nat
l : Vector (Vector α m) n
⊢ countP p l.flatten = (map (countP p) l).sum

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
p : α → Bool
m : Nat
l : Array (Vector α m)
⊢ countP p { toArray := l, size_toArray := ⋯ }.flatten = (map (countP p) { toArray := l, size_toArray := ⋯ }).sum

Proof state:
case mk
α : Type u_1
p : α → Bool
m : Nat
l : Array (Vector α m)
⊢ countP p { toArray := l, size_toArray := ⋯ }.flatten = (map (countP p) { toArray := l, size_toArray := ⋯ }).sum

Tactic:
simp [Function.comp_def]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem top_rpow_of_neg {y : ℝ} (h : y < 0) : (⊤ : ℝ≥0∞) ^ y = 0

Proof state:
y : ℝ
h : y < 0
⊢ ⊤ ^ y = 0

Tactic:
simp [top_rpow_def, asymm h, ne_of_lt h]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem Ico_insert_succ_left (h : a < b) : insert a (Ico a.succ b) = Ico a b

Proof state:
a b : ℕ
h : a < b
⊢ insert a (Ico a.succ b) = Ico a b

Tactic:
rw [Ico_succ_left, ← Ioo_insert_left h]

Result:
no goals