harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesWithinOnBall.continuousWithinAt_insert
    (hf : HasFPowerSeriesWithinOnBall f p s x r) :
    ContinuousWithinAt f (insert x s) x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
⊢ x ∈ insert x s ∩ EMetric.ball x r

Tactic:
simp [hf.r_pos]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
⊢ insert x s ∩ EMetric.ball x r ∈ 𝓝[insert x s] x

Tactic:
exact inter_mem_nhdsWithin _ (EMetric.ball_mem_nhds x hf.r_pos)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
⊢ ContinuousWithinAt f (insert x s) x

Tactic:
apply (hf.continuousOn.continuousWithinAt (x := x) (by simp [hf.r_pos])).mono_of_mem_nhdsWithin

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
⊢ insert x s ∩ EMetric.ball x r ∈ 𝓝[insert x s] x
-- Mathlib/RingTheory/AdjoinRoot.lean
theorem algHom_subsingleton {S : Type*} [CommRing S] [Algebra R S] {r : R} :
    Subsingleton (AdjoinRoot (C r * X - 1) →ₐ[R] S) :=
  ⟨fun f g =>
    algHom_ext
      (@inv_unique _ _ (algebraMap R S r) _ _
        (by rw [← f.commutes, ← _root_.map_mul, algebraMap_eq, root_isInv, map_one])
        (by rw [← g.commutes, ← _root_.map_mul, algebraMap_eq, root_isInv, map_one]))⟩

Proof state:
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
f g : AdjoinRoot (C r * X - 1) →ₐ[R] S
⊢ (algebraMap R S) r * g (root (C r * X - 1)) = 1

Tactic:
rw [← g.commutes, ← _root_.map_mul, algebraMap_eq, root_isInv, map_one]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
f g : AdjoinRoot (C r * X - 1) →ₐ[R] S
⊢ (algebraMap R S) r * f (root (C r * X - 1)) = 1

Tactic:
rw [← f.commutes, ← _root_.map_mul, algebraMap_eq, root_isInv, map_one]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean
@[simp] lemma in₁₀_iff : (graph t).Adj (in₁ b) (in₀ a) ↔ ∃ c, (a, b, c) ∈ t :=
  ⟨by rintro ⟨⟩; exact ⟨_, ‹_›⟩, fun ⟨_, h⟩ ↦ in₁₀ h⟩

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
⊢ (graph t).Adj (in₁ b) (in₀ a) → ∃ c, (a, b, c) ∈ t

Tactic:
rintro ⟨⟩

Result:
case in₁₀
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c✝ : γ
a✝ : (a, b, c✝) ∈ t
⊢ ∃ c, (a, b, c) ∈ t

Proof state:
case in₁₀
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c✝ : γ
a✝ : (a, b, c✝) ∈ t
⊢ ∃ c, (a, b, c) ∈ t

Tactic:
exact ⟨_, ‹_›⟩

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiff_iff_continuous_differentiable {n : ℕ∞} :
    ContDiff 𝕜 n f ↔
      (∀ m : ℕ, m ≤ n → Continuous fun x => iteratedFDeriv 𝕜 m f x) ∧
        ∀ m : ℕ, m < n → Differentiable 𝕜 fun x => iteratedFDeriv 𝕜 m f x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞
⊢ ContDiff 𝕜 (↑n) f ↔
    (∀ (m : ℕ), ↑m ≤ n → Continuous fun x => iteratedFDeriv 𝕜 m f x) ∧
      ∀ (m : ℕ), ↑m < n → Differentiable 𝕜 fun x => iteratedFDeriv 𝕜 m f x

Tactic:
simp [contDiffOn_univ.symm, continuous_iff_continuousOn_univ, differentiableOn_univ.symm,
  iteratedFDerivWithin_univ, contDiffOn_iff_continuousOn_differentiableOn uniqueDiffOn_univ]

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_swap (f : α → β → γ) (s : Finset α) (t : Finset β) :
    image₂ f s t = image₂ (fun a b => f b a) t s :=
  coe_injective <| by
    push_cast
    exact image2_swap _ _ _

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ ↑(image₂ f s t) = ↑(image₂ (fun a b => f b a) t s)

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ image2 f ↑s ↑t = image2 (fun a b => f b a) ↑t ↑s

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ image2 f ↑s ↑t = image2 (fun a b => f b a) ↑t ↑s

Tactic:
exact image2_swap _ _ _

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Complex.lean
theorem volume_preserving_equiv_pi : MeasurePreserving measurableEquivPi

Proof state:
case h.e'_6

⊢ volume = Measure.map (⇑measurableEquivPi.symm) volume

Tactic:
rw [← addHaarMeasure_eq_volume_pi, ← Basis.parallelepiped_basisFun, ← Basis.addHaar,
  measurableEquivPi, Homeomorph.toMeasurableEquiv_symm_coe,
  ContinuousLinearEquiv.symm_toHomeomorph, ContinuousLinearEquiv.coe_toHomeomorph,
  Basis.map_addHaar, eq_comm]

Result:
case h.e'_6

⊢ ((Pi.basisFun ℝ (Fin 2)).map basisOneI.equivFun.toContinuousLinearEquiv.symm.toLinearEquiv).addHaar = volume

Proof state:
case h.e'_6

⊢ ((Pi.basisFun ℝ (Fin 2)).map basisOneI.equivFun.toContinuousLinearEquiv.symm.toLinearEquiv).addHaar = volume

Tactic:
exact (Basis.addHaar_eq_iff _ _).mpr Complex.orthonormalBasisOneI.volume_parallelepiped

Result:
no goals

Proof state:
⊢ MeasurePreserving (⇑measurableEquivPi) volume volume

Tactic:
convert (measurableEquivPi.symm.measurable.measurePreserving volume).symm

Result:
case h.e'_6

⊢ volume = Measure.map (⇑measurableEquivPi.symm) volume
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_union_add_mk_inter {α : Type u} {S T : Set α} :
    #(S ∪ T : Set α) + #(S ∩ T : Set α) = #S + #T

Proof state:
α : Type u
S T : Set α
⊢ #↑(S ∪ T) + #↑(S ∩ T) = #↑S + #↑T

Tactic:
classical
exact Quot.sound ⟨Equiv.Set.unionSumInter S T⟩

Result:
no goals

Proof state:
α : Type u
S T : Set α
⊢ #↑(S ∪ T) + #↑(S ∩ T) = #↑S + #↑T

Tactic:
exact Quot.sound ⟨Equiv.Set.unionSumInter S T⟩

Result:
no goals
-- Mathlib/Topology/Order/ScottTopology.lean
lemma dirSupInaccOn_of_isOpen [IsScottHausdorff α D] (h : IsOpen s) : DirSupInaccOn D s :=
  fun d hd₀ hd₁ hd₂ a hda hd₃ ↦ by
    obtain ⟨b, hbd, hb⟩ := isOpen_iff.mp h hd₀ hd₁ hd₂ hda hd₃; exact ⟨b, hbd, hb ⟨le_rfl, hbd⟩⟩

Proof state:
α : Type u_1
D : Set (Set α)
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScottHausdorff α D
h : IsOpen s
d : Set α
hd₀ : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
a : α
hda : IsLUB d a
hd₃ : a ∈ s
⊢ (d ∩ s).Nonempty

Tactic:
obtain ⟨b, hbd, hb⟩ := isOpen_iff.mp h hd₀ hd₁ hd₂ hda hd₃

Result:
case intro.intro
α : Type u_1
D : Set (Set α)
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScottHausdorff α D
h : IsOpen s
d : Set α
hd₀ : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
a : α
hda : IsLUB d a
hd₃ : a ∈ s
b : α
hbd : b ∈ d
hb : Ici b ∩ d ⊆ s
⊢ (d ∩ s).Nonempty

Proof state:
case intro.intro
α : Type u_1
D : Set (Set α)
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScottHausdorff α D
h : IsOpen s
d : Set α
hd₀ : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 => x1 ≤ x2) d
a : α
hda : IsLUB d a
hd₃ : a ∈ s
b : α
hbd : b ∈ d
hb : Ici b ∩ d ⊆ s
⊢ (d ∩ s).Nonempty

Tactic:
exact ⟨b, hbd, hb ⟨le_rfl, hbd⟩⟩

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem Indep.exists_insert_of_not_maximal (M : Matroid α) ⦃I B : Set α⦄ (hI : M.Indep I)
    (hInotmax : ¬ Maximal M.Indep I) (hB : Maximal M.Indep B) :
    ∃ x ∈ B \ I, M.Indep (insert x I)

Proof state:
case refine_2
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hB : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
hInotmax : ∃ x, M.Indep x ∧ I ⊆ x ∧ ¬I = x
⊢ M.IsBase B

Tactic:
exact hB.1.isBase_of_maximal fun J hJ hBJ ↦ hB.2 hJ hBJ

Result:
no goals

Proof state:
case refine_1
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hB : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
hInotmax : ∃ x, M.Indep x ∧ I ⊆ x ∧ ¬I = x
hIb : M.IsBase I
⊢ False

Tactic:
obtain ⟨I', hII', hI', hne⟩ := hInotmax

Result:
case refine_1.intro.intro.intro
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hB : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
hIb : M.IsBase I
I' : Set α
hII' : M.Indep I'
hI' : I ⊆ I'
hne : ¬I = I'
⊢ False

Proof state:
case refine_1.intro.intro.intro
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hB : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
hIb : M.IsBase I
I' : Set α
hII' : M.Indep I'
hI' : I ⊆ I'
hne : ¬I = I'
⊢ False

Tactic:
exact hne <| hIb.eq_of_subset_indep hII' hI'

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hInotmax : ¬Maximal M.Indep I
hB : Maximal M.Indep B
⊢ ∃ x ∈ B \ I, M.Indep (insert x I)

Tactic:
simp only [maximal_subset_iff, hI, not_and, not_forall, exists_prop, true_imp_iff] at hB hInotmax

Result:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hB : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
hInotmax : ∃ x, M.Indep x ∧ I ⊆ x ∧ ¬I = x
⊢ ∃ x ∈ B \ I, M.Indep (insert x I)

Proof state:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hB : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
hInotmax : ∃ x, M.Indep x ∧ I ⊆ x ∧ ¬I = x
⊢ ∃ x ∈ B \ I, M.Indep (insert x I)

Tactic:
refine hI.exists_insert_of_not_isBase (fun hIb ↦ ?_) ?_

Result:
case refine_1
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hB : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
hInotmax : ∃ x, M.Indep x ∧ I ⊆ x ∧ ¬I = x
hIb : M.IsBase I
⊢ False

case refine_2
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hB : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
hInotmax : ∃ x, M.Indep x ∧ I ⊆ x ∧ ¬I = x
⊢ M.IsBase B
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem exists_bucket' [BEq α] [Hashable α]
    (self : Array (AssocList α β)) (i : USize) (hi : i.toNat < self.size) :
      ∃ l, Perm (self.toList.flatMap AssocList.toList) (self[i.toNat].toList ++ l) ∧
        (∀ [LawfulHashable α], IsHashSelf self → ∀ k,
          (mkIdx self.size (by omega) (hash k)).1.toNat = i.toNat → containsKey k l = false)

Proof state:
case intro.intro.intro
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
self : Array (AssocList α β)
i : USize
hi : i.toNat < self.size
l : List ((a : α) × β a)
h₁ : (toListModel self).Perm (self[i.toNat].toList ++ l)
h₂ :
  ∀ [inst : LawfulHashable α],
    IsHashSelf self → ∀ (k : α), (mkIdx self.size ⋯ (hash k)).val.toNat = i.toNat → containsKey k l = false
⊢ ∃ l,
    (List.flatMap AssocList.toList self.toList).Perm (self[i.toNat].toList ++ l) ∧
      ∀ [inst : LawfulHashable α],
        IsHashSelf self → ∀ (k : α), (mkIdx self.size ⋯ (hash k)).val.toNat = i.toNat → containsKey k l = false

Tactic:
exact ⟨l, h₁, h₂⟩

Result:
no goals

Proof state:
α : Type u
β : α → Type v
γ : Type w
δ : α → Type w
inst✝² : BEq α
inst✝¹ : Hashable α
self : Array (AssocList α β)
i : USize
hi : i.toNat < self.size
l : List ((a : α) × β a)
inst✝ : LawfulHashable α
k : α
⊢ 0 < self.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
self : Array (AssocList α β)
i : USize
hi : i.toNat < self.size
⊢ ∃ l,
    (List.flatMap AssocList.toList self.toList).Perm (self[i.toNat].toList ++ l) ∧
      ∀ [inst : LawfulHashable α],
        IsHashSelf self → ∀ (k : α), (mkIdx self.size ⋯ (hash k)).val.toNat = i.toNat → containsKey k l = false

Tactic:
obtain ⟨l, h₁, -, h₂⟩ := exists_bucket_of_uset self i hi .nil

Result:
case intro.intro.intro
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
self : Array (AssocList α β)
i : USize
hi : i.toNat < self.size
l : List ((a : α) × β a)
h₁ : (toListModel self).Perm (self[i.toNat].toList ++ l)
h₂ :
  ∀ [inst : LawfulHashable α],
    IsHashSelf self → ∀ (k : α), (mkIdx self.size ⋯ (hash k)).val.toNat = i.toNat → containsKey k l = false
⊢ ∃ l,
    (List.flatMap AssocList.toList self.toList).Perm (self[i.toNat].toList ++ l) ∧
      ∀ [inst : LawfulHashable α],
        IsHashSelf self → ∀ (k : α), (mkIdx self.size ⋯ (hash k)).val.toNat = i.toNat → containsKey k l = false
-- Mathlib/Algebra/Homology/Bifunctor.lean
@[reassoc (attr := simp)]
lemma ι_D₁ :
    ιMapBifunctor K₁ K₂ F c i₁ i₂ j h ≫ D₁ K₁ K₂ F c j j' = d₁ K₁ K₂ F c i₁ i₂ j'

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝¹⁰ : Category.{u_9, u_1} C₁
inst✝⁹ : Category.{u_8, u_2} C₂
inst✝⁸ : Category.{u_7, u_3} D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst✝⁷ : HasZeroMorphisms C₁
inst✝⁶ : HasZeroMorphisms C₂
inst✝⁵ : Preadditive D
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
c : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : DecidableEq J
j j' : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
⊢ K₁.ιMapBifunctor K₂ F c i₁ i₂ j h ≫ D₁ K₁ K₂ F c j j' = d₁ K₁ K₂ F c i₁ i₂ j'

Tactic:
apply HomologicalComplex₂.ι_D₁

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem map_one_of_isMulOneCocycle {f : G → M} (hf : IsMulOneCocycle f) :
    f 1 = 1

Proof state:
G : Type u_1
M : Type u_2
inst✝² : Monoid G
inst✝¹ : CommGroup M
inst✝ : MulAction G M
f : G → M
hf : IsMulOneCocycle f
⊢ f 1 = 1

Tactic:
simpa only [mul_one, one_smul, self_eq_mul_right] using hf 1 1

Result:
no goals
-- Mathlib/Topology/Instances/NNReal/Lemmas.lean
theorem summable_comp_injective {β : Type*} {f : α → ℝ≥0} (hf : Summable f) {i : β → α}
    (hi : Function.Injective i) : Summable (f ∘ i)

Proof state:
α : Type u_1
β : Type u_2
f : α → ℝ≥0
hf : Summable fun a => ↑(f a)
i : β → α
hi : Function.Injective i
⊢ Summable fun a => ↑((f ∘ i) a)

Tactic:
exact hf.comp_injective hi

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → ℝ≥0
hf : Summable f
i : β → α
hi : Function.Injective i
⊢ Summable (f ∘ i)

Tactic:
rw [← summable_coe] at hf ⊢

Result:
α : Type u_1
β : Type u_2
f : α → ℝ≥0
hf : Summable fun a => ↑(f a)
i : β → α
hi : Function.Injective i
⊢ Summable fun a => ↑((f ∘ i) a)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/LinearCombo.lean
theorem smul_eval (lc : LinearCombo) (i : Int) (v : Coeffs) :
    (i * lc).eval v = i * lc.eval v

Proof state:
lc : LinearCombo
i : Int
v : Coeffs
⊢ (i * lc).eval v = i * lc.eval v

Tactic:
rcases lc with ⟨a, coeffs⟩

Result:
case mk
i : Int
v : Coeffs
a : Int
coeffs : Coeffs
⊢ (i * { const := a, coeffs := coeffs }).eval v = i * { const := a, coeffs := coeffs }.eval v

Proof state:
case mk
i : Int
v : Coeffs
a : Int
coeffs : Coeffs
⊢ (i * { const := a, coeffs := coeffs }).eval v = i * { const := a, coeffs := coeffs }.eval v

Tactic:
simp [eval, Int.mul_add]

Result:
no goals
-- Mathlib/RingTheory/LocalRing/Quotient.lean
lemma basisQuotient_apply [Fintype ι] (b : Basis ι R S) (i) :
    (basisQuotient b) i = Ideal.Quotient.mk pS (b i)

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : Free R S
ι : Type u_3
inst✝ : Fintype ι
b : Basis ι R S
i : ι
⊢ (basisQuotient b) i = (Ideal.Quotient.mk pS) (b i)

Tactic:
delta basisQuotient

Result:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : Free R S
ι : Type u_3
inst✝ : Fintype ι
b : Basis ι R S
i : ι
⊢ (basisOfTopLeSpanOfCardEqFinrank (⇑(Ideal.Quotient.mk pS) ∘ ⇑b) ⋯ ⋯) i = (Ideal.Quotient.mk pS) (b i)

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : Free R S
ι : Type u_3
inst✝ : Fintype ι
b : Basis ι R S
i : ι
⊢ (basisOfTopLeSpanOfCardEqFinrank (⇑(Ideal.Quotient.mk pS) ∘ ⇑b) ⋯ ⋯) i = (Ideal.Quotient.mk pS) (b i)

Tactic:
rw [coe_basisOfTopLeSpanOfCardEqFinrank, Function.comp_apply]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Content.lean
theorem normUnit_content {p : R[X]} : normUnit (content p) = 1

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ normUnit p.content = 1

Tactic:
by_cases hp0 : p.content = 0

Result:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp0 : p.content = 0
⊢ normUnit p.content = 1

case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp0 : ¬p.content = 0
⊢ normUnit p.content = 1

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp0 : ¬p.content = 0
⊢ normUnit p.content = 1

Tactic:
ext

Result:
case neg.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp0 : ¬p.content = 0
⊢ ↑(normUnit p.content) = ↑1

Proof state:
case pos
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp0 : p.content = 0
⊢ normUnit p.content = 1

Tactic:
simp [hp0]

Result:
no goals

Proof state:
case neg.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp0 : ¬p.content = 0
⊢ ↑(normUnit p.content) = ↑1

Tactic:
apply mul_left_cancel₀ hp0

Result:
case neg.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp0 : ¬p.content = 0
⊢ p.content * ↑(normUnit p.content) = p.content * ↑1

Proof state:
case neg.a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp0 : ¬p.content = 0
⊢ p.content * ↑(normUnit p.content) = p.content * ↑1

Tactic:
erw [← normalize_apply, normalize_content, mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Lemmas.lean
theorem mkConst_le_size (aig : AIG α) (val : Bool) :
    aig.decls.size ≤ (aig.mkConst val).aig.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
⊢ aig.decls.size ≤ (aig.mkConst val).aig.decls.size

Tactic:
simp_arith [mkConst]

Result:
no goals
-- Mathlib/RingTheory/Algebraic/MvPolynomial.lean
theorem transcendental_supported_X_iff [Nontrivial R] {i : σ} {s : Set σ} :
    Transcendental (supported R s) (X i : MvPolynomial σ R) ↔ i ∉ s

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
⊢ Transcendental (↥(supported R s)) (X i) ↔ i ∉ s

Tactic:
simpa [Polynomial.transcendental_X] using
  transcendental_supported_polynomial_aeval_X_iff R (i := i) (s := s) (f := Polynomial.X)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
theorem inv_cpow_eq_ite' (x : ℂ) (n : ℂ) :
    (x ^ n)⁻¹ = if x.arg = π then conj (x⁻¹ ^ conj n) else x⁻¹ ^ n

Proof state:
case neg
x n : ℂ
h : ¬x.arg = π
⊢ (x ^ n)⁻¹ = x⁻¹ ^ n

Tactic:
rw [inv_cpow _ _ h]

Result:
no goals

Proof state:
case pos
x n : ℂ
h : x.arg = π
⊢ (x ^ n)⁻¹ = (x ^ n)⁻¹

Tactic:
rfl

Result:
no goals

Proof state:
x n : ℂ
⊢ (x ^ n)⁻¹ = if x.arg = π then (starRingEnd ℂ) (x⁻¹ ^ (starRingEnd ℂ) n) else x⁻¹ ^ n

Tactic:
rw [inv_cpow_eq_ite, apply_ite conj, conj_conj, conj_conj]

Result:
x n : ℂ
⊢ (x ^ n)⁻¹ = if x.arg = π then if x.arg = π then (x ^ n)⁻¹ else (starRingEnd ℂ) (x ^ (starRingEnd ℂ) n)⁻¹ else x⁻¹ ^ n

Proof state:
x n : ℂ
⊢ (x ^ n)⁻¹ = if x.arg = π then if x.arg = π then (x ^ n)⁻¹ else (starRingEnd ℂ) (x ^ (starRingEnd ℂ) n)⁻¹ else x⁻¹ ^ n

Tactic:
split_ifs with h

Result:
case pos
x n : ℂ
h : x.arg = π
⊢ (x ^ n)⁻¹ = (x ^ n)⁻¹

case neg
x n : ℂ
h : ¬x.arg = π
⊢ (x ^ n)⁻¹ = x⁻¹ ^ n
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
theorem map_update_sum {α : Type*} [DecidableEq ι] (t : Finset α) (i : ι) (g : α → M₁ i)
    (m : ∀ i, M₁ i) : f (update m i (∑ a ∈ t, g a)) = ∑ a ∈ t, f (update m i (g a))

Proof state:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
α : Type u_2
inst✝ : DecidableEq ι
t : Finset α
i : ι
g : α → M₁ i
m : (i : ι) → M₁ i
⊢ f (update m i (∑ a ∈ t, g a)) = ∑ a ∈ t, f (update m i (g a))

Tactic:
induction t using Finset.induction with
| empty => simp
| insert has ih => simp [Finset.sum_insert has, ih]

Result:
no goals

Proof state:
case insert
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
α : Type u_2
inst✝ : DecidableEq ι
i : ι
g : α → M₁ i
m : (i : ι) → M₁ i
a✝ : α
s✝ : Finset α
has : a✝ ∉ s✝
ih : f (update m i (∑ a ∈ s✝, g a)) = ∑ a ∈ s✝, f (update m i (g a))
⊢ f (update m i (∑ a ∈ insert a✝ s✝, g a)) = ∑ a ∈ insert a✝ s✝, f (update m i (g a))

Tactic:
simp [Finset.sum_insert has, ih]

Result:
no goals

Proof state:
case empty
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
α : Type u_2
inst✝ : DecidableEq ι
i : ι
g : α → M₁ i
m : (i : ι) → M₁ i
⊢ f (update m i (∑ a ∈ ∅, g a)) = ∑ a ∈ ∅, f (update m i (g a))

Tactic:
simp

Result:
no goals

Proof state:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
α : Type u_2
inst✝ : DecidableEq ι
t : Finset α
i : ι
g : α → M₁ i
m : (i : ι) → M₁ i
⊢ f (update m i (∑ a ∈ t, g a)) = ∑ a ∈ t, f (update m i (g a))

Tactic:
classical
  induction t using Finset.induction with
  | empty => simp
  | insert has ih => simp [Finset.sum_insert has, ih]

Result:
no goals
-- Mathlib/Analysis/Convex/Topology.lean
theorem Convex.combo_self_interior_subset_interior {s : Set E} (hs : Convex 𝕜 s) {a b : 𝕜}
    (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) : a • s + b • interior s ⊆ interior s

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
⊢ a • s + b • interior s ⊆ interior s

Tactic:
rw [add_comm]

Result:
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
⊢ b • interior s + a • s ⊆ interior s

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
⊢ b • interior s + a • s ⊆ interior s

Tactic:
exact hs.combo_interior_self_subset_interior hb ha (add_comm a b ▸ hab)

Result:
no goals