harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Group/Int.lean
theorem _root_.NNReal.natCast_natAbs (n : ℤ) : (n.natAbs : ℝ≥0) = ‖n‖₊ :=
  NNReal.eq <|
    calc
      ((n.natAbs : ℝ≥0) : ℝ) = (n.natAbs : ℤ)

Proof state:
n : ℤ
⊢ ↑↑n.natAbs = |↑n|

Tactic:
simp only [Int.natCast_natAbs, Int.cast_abs]

Result:
no goals

Proof state:
n : ℤ
⊢ ↑↑n.natAbs = ↑↑n.natAbs

Tactic:
simp only [Int.cast_natCast, NNReal.coe_natCast]

Result:
no goals
-- Mathlib/FieldTheory/PrimitiveElement.lean
theorem primitive_element_iff_minpoly_degree_eq (α : E) :
    F⟮α⟯ = ⊤ ↔ (minpoly F α).degree = finrank F E

Proof state:
F : Type u_3
E : Type u_4
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
α : E
⊢ minpoly F α ≠ 0

Tactic:
exact minpoly.ne_zero_of_finite F α

Result:
no goals

Proof state:
F : Type u_3
E : Type u_4
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
α : E
⊢ F⟮α⟯ = ⊤ ↔ (minpoly F α).degree = ↑(finrank F E)

Tactic:
rw [degree_eq_iff_natDegree_eq, primitive_element_iff_minpoly_natDegree_eq]

Result:
F : Type u_3
E : Type u_4
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
α : E
⊢ minpoly F α ≠ 0
-- Mathlib/CategoryTheory/Sites/CoversTop.lean
lemma ext (F : Sheaf J A) {c : Cone F.1} (hc : IsLimit c) {X : A} {f g : X ⟶ c.pt}
    (h : ∀ (i : I), f ≫ c.π.app (Opposite.op (Y i)) =
      g ≫ c.π.app (Opposite.op (Y i))) :
    f = g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
I : Type u_1
Y : I → C
hY : J.CoversTop Y
F : Sheaf J A
c : Cone F.val
hc : IsLimit c
X : A
f g : X ⟶ c.pt
h : ∀ (i : I), f ≫ c.π.app (Opposite.op (Y i)) = g ≫ c.π.app (Opposite.op (Y i))
Z : Cᵒᵖ
⊢ ∀ (I_1 : (hY.cover (Opposite.unop Z)).Arrow),
    (f ≫ c.π.app Z) ≫ F.val.map I_1.f.op = (g ≫ c.π.app Z) ≫ F.val.map I_1.f.op

Tactic:
rintro ⟨W, a, ⟨i, ⟨b⟩⟩⟩

Result:
case mk.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
I : Type u_1
Y : I → C
hY : J.CoversTop Y
F : Sheaf J A
c : Cone F.val
hc : IsLimit c
X : A
f g : X ⟶ c.pt
h : ∀ (i : I), f ≫ c.π.app (Opposite.op (Y i)) = g ≫ c.π.app (Opposite.op (Y i))
Z : Cᵒᵖ
W : C
a : W ⟶ Opposite.unop Z
i : I
b : W ⟶ Y i
⊢ (f ≫ c.π.app Z) ≫ F.val.map { Y := W, f := a, hf := ⋯ }.f.op =
    (g ≫ c.π.app Z) ≫ F.val.map { Y := W, f := a, hf := ⋯ }.f.op

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
I : Type u_1
Y : I → C
hY : J.CoversTop Y
F : Sheaf J A
c : Cone F.val
hc : IsLimit c
X : A
f g : X ⟶ c.pt
h : ∀ (i : I), f ≫ c.π.app (Opposite.op (Y i)) = g ≫ c.π.app (Opposite.op (Y i))
⊢ f = g

Tactic:
refine hc.hom_ext (fun Z => F.2.hom_ext (hY.cover Z.unop) _ _ ?_)

Result:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
I : Type u_1
Y : I → C
hY : J.CoversTop Y
F : Sheaf J A
c : Cone F.val
hc : IsLimit c
X : A
f g : X ⟶ c.pt
h : ∀ (i : I), f ≫ c.π.app (Opposite.op (Y i)) = g ≫ c.π.app (Opposite.op (Y i))
Z : Cᵒᵖ
⊢ ∀ (I_1 : (hY.cover (Opposite.unop Z)).Arrow),
    (f ≫ c.π.app Z) ≫ F.val.map I_1.f.op = (g ≫ c.π.app Z) ≫ F.val.map I_1.f.op

Proof state:
case mk.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
I : Type u_1
Y : I → C
hY : J.CoversTop Y
F : Sheaf J A
c : Cone F.val
hc : IsLimit c
X : A
f g : X ⟶ c.pt
h : ∀ (i : I), f ≫ c.π.app (Opposite.op (Y i)) = g ≫ c.π.app (Opposite.op (Y i))
Z : Cᵒᵖ
W : C
a : W ⟶ Opposite.unop Z
i : I
b : W ⟶ Y i
⊢ (f ≫ c.π.app Z) ≫ F.val.map { Y := W, f := a, hf := ⋯ }.f.op =
    (g ≫ c.π.app Z) ≫ F.val.map { Y := W, f := a, hf := ⋯ }.f.op

Tactic:
simpa using h i =≫ F.1.map b.op

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem getElem?_zipWith {f : α → β → γ} {i : Nat} :
    (zipWith f as bs)[i]? = match as[i]?, bs[i]? with
      | some a, some b => some (f a b) | _, _ => none

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
i : Nat
toList✝¹ : List α
toList✝ : List β
⊢ (match toList✝¹[i]?, toList✝[i]? with
    | some a, some b => some (f a b)
    | x, x_1 => none) =
    match toList✝¹[i]?, toList✝[i]? with
    | some a, some b => some (f a b)
    | x, x_1 => none

Tactic:
rfl

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
i : Nat
toList✝¹ : List α
toList✝ : List β
⊢ (zipWith f { toList := toList✝¹ } { toList := toList✝ })[i]? =
    match { toList := toList✝¹ }[i]?, { toList := toList✝ }[i]? with
    | some a, some b => some (f a b)
    | x, x_1 => none

Tactic:
simp [List.getElem?_zipWith]

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
i : Nat
toList✝¹ : List α
toList✝ : List β
⊢ (match toList✝¹[i]?, toList✝[i]? with
    | some a, some b => some (f a b)
    | x, x_1 => none) =
    match toList✝¹[i]?, toList✝[i]? with
    | some a, some b => some (f a b)
    | x, x_1 => none

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : Array α
bs : Array β
f : α → β → γ
i : Nat
⊢ (zipWith f as bs)[i]? =
    match as[i]?, bs[i]? with
    | some a, some b => some (f a b)
    | x, x_1 => none

Tactic:
cases as

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
bs : Array β
f : α → β → γ
i : Nat
toList✝ : List α
⊢ (zipWith f { toList := toList✝ } bs)[i]? =
    match { toList := toList✝ }[i]?, bs[i]? with
    | some a, some b => some (f a b)
    | x, x_1 => none

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
bs : Array β
f : α → β → γ
i : Nat
toList✝ : List α
⊢ (zipWith f { toList := toList✝ } bs)[i]? =
    match { toList := toList✝ }[i]?, bs[i]? with
    | some a, some b => some (f a b)
    | x, x_1 => none

Tactic:
cases bs

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
i : Nat
toList✝¹ : List α
toList✝ : List β
⊢ (zipWith f { toList := toList✝¹ } { toList := toList✝ })[i]? =
    match { toList := toList✝¹ }[i]?, { toList := toList✝ }[i]? with
    | some a, some b => some (f a b)
    | x, x_1 => none
-- Mathlib/Probability/Moments/Basic.lean
theorem mgf_add_const (α : ℝ) : mgf (fun ω => X ω + α) μ t = mgf X μ t *  exp (t * α)

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
⊢ mgf (fun ω => X ω + α) μ t = mgf X μ t * rexp (t * α)

Tactic:
simp only [add_comm, mgf_const_add, mul_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
@[simp]
lemma dualAnnihilator_ker_eq_range_flip [IsReflexive K V₂] :
    (ker B).dualAnnihilator = range B.flip

Proof state:
K : Type uK
inst✝⁵ : Field K
V₁ : Type uV₁
V₂ : Type uV₂
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst✝ : IsReflexive K V₂
⊢ (ker B).dualAnnihilator = range B.flip

Tactic:
change _ = range (B.dualMap.comp (Module.evalEquiv K V₂).toLinearMap)

Result:
K : Type uK
inst✝⁵ : Field K
V₁ : Type uV₁
V₂ : Type uV₂
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst✝ : IsReflexive K V₂
⊢ (ker B).dualAnnihilator = range (B.dualMap ∘ₗ ↑(evalEquiv K V₂))

Proof state:
K : Type uK
inst✝⁵ : Field K
V₁ : Type uV₁
V₂ : Type uV₂
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst✝ : IsReflexive K V₂
⊢ (ker B).dualAnnihilator = range (B.dualMap ∘ₗ ↑(evalEquiv K V₂))

Tactic:
rw [← range_dualMap_eq_dualAnnihilator_ker, range_comp_of_range_eq_top _ (LinearEquiv.range _)]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem Finite.cast_ncard_eq (hs : s.Finite) : s.ncard = s.encard

Proof state:
α : Type u_1
s : Set α
hs : s.Finite
⊢ ↑s.ncard = s.encard

Tactic:
rwa [ncard, ENat.coe_toNat_eq_self, ne_eq, encard_eq_top_iff, Set.Infinite, not_not]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Induced.lean
theorem trim_binop {m₁ m₂ m₃ : OuterMeasure α} {op : ℝ≥0∞ → ℝ≥0∞ → ℝ≥0∞}
    (h : ∀ s, m₁ s = op (m₂ s) (m₃ s)) (s : Set α) : m₁.trim s = op (m₂.trim s) (m₃.trim s)

Proof state:
case intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
m₁ m₂ m₃ : OuterMeasure α
op : ℝ≥0∞ → ℝ≥0∞ → ℝ≥0∞
h : ∀ (s : Set α), m₁ s = op (m₂ s) (m₃ s)
s t : Set α
_hst : s ⊆ t
_ht : MeasurableSet t
htm : m₁ t = m₁.trim s ∧ m₂ t = m₂.trim s ∧ m₃ t = m₃.trim s ∧ ∀ (i : Fin 0), (![] i) t = (![] i).trim s
⊢ m₁.trim s = op (m₂.trim s) (m₃.trim s)

Tactic:
rw [← htm.1, ← htm.2.1, ← htm.2.2.1, h]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
m₁ m₂ m₃ : OuterMeasure α
op : ℝ≥0∞ → ℝ≥0∞ → ℝ≥0∞
h : ∀ (s : Set α), m₁ s = op (m₂ s) (m₃ s)
s : Set α
⊢ m₁.trim s = op (m₂.trim s) (m₃.trim s)

Tactic:
rcases exists_measurable_superset_forall_eq_trim ![m₁, m₂, m₃] s with ⟨t, _hst, _ht, htm⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
m₁ m₂ m₃ : OuterMeasure α
op : ℝ≥0∞ → ℝ≥0∞ → ℝ≥0∞
h : ∀ (s : Set α), m₁ s = op (m₂ s) (m₃ s)
s t : Set α
_hst : s ⊆ t
_ht : MeasurableSet t
htm : ∀ (i : Fin (Nat.succ 0).succ.succ), (![m₁, m₂, m₃] i) t = (![m₁, m₂, m₃] i).trim s
⊢ m₁.trim s = op (m₂.trim s) (m₃.trim s)

Proof state:
case intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
m₁ m₂ m₃ : OuterMeasure α
op : ℝ≥0∞ → ℝ≥0∞ → ℝ≥0∞
h : ∀ (s : Set α), m₁ s = op (m₂ s) (m₃ s)
s t : Set α
_hst : s ⊆ t
_ht : MeasurableSet t
htm : ∀ (i : Fin (Nat.succ 0).succ.succ), (![m₁, m₂, m₃] i) t = (![m₁, m₂, m₃] i).trim s
⊢ m₁.trim s = op (m₂.trim s) (m₃.trim s)

Tactic:
simp only [Fin.forall_iff_succ, Matrix.cons_val_zero, Matrix.cons_val_succ] at htm

Result:
case intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
m₁ m₂ m₃ : OuterMeasure α
op : ℝ≥0∞ → ℝ≥0∞ → ℝ≥0∞
h : ∀ (s : Set α), m₁ s = op (m₂ s) (m₃ s)
s t : Set α
_hst : s ⊆ t
_ht : MeasurableSet t
htm : m₁ t = m₁.trim s ∧ m₂ t = m₂.trim s ∧ m₃ t = m₃.trim s ∧ ∀ (i : Fin 0), (![] i) t = (![] i).trim s
⊢ m₁.trim s = op (m₂.trim s) (m₃.trim s)
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem sum_def {A} [AddCommMonoid A] {p : MvPolynomial σ R} {b : (σ →₀ ℕ) → R → A} :
    p.sum b = ∑ m ∈ p.support, b m (p.coeff m)

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
inst✝ : AddCommMonoid A
p : MvPolynomial σ R
b : (σ →₀ ℕ) → R → A
⊢ sum p b = ∑ m ∈ p.support, b m (coeff m p)

Tactic:
simp [support, Finsupp.sum, coeff]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem out_lift_equiv (a : Cardinal.{u}) : Nonempty ((lift.{v} a).out ≃ a.out)

Proof state:
a : Cardinal.{u}
⊢ Nonempty (Quotient.out (lift.{v, u} a) ≃ Quotient.out a)

Tactic:
rw [← mk_out a, ← mk_uLift, mk_out]

Result:
a : Cardinal.{u}
⊢ Nonempty (Quotient.out #(ULift.{v, u} (Quotient.out a)) ≃ Quotient.out a)

Proof state:
a : Cardinal.{u}
⊢ Nonempty (Quotient.out #(ULift.{v, u} (Quotient.out a)) ≃ Quotient.out a)

Tactic:
exact ⟨outMkEquiv.trans Equiv.ulift⟩

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[simp] lemma prod'_ε_fst : (ε (prod' F G)).1 = ε F

Proof state:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
⊢ (ε (F.prod G)).1 = ε F

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
⊢ (ε (F.prod' G)).1 = ε F

Tactic:
change _ ≫ F.map (𝟙 _) = _

Result:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
⊢ (ε (F.prod G)).1 ≫ F.map (𝟙 (𝟙_ (C × C)).1) = ε F

Proof state:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
⊢ (ε (F.prod G)).1 ≫ F.map (𝟙 (𝟙_ (C × C)).1) = ε F

Tactic:
rw [Functor.map_id, Category.comp_id]

Result:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
⊢ (ε (F.prod G)).1 = ε F
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[ext]
lemma ext (z₁ z₂ : Cochain F G n)
    (h : ∀ (p q hpq), z₁.v p q hpq = z₂.v p q hpq) : z₁ = z₂

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z₁ z₂ : Cochain F G n
h : ∀ (p q : ℤ) (hpq : p + n = q), z₁.v p q hpq = z₂.v p q hpq
⊢ z₁ = z₂

Tactic:
funext ⟨p, q, hpq⟩

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z₁ z₂ : Cochain F G n
h : ∀ (p q : ℤ) (hpq : p + n = q), z₁.v p q hpq = z₂.v p q hpq
p q : ℤ
hpq : p + n = q
⊢ z₁ { p := p, q := q, hpq := hpq } = z₂ { p := p, q := q, hpq := hpq }

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z₁ z₂ : Cochain F G n
h : ∀ (p q : ℤ) (hpq : p + n = q), z₁.v p q hpq = z₂.v p q hpq
p q : ℤ
hpq : p + n = q
⊢ z₁ { p := p, q := q, hpq := hpq } = z₂ { p := p, q := q, hpq := hpq }

Tactic:
apply h

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem Iic_sInf (s : Set α) : Iic (sInf s) = ⋂ a ∈ s, Iic a

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
⊢ Iic (sInf s) = ⋂ a ∈ s, Iic a

Tactic:
rw [sInf_eq_iInf, Iic_iInf₂]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem cmp_to_nat_lemma {m n : PosNum} : (m : ℕ) < n → (bit1 m : ℕ) < bit0 n :=
  show (m : ℕ) < n → (m + m + 1 + 1 : ℕ) ≤ n + n by
    intro h; rw [Nat.add_right_comm m m 1, add_assoc]; exact Nat.add_le_add h h

Proof state:
m n : PosNum
h : ↑m < ↑n
⊢ ↑m + ↑m + 1 + 1 ≤ ↑n + ↑n

Tactic:
rw [Nat.add_right_comm m m 1, add_assoc]

Result:
m n : PosNum
h : ↑m < ↑n
⊢ ↑m + 1 + (↑m + 1) ≤ ↑n + ↑n

Proof state:
m n : PosNum
⊢ ↑m < ↑n → ↑m + ↑m + 1 + 1 ≤ ↑n + ↑n

Tactic:
intro h

Result:
m n : PosNum
h : ↑m < ↑n
⊢ ↑m + ↑m + 1 + 1 ≤ ↑n + ↑n

Proof state:
m n : PosNum
h : ↑m < ↑n
⊢ ↑m + 1 + (↑m + 1) ≤ ↑n + ↑n

Tactic:
exact Nat.add_le_add h h

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Subspace.lean
theorem OrthogonalFamily.norm_sum (l : ∀ i, G i) (s : Finset ι) :
    ‖∑ i ∈ s, V i (l i)‖ ^ 2 = ∑ i ∈ s, ‖l i‖ ^ 2

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
l : (i : ι) → G i
s : Finset ι
⊢ ↑‖∑ i ∈ s, (V i) (l i)‖ ^ 2 = ∑ i ∈ s, ↑‖l i‖ ^ 2

Tactic:
simp only [← inner_self_eq_norm_sq_to_K, hV.inner_sum]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
l : (i : ι) → G i
s : Finset ι
⊢ ‖∑ i ∈ s, (V i) (l i)‖ ^ 2 = ∑ i ∈ s, ‖l i‖ ^ 2

Tactic:
have : ((‖∑ i ∈ s, V i (l i)‖ : ℝ) : 𝕜) ^ 2 = ∑ i ∈ s, ((‖l i‖ : ℝ) : 𝕜) ^ 2 := by
  simp only [← inner_self_eq_norm_sq_to_K, hV.inner_sum]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
l : (i : ι) → G i
s : Finset ι
this : ↑‖∑ i ∈ s, (V i) (l i)‖ ^ 2 = ∑ i ∈ s, ↑‖l i‖ ^ 2
⊢ ‖∑ i ∈ s, (V i) (l i)‖ ^ 2 = ∑ i ∈ s, ‖l i‖ ^ 2

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
l : (i : ι) → G i
s : Finset ι
this : ↑‖∑ i ∈ s, (V i) (l i)‖ ^ 2 = ∑ i ∈ s, ↑‖l i‖ ^ 2
⊢ ‖∑ i ∈ s, (V i) (l i)‖ ^ 2 = ∑ i ∈ s, ‖l i‖ ^ 2

Tactic:
exact mod_cast this

Result:
no goals
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
theorem app_eq_invApp_app_of_comp_eq_aux {X Y U : Scheme.{u}} (f : Y ⟶ U) (g : U ⟶ X) (fg : Y ⟶ X)
    (H : fg = f ≫ g) [h : IsOpenImmersion g] (V : U.Opens) :
    f ⁻¹ᵁ V = fg ⁻¹ᵁ (g ''ᵁ V)

Proof state:
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
⊢ f ⁻¹ᵁ V = (Opens.map f.base).obj ((Opens.map g.base).obj (g ''ᵁ V))

Tactic:
congr 1

Result:
case e_a
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
⊢ V = (Opens.map g.base).obj (g ''ᵁ V)

Proof state:
case e_a.h
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
⊢ ↑V = ↑((Opens.map g.base).obj (g ''ᵁ V))

Tactic:
exact (Set.preimage_image_eq _ h.base_open.injective).symm

Result:
no goals

Proof state:
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
fg : Y ⟶ X
H : fg = f ≫ g
h : IsOpenImmersion g
V : U.Opens
⊢ f ⁻¹ᵁ V = fg ⁻¹ᵁ g ''ᵁ V

Tactic:
subst H

Result:
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
⊢ f ⁻¹ᵁ V = (f ≫ g) ⁻¹ᵁ g ''ᵁ V

Proof state:
case e_a
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
⊢ V = (Opens.map g.base).obj (g ''ᵁ V)

Tactic:
ext1

Result:
case e_a.h
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
⊢ ↑V = ↑((Opens.map g.base).obj (g ''ᵁ V))

Proof state:
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
⊢ f ⁻¹ᵁ V = (f ≫ g) ⁻¹ᵁ g ''ᵁ V

Tactic:
rw [Scheme.comp_base, Opens.map_comp_obj]

Result:
X Y U : Scheme
f : Y ⟶ U
g : U ⟶ X
h : IsOpenImmersion g
V : U.Opens
⊢ f ⁻¹ᵁ V = (Opens.map f.base).obj ((Opens.map g.base).obj (g ''ᵁ V))
-- Mathlib/GroupTheory/Perm/ConjAct.lean
theorem cycleFactorsFinset_conj (g k : Perm α) :
    (ConjAct.toConjAct k • g).cycleFactorsFinset =
      Finset.map (MulAut.conj k).toEquiv.toEmbedding g.cycleFactorsFinset

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c ∈ (k * g * k⁻¹).cycleFactorsFinset ↔ k * (MulAut.conj k).symm c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset

Tactic:
simp [mul_assoc]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k : Perm α
⊢ (ConjAct.toConjAct k • g).cycleFactorsFinset = Finset.map (MulAut.conj k).toEmbedding g.cycleFactorsFinset

Tactic:
ext c

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c ∈ (ConjAct.toConjAct k • g).cycleFactorsFinset ↔ c ∈ Finset.map (MulAut.conj k).toEmbedding g.cycleFactorsFinset

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c ∈ (ConjAct.toConjAct k • g).cycleFactorsFinset ↔ c ∈ Finset.map (MulAut.conj k).toEmbedding g.cycleFactorsFinset

Tactic:
rw [ConjAct.smul_def, ConjAct.ofConjAct_toConjAct, Finset.mem_map_equiv,
  ← mem_cycleFactorsFinset_conj g k]

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
⊢ c ∈ (k * g * k⁻¹).cycleFactorsFinset ↔ k * (MulAut.conj k).symm c * k⁻¹ ∈ (k * g * k⁻¹).cycleFactorsFinset
-- Mathlib/MeasureTheory/Covering/Differentiation.lean
theorem aemeasurable_limRatio : AEMeasurable (v.limRatio ρ) μ

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
⊢ AEMeasurable (v.limRatio ρ) μ

Tactic:
apply ENNReal.aemeasurable_of_exist_almost_disjoint_supersets _ _ fun p q hpq => ?_

Result:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
⊢ ∃ u v_1,
    MeasurableSet u ∧
      MeasurableSet v_1 ∧ {x | v.limRatio ρ x < ↑p} ⊆ u ∧ {x | ↑q < v.limRatio ρ x} ⊆ v_1 ∧ μ (u ∩ v_1) = 0

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
⊢ ∃ u v_1,
    MeasurableSet u ∧
      MeasurableSet v_1 ∧ {x | v.limRatio ρ x < ↑p} ⊆ u ∧ {x | ↑q < v.limRatio ρ x} ⊆ v_1 ∧ μ (u ∩ v_1) = 0

Tactic:
exact v.exists_measurable_supersets_limRatio hρ hpq

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
@[simp]
lemma DifferentiableOn.sub_iff_right (hg : DifferentiableOn 𝕜 f s) :
    DifferentiableOn 𝕜 (fun y => f y - g y) s ↔ DifferentiableOn 𝕜 g s

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
s : Set E
hg : DifferentiableOn 𝕜 f s
⊢ DifferentiableOn 𝕜 (fun y => f y - g y) s ↔ DifferentiableOn 𝕜 g s

Tactic:
simp only [sub_eq_add_neg, differentiableOn_neg_iff, hg, add_iff_right]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem mkMetric_le_liminf_sum {β : Type*} {ι : β → Type*} [hι : ∀ n, Fintype (ι n)] (s : Set X)
    {l : Filter β} (r : β → ℝ≥0∞) (hr : Tendsto r l (𝓝 0)) (t : ∀ n : β, ι n → Set X)
    (ht : ∀ᶠ n in l, ∀ i, diam (t n i) ≤ r n) (hst : ∀ᶠ n in l, s ⊆ ⋃ i, t n i) (m : ℝ≥0∞ → ℝ≥0∞) :
    mkMetric m s ≤ liminf (fun n => ∑ i, m (diam (t n i))) l

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
β : Type u_4
ι : β → Type u_5
hι : (n : β) → Fintype (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), diam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i
m : ℝ≥0∞ → ℝ≥0∞
⊢ (mkMetric m) s ≤ liminf (fun n => ∑ i : ι n, m (diam (t n i))) l

Tactic:
simpa only [tsum_fintype] using mkMetric_le_liminf_tsum s r hr t ht hst m

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem set_mk (a : Array α) (h : a.size = n) (i x w) :
    (Vector.mk a h).set i x = Vector.mk (a.set i x) (by simp [h]) := rfl

Proof state:
α : Type ?u.13676
n : Nat
a : Array α
h : a.size = n
i : Nat
x : α
w : i < n
⊢ (a.set i x ⋯).size = n

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_const_mul_Icc (a b : α) {c : α} (h : 0 < c) :
    (c * ·) ⁻¹' Icc a b = Icc (a / c) (b / c)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b c : α
h : 0 < c
⊢ (fun x => c * x) ⁻¹' Icc a b = Icc (a / c) (b / c)

Tactic:
simp [← Ici_inter_Iic, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/DecidableEq.lean
theorem beq_toArray [BEq α] (a b : List α) : (a.toArray == b.toArray) = (a == b)

Proof state:
α : Type u_1
inst✝ : BEq α
a b : List α
⊢ (a.toArray == b.toArray) = (a == b)

Tactic:
simp [beq_eq_decide, Array.beq_eq_decide]

Result:
no goals
-- Mathlib/Data/Fintype/Sets.lean
theorem toFinset_univ [Fintype α] [Fintype (Set.univ : Set α)] :
    (Set.univ : Set α).toFinset = Finset.univ

Proof state:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Fintype ↑univ
a✝ : α
⊢ a✝ ∈ univ.toFinset ↔ a✝ ∈ Finset.univ

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Fintype ↑univ
⊢ univ.toFinset = Finset.univ

Tactic:
ext

Result:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Fintype ↑univ
a✝ : α
⊢ a✝ ∈ univ.toFinset ↔ a✝ ∈ Finset.univ