harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Icc_subset_Icc_iff (h₁ : a₁ ≤ b₁) : Icc a₁ b₁ ⊆ Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Proof state:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ Icc a₁ b₁ ⊆ Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Tactic:
rw [← coe_subset, coe_Icc, coe_Icc, Set.Icc_subset_Icc_iff h₁]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem lt_univ {c} : c < univ.{u, u + 1} ↔ ∃ c', c = lift.{u + 1, u} c' :=
  ⟨fun h => by
    have := ord_lt_ord.2 h
    rw [ord_univ] at this
    obtain ⟨o, e⟩ := liftPrincipalSeg.mem_range_of_rel_top (by simpa only [liftPrincipalSeg_top])
    have := card_ord c
    rw [← e, liftPrincipalSeg_coe, ← lift_card] at this
    exact ⟨_, this.symm⟩, fun ⟨_, e⟩ => e.symm ▸ lift_lt_univ _⟩

Proof state:
case intro
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this : c.ord < Ordinal.univ.{u, u + 1}
o : Ordinal.{u}
e : liftPrincipalSeg.toRelEmbedding o = c.ord
⊢ ∃ c', c = lift.{u + 1, u} c'

Tactic:
have := card_ord c

Result:
case intro
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this✝ : c.ord < Ordinal.univ.{u, u + 1}
o : Ordinal.{u}
e : liftPrincipalSeg.toRelEmbedding o = c.ord
this : c.ord.card = c
⊢ ∃ c', c = lift.{u + 1, u} c'

Proof state:
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this : c.ord < univ.{u, u + 1}.ord
⊢ ∃ c', c = lift.{u + 1, u} c'

Tactic:
rw [ord_univ] at this

Result:
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this : c.ord < Ordinal.univ.{u, u + 1}
⊢ ∃ c', c = lift.{u + 1, u} c'

Proof state:
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this : c.ord < Ordinal.univ.{u, u + 1}
⊢ ∃ c', c = lift.{u + 1, u} c'

Tactic:
obtain ⟨o, e⟩ := liftPrincipalSeg.mem_range_of_rel_top (by simpa only [liftPrincipalSeg_top])

Result:
case intro
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this : c.ord < Ordinal.univ.{u, u + 1}
o : Ordinal.{u}
e : liftPrincipalSeg.toRelEmbedding o = c.ord
⊢ ∃ c', c = lift.{u + 1, u} c'

Proof state:
case intro
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this✝ : c.ord < Ordinal.univ.{u, u + 1}
o : Ordinal.{u}
e : liftPrincipalSeg.toRelEmbedding o = c.ord
this : c.ord.card = c
⊢ ∃ c', c = lift.{u + 1, u} c'

Tactic:
rw [← e, liftPrincipalSeg_coe, ← lift_card] at this

Result:
case intro
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this✝ : c.ord < Ordinal.univ.{u, u + 1}
o : Ordinal.{u}
e : liftPrincipalSeg.toRelEmbedding o = c.ord
this : lift.{u + 1, u} o.card = c
⊢ ∃ c', c = lift.{u + 1, u} c'

Proof state:
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this : c.ord < Ordinal.univ.{u, u + 1}
⊢ ?m.167745 < liftPrincipalSeg.top

Tactic:
simpa only [liftPrincipalSeg_top]

Result:
no goals

Proof state:
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
⊢ ∃ c', c = lift.{u + 1, u} c'

Tactic:
have := ord_lt_ord.2 h

Result:
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this : c.ord < univ.{u, u + 1}.ord
⊢ ∃ c', c = lift.{u + 1, u} c'

Proof state:
case intro
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this✝ : c.ord < Ordinal.univ.{u, u + 1}
o : Ordinal.{u}
e : liftPrincipalSeg.toRelEmbedding o = c.ord
this : lift.{u + 1, u} o.card = c
⊢ ∃ c', c = lift.{u + 1, u} c'

Tactic:
exact ⟨_, this.symm⟩

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean
theorem contDiffOn_log {n : WithTop ℕ∞} : ContDiffOn ℝ n log {0}ᶜ

Proof state:
n : WithTop ℕ∞
⊢ ContDiffOn ℝ n log {0}ᶜ

Tactic:
intro x hx

Result:
n : WithTop ℕ∞
x : ℝ
hx : x ∈ {0}ᶜ
⊢ ContDiffWithinAt ℝ n log {0}ᶜ x

Proof state:
n : WithTop ℕ∞
x : ℝ
hx : x ∈ {0}ᶜ
⊢ ContDiffWithinAt ℝ n log {0}ᶜ x

Tactic:
simp only [mem_compl_iff, mem_singleton_iff] at hx

Result:
n : WithTop ℕ∞
x : ℝ
hx : ¬x = 0
⊢ ContDiffWithinAt ℝ n log {0}ᶜ x

Proof state:
n : WithTop ℕ∞
x : ℝ
hx : ¬x = 0
⊢ ContDiffWithinAt ℝ n log {0}ᶜ x

Tactic:
exact (contDiffAt_log.2 hx).contDiffWithinAt

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem isBase_iff_maximal_indep : M.IsBase B ↔ Maximal M.Indep B

Proof state:
α : Type u_1
M : Matroid α
B : Set α
⊢ M.IsBase B ↔ M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t

Tactic:
refine ⟨fun h ↦ ⟨h.indep, fun _ ↦ h.eq_of_subset_indep⟩, fun ⟨h, h'⟩ ↦ ?_⟩

Result:
α : Type u_1
M : Matroid α
B : Set α
x✝ : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
h : M.Indep B
h' : ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
⊢ M.IsBase B

Proof state:
α : Type u_1
M : Matroid α
B : Set α
x✝ : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
h : M.Indep B
h' : ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
⊢ M.IsBase B

Tactic:
obtain ⟨B', hB', hBB'⟩ := h.exists_isBase_superset

Result:
case intro.intro
α : Type u_1
M : Matroid α
B : Set α
x✝ : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
h : M.Indep B
h' : ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
B' : Set α
hB' : M.IsBase B'
hBB' : B ⊆ B'
⊢ M.IsBase B

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
B : Set α
x✝ : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
h : M.Indep B
h' : ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
B' : Set α
hB' : M.IsBase B'
hBB' : B ⊆ B'
⊢ M.IsBase B

Tactic:
rwa [h' hB'.indep hBB']

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
B : Set α
⊢ M.IsBase B ↔ Maximal M.Indep B

Tactic:
rw [maximal_subset_iff]

Result:
α : Type u_1
M : Matroid α
B : Set α
⊢ M.IsBase B ↔ M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem norm_ofSubsingleton [Subsingleton ι] (i : ι) (f : G →L[𝕜] G') :
    ‖ofSubsingleton 𝕜 G G' i f‖ = ‖f‖

Proof state:
𝕜 : Type u
ι : Type v
G : Type wG
G' : Type wG'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : SeminormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
inst✝¹ : Fintype ι
inst✝ : Subsingleton ι
i : ι
f : G →L[𝕜] G'
⊢ ‖(ofSubsingleton 𝕜 G G' i) f‖ = ‖f‖

Tactic:
letI : Unique ι := uniqueOfSubsingleton i

Result:
𝕜 : Type u
ι : Type v
G : Type wG
G' : Type wG'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : SeminormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
inst✝¹ : Fintype ι
inst✝ : Subsingleton ι
i : ι
f : G →L[𝕜] G'
this : Unique ι := uniqueOfSubsingleton i
⊢ ‖(ofSubsingleton 𝕜 G G' i) f‖ = ‖f‖

Proof state:
𝕜 : Type u
ι : Type v
G : Type wG
G' : Type wG'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : SeminormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
inst✝¹ : Fintype ι
inst✝ : Subsingleton ι
i : ι
f : G →L[𝕜] G'
this : Unique ι := uniqueOfSubsingleton i
⊢ ‖(ofSubsingleton 𝕜 G G' i) f‖ = ‖f‖

Tactic:
simp [norm_def, ContinuousLinearMap.norm_def, (Equiv.funUnique _ _).symm.surjective.forall]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Equiv.lean
theorem ofBijective_symm_apply_apply [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {h} (x : M) :
    (ofBijective f h).symm (f x) = x

Proof state:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
f : M →ₛₗ[σ₁₂] M₂
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
h : Bijective ⇑f
x : M
⊢ (ofBijective f h).symm (f x) = x

Tactic:
simp [LinearEquiv.symm_apply_eq]

Result:
no goals
-- Mathlib/RingTheory/WittVector/DiscreteValuationRing.lean
theorem isUnit_of_coeff_zero_ne_zero (x : 𝕎 k) (hx : x.coeff 0 ≠ 0) : IsUnit x

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
x : 𝕎 k
hx : x.coeff 0 ≠ 0
y : kˣ := Units.mk0 (x.coeff 0) hx
hy : x.coeff 0 = ↑y
⊢ IsUnit x

Tactic:
exact (mkUnit hy).isUnit

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
x : 𝕎 k
hx : x.coeff 0 ≠ 0
⊢ IsUnit x

Tactic:
let y : kˣ := Units.mk0 (x.coeff 0) hx

Result:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
x : 𝕎 k
hx : x.coeff 0 ≠ 0
y : kˣ := Units.mk0 (x.coeff 0) hx
⊢ IsUnit x

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
x : 𝕎 k
hx : x.coeff 0 ≠ 0
y : kˣ := Units.mk0 (x.coeff 0) hx
⊢ IsUnit x

Tactic:
have hy : x.coeff 0 = y := rfl

Result:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
x : 𝕎 k
hx : x.coeff 0 ≠ 0
y : kˣ := Units.mk0 (x.coeff 0) hx
hy : x.coeff 0 = ↑y
⊢ IsUnit x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapFinIdx_eq_mapIdx {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} {g : Nat → α → β}
    (h : ∀ (i : Nat) (h : i < l.length), f i l[i] h = g i l[i]) :
    l.mapFinIdx f = l.mapIdx g

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
g : Nat → α → β
h : ∀ (i : Nat) (h : i < l.length), f i l[i] h = g i l[i]
⊢ l.mapFinIdx f = mapIdx g l

Tactic:
simp_all [mapFinIdx_eq_iff]

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Nat.lean
theorem normalize_of_nonpos {z : ℤ} (h : z ≤ 0) : normalize z = -z

Proof state:
case inr
z : ℤ
h✝ : z ≤ 0
h : z < 0
⊢ normalize z = -z

Tactic:
rw [normalize_apply, normUnit_eq, if_neg (not_le_of_gt h), Units.val_neg, Units.val_one,
  mul_neg_one]

Result:
no goals

Proof state:
case inl
h : 0 ≤ 0
⊢ normalize 0 = -0

Tactic:
simp

Result:
no goals

Proof state:
z : ℤ
h : z ≤ 0
⊢ normalize z = -z

Tactic:
obtain rfl | h := h.eq_or_lt

Result:
case inl
h : 0 ≤ 0
⊢ normalize 0 = -0

case inr
z : ℤ
h✝ : z ≤ 0
h : z < 0
⊢ normalize z = -z
-- Mathlib/Geometry/Manifold/PartitionOfUnity.lean
theorem exists_isSubordinate_chartAt_source :
    ∃ f : SmoothPartitionOfUnity M I M univ, f.IsSubordinate (fun x ↦ (chartAt H x).source)

Proof state:
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
⊢ ∃ f, f.IsSubordinate fun x => (chartAt H x).source

Tactic:
apply exists_isSubordinate _ isClosed_univ _ (fun i ↦ (chartAt H _).open_source) (fun x _ ↦ ?_)

Result:
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
x : M
x✝ : x ∈ univ
⊢ x ∈ ⋃ i, (chartAt H i).source

Proof state:
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
x : M
x✝ : x ∈ univ
⊢ x ∈ ⋃ i, (chartAt H i).source

Tactic:
exact mem_iUnion_of_mem x (mem_chart_source H x)

Result:
no goals
-- Mathlib/Algebra/Polynomial/BigOperators.lean
theorem coeff_zero_multiset_prod : t.prod.coeff 0 = (t.map fun f => coeff f 0).prod

Proof state:
case refine_2
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ht : t.prod.coeff 0 = (Multiset.map (fun f => f.coeff 0) t).prod
⊢ (a ::ₘ t).prod.coeff 0 = (Multiset.map (fun f => f.coeff 0) (a ::ₘ t)).prod

Tactic:
rw [Multiset.prod_cons, Multiset.map_cons, Multiset.prod_cons, Polynomial.mul_coeff_zero, ht]

Result:
no goals

Proof state:
case refine_1
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
⊢ (prod 0).coeff 0 = (Multiset.map (fun f => f.coeff 0) 0).prod

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
⊢ t.prod.coeff 0 = (Multiset.map (fun f => f.coeff 0) t).prod

Tactic:
refine Multiset.induction_on t ?_ fun a t ht => ?_

Result:
case refine_1
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
⊢ (prod 0).coeff 0 = (Multiset.map (fun f => f.coeff 0) 0).prod

case refine_2
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ht : t.prod.coeff 0 = (Multiset.map (fun f => f.coeff 0) t).prod
⊢ (a ::ₘ t).prod.coeff 0 = (Multiset.map (fun f => f.coeff 0) (a ::ₘ t)).prod
-- Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean
theorem ι_colimitCompWhiskeringLeftIsoCompColimit_hom (F : J ⥤ K ⥤ C) (G : D ⥤ K)
    [HasColimitsOfShape J C] (j : J) :
    colimit.ι (F ⋙ (whiskeringLeft _ _ _).obj G) j ≫
      (colimitCompWhiskeringLeftIsoCompColimit F G).hom = whiskerLeft G (colimit.ι F j)

Proof state:
case w.h
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
G : D ⥤ K
inst✝ : HasColimitsOfShape J C
j : J
d : D
⊢ (colimit.ι (F ⋙ (whiskeringLeft D K C).obj G) j ≫ (colimitCompWhiskeringLeftIsoCompColimit F G).hom).app d =
    (whiskerLeft G (colimit.ι F j)).app d

Tactic:
simp [colimitCompWhiskeringLeftIsoCompColimit]

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
G : D ⥤ K
inst✝ : HasColimitsOfShape J C
j : J
⊢ colimit.ι (F ⋙ (whiskeringLeft D K C).obj G) j ≫ (colimitCompWhiskeringLeftIsoCompColimit F G).hom =
    whiskerLeft G (colimit.ι F j)

Tactic:
ext d

Result:
case w.h
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
G : D ⥤ K
inst✝ : HasColimitsOfShape J C
j : J
d : D
⊢ (colimit.ι (F ⋙ (whiskeringLeft D K C).obj G) j ≫ (colimitCompWhiskeringLeftIsoCompColimit F G).hom).app d =
    (whiskerLeft G (colimit.ι F j)).app d
-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem linearCombination_restrict (s : Set α) :
    linearCombination R (s.restrict v) = Submodule.subtype _ ∘ₗ
      linearCombinationOn α M R v s ∘ₗ (supportedEquivFinsupp s).symm.toLinearMap

Proof state:
case h.h
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
a✝ : ↑s
⊢ (linearCombination R (s.restrict v) ∘ₗ lsingle a✝) 1 =
    (((span R (v '' s)).subtype ∘ₗ linearCombinationOn α M R v s ∘ₗ ↑(supportedEquivFinsupp s).symm) ∘ₗ lsingle a✝) 1

Tactic:
simp [linearCombinationOn]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
⊢ linearCombination R (s.restrict v) =
    (span R (v '' s)).subtype ∘ₗ linearCombinationOn α M R v s ∘ₗ ↑(supportedEquivFinsupp s).symm

Tactic:
ext

Result:
case h.h
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
a✝ : ↑s
⊢ (linearCombination R (s.restrict v) ∘ₗ lsingle a✝) 1 =
    (((span R (v '' s)).subtype ∘ₗ linearCombinationOn α M R v s ∘ₗ ↑(supportedEquivFinsupp s).symm) ∘ₗ lsingle a✝) 1

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
s : Set α
⊢ linearCombination R (s.restrict v) =
    (span R (v '' s)).subtype ∘ₗ linearCombinationOn α M R v s ∘ₗ ↑(supportedEquivFinsupp s).symm

Tactic:
classical ext; simp [linearCombinationOn]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem or_append {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} :
    (x₁ ++ y₁) ||| (x₂ ++ y₂) = (x₁ ||| x₂) ++ (y₁ ||| y₂)

Proof state:
w v : Nat
x₁ x₂ : BitVec w
y₁ y₂ : BitVec v
⊢ x₁ ++ y₁ ||| x₂ ++ y₂ = (x₁ ||| x₂) ++ (y₁ ||| y₂)

Tactic:
ext i

Result:
case pred
w v : Nat
x₁ x₂ : BitVec w
y₁ y₂ : BitVec v
i : Nat
a✝ : i < w + v
⊢ (x₁ ++ y₁ ||| x₂ ++ y₂).getLsbD i = ((x₁ ||| x₂) ++ (y₁ ||| y₂)).getLsbD i

Proof state:
case pred
w v : Nat
x₁ x₂ : BitVec w
y₁ y₂ : BitVec v
i : Nat
a✝ : i < w + v
⊢ (x₁ ++ y₁ ||| x₂ ++ y₂).getLsbD i = if i < v then (y₁ ||| y₂).getLsbD i else (x₁ ||| x₂).getLsbD (i - v)

Tactic:
split <;> simp [getLsbD_append, *]

Result:
no goals

Proof state:
case pred
w v : Nat
x₁ x₂ : BitVec w
y₁ y₂ : BitVec v
i : Nat
a✝ : i < w + v
⊢ (x₁ ++ y₁ ||| x₂ ++ y₂).getLsbD i = ((x₁ ||| x₂) ++ (y₁ ||| y₂)).getLsbD i

Tactic:
simp only [getLsbD_append, cond_eq_if]

Result:
case pred
w v : Nat
x₁ x₂ : BitVec w
y₁ y₂ : BitVec v
i : Nat
a✝ : i < w + v
⊢ (x₁ ++ y₁ ||| x₂ ++ y₂).getLsbD i = if i < v then (y₁ ||| y₂).getLsbD i else (x₁ ||| x₂).getLsbD (i - v)
-- Mathlib/Algebra/Group/Pi/Basic.lean
theorem apply_mulSingle₂ (f' : ∀ i, f i → g i → h i) (hf' : ∀ i, f' i 1 1 = 1) (i : I)
    (x : f i) (y : g i) (j : I) :
    f' j (mulSingle i x j) (mulSingle i y j) = mulSingle i (f' i x y) j

Proof state:
I : Type u
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
inst✝³ : DecidableEq I
inst✝² : (i : I) → One (f i)
inst✝¹ : (i : I) → One (g i)
inst✝ : (i : I) → One (h i)
f' : (i : I) → f i → g i → h i
hf' : ∀ (i : I), f' i 1 1 = 1
i : I
x : f i
y : g i
j : I
⊢ f' j (mulSingle i x j) (mulSingle i y j) = mulSingle i (f' i x y) j

Tactic:
by_cases h : j = i

Result:
case pos
I : Type u
f : I → Type v₁
g : I → Type v₂
h✝ : I → Type v₃
inst✝³ : DecidableEq I
inst✝² : (i : I) → One (f i)
inst✝¹ : (i : I) → One (g i)
inst✝ : (i : I) → One (h✝ i)
f' : (i : I) → f i → g i → h✝ i
hf' : ∀ (i : I), f' i 1 1 = 1
i : I
x : f i
y : g i
j : I
h : j = i
⊢ f' j (mulSingle i x j) (mulSingle i y j) = mulSingle i (f' i x y) j

case neg
I : Type u
f : I → Type v₁
g : I → Type v₂
h✝ : I → Type v₃
inst✝³ : DecidableEq I
inst✝² : (i : I) → One (f i)
inst✝¹ : (i : I) → One (g i)
inst✝ : (i : I) → One (h✝ i)
f' : (i : I) → f i → g i → h✝ i
hf' : ∀ (i : I), f' i 1 1 = 1
i : I
x : f i
y : g i
j : I
h : ¬j = i
⊢ f' j (mulSingle i x j) (mulSingle i y j) = mulSingle i (f' i x y) j

Proof state:
case pos
I : Type u
f : I → Type v₁
g : I → Type v₂
h✝ : I → Type v₃
inst✝³ : DecidableEq I
inst✝² : (i : I) → One (f i)
inst✝¹ : (i : I) → One (g i)
inst✝ : (i : I) → One (h✝ i)
f' : (i : I) → f i → g i → h✝ i
hf' : ∀ (i : I), f' i 1 1 = 1
i : I
x : f i
y : g i
j : I
h : j = i
⊢ f' j (mulSingle i x j) (mulSingle i y j) = mulSingle i (f' i x y) j

Tactic:
subst h

Result:
case pos
I : Type u
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
inst✝³ : DecidableEq I
inst✝² : (i : I) → One (f i)
inst✝¹ : (i : I) → One (g i)
inst✝ : (i : I) → One (h i)
f' : (i : I) → f i → g i → h i
hf' : ∀ (i : I), f' i 1 1 = 1
j : I
x : f j
y : g j
⊢ f' j (mulSingle j x j) (mulSingle j y j) = mulSingle j (f' j x y) j

Proof state:
case pos
I : Type u
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
inst✝³ : DecidableEq I
inst✝² : (i : I) → One (f i)
inst✝¹ : (i : I) → One (g i)
inst✝ : (i : I) → One (h i)
f' : (i : I) → f i → g i → h i
hf' : ∀ (i : I), f' i 1 1 = 1
j : I
x : f j
y : g j
⊢ f' j (mulSingle j x j) (mulSingle j y j) = mulSingle j (f' j x y) j

Tactic:
simp only [mulSingle_eq_same]

Result:
no goals

Proof state:
case neg
I : Type u
f : I → Type v₁
g : I → Type v₂
h✝ : I → Type v₃
inst✝³ : DecidableEq I
inst✝² : (i : I) → One (f i)
inst✝¹ : (i : I) → One (g i)
inst✝ : (i : I) → One (h✝ i)
f' : (i : I) → f i → g i → h✝ i
hf' : ∀ (i : I), f' i 1 1 = 1
i : I
x : f i
y : g i
j : I
h : ¬j = i
⊢ f' j (mulSingle i x j) (mulSingle i y j) = mulSingle i (f' i x y) j

Tactic:
simp only [mulSingle_eq_of_ne h, hf']

Result:
no goals
-- Mathlib/Data/Complex/Norm.lean
theorem isCauSeq_conj (f : CauSeq ℂ (‖·‖)) :
    IsCauSeq (‖·‖) fun n ↦ conj (f n) := fun ε ε0 ↦
  let ⟨i, hi⟩ := f.2 ε ε0
  ⟨i, fun j hj => by
    simp_rw [← RingHom.map_sub, norm_conj]; exact hi j hj⟩

Proof state:
f : CauSeq ℂ fun x => ‖x‖
ε : ℝ
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, (fun x => ‖x‖) (↑f j - ↑f i) < ε
j : ℕ
hj : j ≥ i
⊢ ‖↑f j - ↑f i‖ < ε

Tactic:
exact hi j hj

Result:
no goals

Proof state:
f : CauSeq ℂ fun x => ‖x‖
ε : ℝ
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, (fun x => ‖x‖) (↑f j - ↑f i) < ε
j : ℕ
hj : j ≥ i
⊢ (fun x => ‖x‖) ((fun n => (starRingEnd ℂ) (↑f n)) j - (fun n => (starRingEnd ℂ) (↑f n)) i) < ε

Tactic:
simp_rw [← RingHom.map_sub, norm_conj]

Result:
f : CauSeq ℂ fun x => ‖x‖
ε : ℝ
ε0 : ε > 0
i : ℕ
hi : ∀ j ≥ i, (fun x => ‖x‖) (↑f j - ↑f i) < ε
j : ℕ
hj : j ≥ i
⊢ ‖↑f j - ↑f i‖ < ε
-- Mathlib/Topology/Exterior.lean
lemma specializes_iff_exterior_subset : x ⤳ y ↔ exterior {x} ⊆ exterior {y}

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
x y : X
⊢ x ⤳ y ↔ exterior {x} ⊆ exterior {y}

Tactic:
simp [Specializes]

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem IsRestriction.isStrictRestriction_of_ground_ne (h : N ≤r M) (hne : N.E ≠ M.E) : N <r M

Proof state:
α : Type u_1
M N : Matroid α
h : N ≤r M
hne : N.E ≠ M.E
⊢ N <r M

Tactic:
rw [← h.eq_restrict]

Result:
α : Type u_1
M N : Matroid α
h : N ≤r M
hne : N.E ≠ M.E
⊢ M ↾ N.E <r M

Proof state:
α : Type u_1
M N : Matroid α
h : N ≤r M
hne : N.E ≠ M.E
⊢ M ↾ N.E <r M

Tactic:
exact restrict_isStrictRestriction (h.subset.ssubset_of_ne hne)

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean
theorem Cotrident.ofCocone_ι {F : WalkingParallelFamily J ⥤ C} (t : Cocone F) (j) :
    (Cotrident.ofCocone t).ι.app j = eqToHom (by cases j <;> aesop_cat) ≫ t.ι.app j :=
  rfl

Proof state:
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cocone F
j : WalkingParallelFamily J
⊢ (parallelFamily fun j => F.map (line j)).obj j = F.obj j

Tactic:
cases j <;> aesop_cat

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Images.lean
theorem image.isoStrongEpiMono_hom_comp_ι {I' : C} (e : X ⟶ I') (m : I' ⟶ Y) (comm : e ≫ m = f)
    [StrongEpi e] [Mono m] : (image.isoStrongEpiMono e m comm).hom ≫ image.ι f = m

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasStrongEpiMonoFactorisations C
X Y : C
f : X ⟶ Y
I' : C
e : X ⟶ I'
m : I' ⟶ Y
comm : e ≫ m = f
inst✝¹ : StrongEpi e
inst✝ : Mono m
⊢ (StrongEpiMonoFactorisation.mk (MonoFactorisation.mk I' m e ⋯)).toMonoIsImage.lift (Image.monoFactorisation f) ≫ ι f =
    m

Tactic:
apply IsImage.lift_fac

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasStrongEpiMonoFactorisations C
X Y : C
f : X ⟶ Y
I' : C
e : X ⟶ I'
m : I' ⟶ Y
comm : e ≫ m = f
inst✝¹ : StrongEpi e
inst✝ : Mono m
⊢ (isoStrongEpiMono e m comm).hom ≫ ι f = m

Tactic:
dsimp [isoStrongEpiMono]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasStrongEpiMonoFactorisations C
X Y : C
f : X ⟶ Y
I' : C
e : X ⟶ I'
m : I' ⟶ Y
comm : e ≫ m = f
inst✝¹ : StrongEpi e
inst✝ : Mono m
⊢ (StrongEpiMonoFactorisation.mk (MonoFactorisation.mk I' m e ⋯)).toMonoIsImage.lift (Image.monoFactorisation f) ≫ ι f =
    m
-- Mathlib/Data/DFinsupp/BigOperators.lean
theorem prod_subtypeDomain_index [∀ i, Zero (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)]
    [CommMonoid γ] {v : Π₀ i, β i} {p : ι → Prop} [DecidablePred p] {h : ∀ i, β i → γ}
    (hp : ∀ x ∈ v.support, p x) : (v.subtypeDomain p).prod (fun i b => h i b) = v.prod h

Proof state:
ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → Zero (β i)
inst✝² : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝¹ : CommMonoid γ
v : Π₀ (i : ι), β i
p : ι → Prop
inst✝ : DecidablePred p
h : (i : ι) → β i → γ
hp : ∀ x ∈ v.support, p x
⊢ ((subtypeDomain p v).prod fun i b => h (↑i) b) = v.prod h

Tactic:
refine Finset.prod_bij (fun p _ ↦ p) ?_ ?_ ?_ ?_ <;> aesop

Result:
no goals