harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Bounds/Basic.lean
theorem isGLB_Ioo {a b : γ} (h : a < b) : IsGLB (Ioo a b) a :=
  ⟨fun _ hx => hx.1.le, fun x hx => by
    rcases eq_or_lt_of_le (le_sup_right : a ≤ x ⊔ a) with h₁ | h₂
    · exact h₁.symm ▸ le_sup_left
    obtain ⟨y, lty, ylt⟩ := exists_between h₂
    apply (not_lt_of_le (sup_le (hx ⟨lty, ylt.trans_le (sup_le _ h.le)⟩) lty.le) ylt).elim
    obtain ⟨u, au, ub⟩ := exists_between h
    apply (hx ⟨au, ub⟩).trans ub.le⟩

Proof state:
case inr
γ : Type v
inst✝¹ : SemilatticeSup γ
inst✝ : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₂ : a < x ⊔ a
⊢ x ≤ a

Tactic:
obtain ⟨y, lty, ylt⟩ := exists_between h₂

Result:
case inr.intro.intro
γ : Type v
inst✝¹ : SemilatticeSup γ
inst✝ : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₂ : a < x ⊔ a
y : γ
lty : a < y
ylt : y < x ⊔ a
⊢ x ≤ a

Proof state:
case inr.intro.intro
γ : Type v
inst✝¹ : SemilatticeSup γ
inst✝ : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₂ : a < x ⊔ a
y : γ
lty : a < y
ylt : y < x ⊔ a
⊢ x ≤ a

Tactic:
apply (not_lt_of_le (sup_le (hx ⟨lty, ylt.trans_le (sup_le _ h.le)⟩) lty.le) ylt).elim

Result:
γ : Type v
inst✝¹ : SemilatticeSup γ
inst✝ : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₂ : a < x ⊔ a
y : γ
lty : a < y
ylt : y < x ⊔ a
⊢ x ≤ b

Proof state:
γ : Type v
inst✝¹ : SemilatticeSup γ
inst✝ : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₂ : a < x ⊔ a
y : γ
lty : a < y
ylt : y < x ⊔ a
⊢ x ≤ b

Tactic:
obtain ⟨u, au, ub⟩ := exists_between h

Result:
case intro.intro
γ : Type v
inst✝¹ : SemilatticeSup γ
inst✝ : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₂ : a < x ⊔ a
y : γ
lty : a < y
ylt : y < x ⊔ a
u : γ
au : a < u
ub : u < b
⊢ x ≤ b

Proof state:
γ : Type v
inst✝¹ : SemilatticeSup γ
inst✝ : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
⊢ x ≤ a

Tactic:
rcases eq_or_lt_of_le (le_sup_right : a ≤ x ⊔ a) with h₁ | h₂

Result:
case inl
γ : Type v
inst✝¹ : SemilatticeSup γ
inst✝ : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₁ : a = x ⊔ a
⊢ x ≤ a

case inr
γ : Type v
inst✝¹ : SemilatticeSup γ
inst✝ : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₂ : a < x ⊔ a
⊢ x ≤ a

Proof state:
case inl
γ : Type v
inst✝¹ : SemilatticeSup γ
inst✝ : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₁ : a = x ⊔ a
⊢ x ≤ a

Tactic:
exact h₁.symm ▸ le_sup_left

Result:
no goals

Proof state:
case intro.intro
γ : Type v
inst✝¹ : SemilatticeSup γ
inst✝ : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₂ : a < x ⊔ a
y : γ
lty : a < y
ylt : y < x ⊔ a
u : γ
au : a < u
ub : u < b
⊢ x ≤ b

Tactic:
apply (hx ⟨au, ub⟩).trans ub.le

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
protected lemma pow [StarOrderedRing R] [DecidableEq n]
    {M : Matrix n n R} (hM : M.PosSemidef) (k : ℕ) :
    PosSemidef (M ^ k) :=
  match k with
  | 0 => .one
  | 1 => by simpa using hM
  | (k + 2) => by
    rw [pow_succ, pow_succ']
    simpa only [hM.isHermitian.eq] using (hM.pow k).mul_mul_conjTranspose_same M

Proof state:
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
M : Matrix n n R
hM : M.PosSemidef
k : ℕ
⊢ (M ^ 1).PosSemidef

Tactic:
simpa using hM

Result:
no goals

Proof state:
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
M : Matrix n n R
hM : M.PosSemidef
k✝ k : ℕ
⊢ (M * M ^ k * M).PosSemidef

Tactic:
simpa only [hM.isHermitian.eq] using (hM.pow k).mul_mul_conjTranspose_same M

Result:
no goals

Proof state:
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
M : Matrix n n R
hM : M.PosSemidef
k✝ k : ℕ
⊢ (M ^ (k + 2)).PosSemidef

Tactic:
rw [pow_succ, pow_succ']

Result:
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
M : Matrix n n R
hM : M.PosSemidef
k✝ k : ℕ
⊢ (M * M ^ k * M).PosSemidef
-- Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean
theorem map_comp_c_app (F : J ⥤ PresheafedSpace.{_, _, v} C) {j₁ j₂ j₃}
    (f : j₁ ⟶ j₂) (g : j₂ ⟶ j₃) (U) :
    (F.map (f ≫ g)).c.app U =
      (F.map g).c.app U ≫
        ((pushforward C (F.map g).base).map (F.map f).c).app U ≫
          (pushforwardEq (congr_arg Hom.base (F.map_comp f g).symm) _).hom.app U

Proof state:
J : Type u'
inst✝¹ : Category.{v', u'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ PresheafedSpace C
j₁ j₂ j₃ : J
f : j₁ ⟶ j₂
g : j₂ ⟶ j₃
U : (Opens ↑↑(F.obj j₃))ᵒᵖ
⊢ (F.map (f ≫ g)).c.app U =
    (F.map g).c.app U ≫
      ((pushforward C (F.map g).base).map (F.map f).c).app U ≫ (pushforwardEq ⋯ (F.obj j₁).presheaf).hom.app U

Tactic:
simp [PresheafedSpace.congr_app (F.map_comp f g)]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem mul_singleton_mem_nhds_of_nhds_one (a : α) (h : s ∈ 𝓝 (1 : α)) : s * {a} ∈ 𝓝 a

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul αᵐᵒᵖ α
s : Set α
a : α
h : s ∈ 𝓝 1
⊢ s * {a} ∈ 𝓝 a

Tactic:
simpa only [one_mul] using mul_singleton_mem_nhds a h

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Coeff.lean
theorem support_map_of_injective [Semiring R] [Semiring S] (p : R[X]) {f : R →+* S}
    (hf : Function.Injective f) : (map f p).support = p.support

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : Function.Injective ⇑f
⊢ (map f p).support = p.support

Tactic:
simp_rw [Finset.ext_iff, mem_support_iff, coeff_map, ← map_zero f, hf.ne_iff,
  forall_const]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
lemma isStableUnderLimitsOfShape_iff_limitsOfShape_le :
    W.IsStableUnderLimitsOfShape J ↔ W.limitsOfShape J ≤ W

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{u_2, u_1} J
⊢ W.limitsOfShape J ≤ W → W.IsStableUnderLimitsOfShape J

Tactic:
intro h _ _ _ _ h₁ h₂ f hf

Result:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{u_2, u_1} J
h : W.limitsOfShape J ≤ W
X₁✝ X₂✝ : J ⥤ C
c₁✝ : Cone X₁✝
c₂✝ : Cone X₂✝
h₁ : IsLimit c₁✝
h₂ : IsLimit c₂✝
f : X₁✝ ⟶ X₂✝
hf : W.functorCategory J f
⊢ W (h₂.lift { pt := c₁✝.pt, π := c₁✝.π ≫ f })

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{u_2, u_1} J
h : W.limitsOfShape J ≤ W
X₁✝ X₂✝ : J ⥤ C
c₁✝ : Cone X₁✝
c₂✝ : Cone X₂✝
h₁ : IsLimit c₁✝
h₂ : IsLimit c₂✝
f : X₁✝ ⟶ X₂✝
hf : W.functorCategory J f
⊢ W (h₂.lift { pt := c₁✝.pt, π := c₁✝.π ≫ f })

Tactic:
exact h _ ⟨_, _, _, _, h₁, _, _, hf⟩

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{u_2, u_1} J
⊢ W.IsStableUnderLimitsOfShape J ↔ W.limitsOfShape J ≤ W

Tactic:
constructor

Result:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{u_2, u_1} J
⊢ W.IsStableUnderLimitsOfShape J → W.limitsOfShape J ≤ W

case mpr
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{u_2, u_1} J
⊢ W.limitsOfShape J ≤ W → W.IsStableUnderLimitsOfShape J

Proof state:
case mp.mk
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{u_2, u_1} J
h : W.IsStableUnderLimitsOfShape J
X Y : C
X₁✝ X₂✝ : J ⥤ C
c₁✝ : Cone X₁✝
c₂✝ : Cone X₂✝
h₁ : IsLimit c₁✝
h₂ : IsLimit c₂✝
f : X₁✝ ⟶ X₂✝
hf : W.functorCategory J f
⊢ W (h₂.lift { pt := c₁✝.pt, π := c₁✝.π ≫ f })

Tactic:
exact h _ _ _ _ h₁ h₂ f hf

Result:
no goals

Proof state:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{u_2, u_1} J
⊢ W.IsStableUnderLimitsOfShape J → W.limitsOfShape J ≤ W

Tactic:
rintro h _ _ _ ⟨_, _, _, _, h₁, h₂, f, hf⟩

Result:
case mp.mk
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{u_2, u_1} J
h : W.IsStableUnderLimitsOfShape J
X Y : C
X₁✝ X₂✝ : J ⥤ C
c₁✝ : Cone X₁✝
c₂✝ : Cone X₂✝
h₁ : IsLimit c₁✝
h₂ : IsLimit c₂✝
f : X₁✝ ⟶ X₂✝
hf : W.functorCategory J f
⊢ W (h₂.lift { pt := c₁✝.pt, π := c₁✝.π ≫ f })
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Cospan.lean
theorem cospanExt_hom_app_right :
    (cospanExt iX iY iZ wf wg).hom.app WalkingCospan.right = iY.hom

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iZ.hom
wg : iY.hom ≫ g' = g ≫ iZ.hom
⊢ (cospanExt iX iY iZ wf wg).hom.app WalkingCospan.right = iY.hom

Tactic:
dsimp [cospanExt]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem infEdist_le_edist_add_infEdist : infEdist x s ≤ edist x y + infEdist y s

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
s : Set α
⊢ infEdist x s ≤ edist x y + infEdist y s

Tactic:
rw [add_comm]

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
s : Set α
⊢ infEdist x s ≤ infEdist y s + edist x y

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
s : Set α
⊢ infEdist x s ≤ infEdist y s + edist x y

Tactic:
exact infEdist_le_infEdist_add_edist

Result:
no goals
-- Mathlib/Topology/Instances/NNReal/Lemmas.lean
theorem _root_.Real.tendsto_of_bddAbove_monotone {f : ℕ → ℝ} (h_bdd : BddAbove (Set.range f))
    (h_mon : Monotone f) : ∃ r : ℝ, Tendsto f atTop (𝓝 r)

Proof state:
f : ℕ → ℝ
h_bdd : BddAbove (range f)
h_mon : Monotone f
⊢ ∃ r, Tendsto f atTop (𝓝 r)

Tactic:
obtain ⟨B, hB⟩ := Real.exists_isLUB (Set.range_nonempty f) h_bdd

Result:
case intro
f : ℕ → ℝ
h_bdd : BddAbove (range f)
h_mon : Monotone f
B : ℝ
hB : IsLUB (range f) B
⊢ ∃ r, Tendsto f atTop (𝓝 r)

Proof state:
case intro
f : ℕ → ℝ
h_bdd : BddAbove (range f)
h_mon : Monotone f
B : ℝ
hB : IsLUB (range f) B
⊢ ∃ r, Tendsto f atTop (𝓝 r)

Tactic:
exact ⟨B, tendsto_atTop_isLUB h_mon hB⟩

Result:
no goals
-- Mathlib/Algebra/Lie/Character.lean
theorem lieCharacter_apply_lie' (χ : LieCharacter R L) (x y : L) : ⁅χ x, χ y⁆ = 0

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
χ : LieCharacter R L
x y : L
⊢ ⁅χ x, χ y⁆ = 0

Tactic:
rw [LieRing.of_associative_ring_bracket, mul_comm, sub_self]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Stalk.lean
lemma Spec_fromSpecStalk (R : CommRingCat) (x) :
    (Spec R).fromSpecStalk x =
      Spec.map ((ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial)

Proof state:
R : CommRingCat
x : ↑↑(Spec R).toPresheafedSpace
⊢ (Spec R).fromSpecStalk x = Spec.map ((ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial)

Tactic:
rw [← (isAffineOpen_top (Spec R)).fromSpecStalk_eq_fromSpecStalk (x := x) trivial,
  IsAffineOpen.fromSpecStalk, IsAffineOpen.fromSpec_top, isoSpec_Spec_inv,
  ← Spec.map_comp]

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
theorem other_invol {a : α} {z : Sym2 α} (ha : a ∈ z) (hb : Mem.other ha ∈ z) :
    Mem.other hb = a

Proof state:
case h.e'_2.h.e'_3
α : Type u_1
a : α
z : Sym2 α
ha : a ∈ z
hb✝ : Mem.other ha ∈ z
hb : Mem.other' ha ∈ z
⊢ Mem.other ha = Mem.other' ha

Tactic:
apply other_eq_other'

Result:
no goals

Proof state:
α : Type u_1
a : α
z : Sym2 α
ha : a ∈ z
hb : Mem.other ha ∈ z
⊢ Mem.other hb = a

Tactic:
rw [other_eq_other'] at hb ⊢

Result:
α : Type u_1
a : α
z : Sym2 α
ha : a ∈ z
hb✝ : Mem.other ha ∈ z
hb : Mem.other' ha ∈ z
⊢ Mem.other' hb✝ = a

Proof state:
α : Type u_1
a : α
z : Sym2 α
ha : a ∈ z
hb : Mem.other ha ∈ z
⊢ Mem.other hb = a

Tactic:
classical
  rw [other_eq_other'] at hb ⊢
  convert other_invol' ha hb using 2
  apply other_eq_other'

Result:
no goals

Proof state:
α : Type u_1
a : α
z : Sym2 α
ha : a ∈ z
hb✝ : Mem.other ha ∈ z
hb : Mem.other' ha ∈ z
⊢ Mem.other' hb✝ = a

Tactic:
convert other_invol' ha hb using 2

Result:
case h.e'_2.h.e'_3
α : Type u_1
a : α
z : Sym2 α
ha : a ∈ z
hb✝ : Mem.other ha ∈ z
hb : Mem.other' ha ∈ z
⊢ Mem.other ha = Mem.other' ha
-- Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
theorem singularPart_zero (μ : Measure α) : (0 : SignedMeasure α).singularPart μ = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ singularPart 0 μ = 0

Tactic:
refine (eq_singularPart 0 0 VectorMeasure.MutuallySingular.zero_left ?_).symm

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ 0 = 0 + μ.withDensityᵥ 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ 0 = 0 + μ.withDensityᵥ 0

Tactic:
rw [zero_add, withDensityᵥ_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
theorem _root_.MeasurableSet.of_mem_measurableCylinders {s : Set (Π i, α i)}
    (hs : s ∈ measurableCylinders α) : MeasurableSet s

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s : Set ((i : ι) → α i)
hs : s ∈ measurableCylinders α
⊢ MeasurableSet s

Tactic:
obtain ⟨I, t, mt, rfl⟩ := (mem_measurableCylinders s).1 hs

Result:
case intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
I : Finset ι
t : Set ((i : { x // x ∈ I }) → α ↑i)
mt : MeasurableSet t
hs : cylinder I t ∈ measurableCylinders α
⊢ MeasurableSet (cylinder I t)

Proof state:
case intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
I : Finset ι
t : Set ((i : { x // x ∈ I }) → α ↑i)
mt : MeasurableSet t
hs : cylinder I t ∈ measurableCylinders α
⊢ MeasurableSet (cylinder I t)

Tactic:
exact mt.cylinder

Result:
no goals
-- Mathlib/Data/Part.lean
theorem some_inter_some [Inter α] (a b : α) : some a ∩ some b = some (a ∩ b)

Proof state:
α : Type u_1
inst✝ : Inter α
a b : α
⊢ some a ∩ some b = some (a ∩ b)

Tactic:
simp [inter_def]

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred.lean
theorem sub_one_lt_iff_of_not_isMin (hx : ¬ IsMin x) : x - 1 < y ↔ x ≤ y

Proof state:
α : Type u_1
x y : α
inst✝³ : LinearOrder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
hx : ¬IsMin x
⊢ x - 1 < y ↔ x ≤ y

Tactic:
rw [← pred_eq_sub_one, pred_lt_iff_of_not_isMin hx]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_biUnion [DecidableEq α] {s : Finset γ} {t : γ → Finset α}
    (hs : Set.PairwiseDisjoint (↑s) t) : ∏ x ∈ s.biUnion t, f x = ∏ x ∈ s, ∏ i ∈ t x, f i

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset γ
t : γ → Finset α
hs : (↑s).PairwiseDisjoint t
⊢ ∏ x ∈ s.biUnion t, f x = ∏ x ∈ s, ∏ i ∈ t x, f i

Tactic:
rw [← disjiUnion_eq_biUnion _ _ hs, prod_disjiUnion]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_sign_sub_left (x y : V) : (o.oangle (x - y) y).sign = (o.oangle x y).sign

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ (o.oangle (x - y) y).sign = (o.oangle x y).sign

Tactic:
rw [← o.oangle_sign_sub_smul_left x y 1, one_smul]

Result:
no goals
-- Mathlib/Algebra/Algebra/Bilinear.lean
theorem mulRight_eq_zero_iff (a : A) : mulRight R a = 0 ↔ a = 0

Proof state:
case mpr
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : A
h : a = 0
⊢ mulRight R 0 = 0

Tactic:
exact mulRight_zero_eq_zero _ _

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : A
⊢ mulRight R a = 0 ↔ a = 0

Tactic:
constructor <;> intro h

Result:
case mp
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : A
h : mulRight R a = 0
⊢ a = 0

case mpr
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : A
h : a = 0
⊢ mulRight R a = 0

Proof state:
case mpr
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : A
h : a = 0
⊢ mulRight R a = 0

Tactic:
rw [h]

Result:
case mpr
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : A
h : a = 0
⊢ mulRight R 0 = 0

Proof state:
case mp
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : A
h : mulRight R a = 0
⊢ a = 0

Tactic:
rw [← one_mul a, ← mulRight_apply R a 1, h, LinearMap.zero_apply]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Split.lean
theorem congr_f {S₁ S₂ : Split C} {Φ₁ Φ₂ : S₁ ⟶ S₂} (h : Φ₁ = Φ₂) (n : ℕ) : Φ₁.f n = Φ₂.f n

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
S₁ S₂ : Split C
Φ₁ Φ₂ : S₁ ⟶ S₂
h : Φ₁ = Φ₂
n : ℕ
⊢ Φ₁.f n = Φ₂.f n

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Order/Defs/Unbundled.lean
theorem antisymm_iff [IsRefl α r] [IsAntisymm α r] {a b : α} : r a b ∧ r b a ↔ a = b :=
  ⟨fun h => antisymm h.1 h.2, by
    rintro rfl
    exact ⟨refl _, refl _⟩⟩

Proof state:
α : Type u_1
r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsAntisymm α r
a : α
⊢ r a a ∧ r a a

Tactic:
exact ⟨refl _, refl _⟩

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsAntisymm α r
a b : α
⊢ a = b → r a b ∧ r b a

Tactic:
rintro rfl

Result:
α : Type u_1
r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsAntisymm α r
a : α
⊢ r a a ∧ r a a
-- Mathlib/SetTheory/Cardinal/Finsupp.lean
theorem mk_finsupp_of_fintype (α β : Type u) [Fintype α] [Zero β] :
    #(α →₀ β) = #β ^ Fintype.card α

Proof state:
α β : Type u
inst✝¹ : Fintype α
inst✝ : Zero β
⊢ #(α →₀ β) = #β ^ Fintype.card α

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
theorem le_bind {α β : Type*} {f : α → Multiset β} (S : Multiset α) {x : α} (hx : x ∈ S) :
    f x ≤ S.bind f

Proof state:
case intro
α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
m' : Multiset ℕ
hm' : map (fun b => count a (f b)) S = (fun b => count a (f b)) x ::ₘ m'
⊢ count a (f x) ≤ (fun b => count a (f b)) x + m'.sum

Tactic:
exact Nat.le_add_right _ _

Result:
no goals

Proof state:
case intro
α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
m' : Multiset ℕ
hm' : map (fun b => count a (f b)) S = (fun b => count a (f b)) x ::ₘ m'
⊢ count a (f x) ≤ count a (S.bind f)

Tactic:
rw [count_bind, hm', sum_cons]

Result:
case intro
α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
m' : Multiset ℕ
hm' : map (fun b => count a (f b)) S = (fun b => count a (f b)) x ::ₘ m'
⊢ count a (f x) ≤ (fun b => count a (f b)) x + m'.sum

Proof state:
α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
⊢ f x ≤ S.bind f

Tactic:
refine le_iff_count.2 fun a ↦ ?_

Result:
α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
⊢ count a (f x) ≤ count a (S.bind f)

Proof state:
α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
⊢ f x ≤ S.bind f

Tactic:
classical
refine le_iff_count.2 fun a ↦ ?_
obtain ⟨m', hm'⟩ := exists_cons_of_mem <| mem_map_of_mem (fun b ↦ count a (f b)) hx
rw [count_bind, hm', sum_cons]
exact Nat.le_add_right _ _

Result:
no goals

Proof state:
α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
⊢ count a (f x) ≤ count a (S.bind f)

Tactic:
obtain ⟨m', hm'⟩ := exists_cons_of_mem <| mem_map_of_mem (fun b ↦ count a (f b)) hx

Result:
case intro
α : Type u_4
β : Type u_5
f : α → Multiset β
S : Multiset α
x : α
hx : x ∈ S
a : β
m' : Multiset ℕ
hm' : map (fun b => count a (f b)) S = (fun b => count a (f b)) x ::ₘ m'
⊢ count a (f x) ≤ count a (S.bind f)
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
@[reassoc (attr := simp)]
lemma f'_cyclesMap' : h₁.f' ≫ cyclesMap' φ h₁ h₂ = φ.τ₁ ≫ h₂.f'

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ h₁.f' ≫ cyclesMap' φ h₁ h₂ = φ.τ₁ ≫ h₂.f'

Tactic:
simp only [← cancel_mono h₂.i, assoc, φ.comm₁₂, cyclesMap'_i,
  LeftHomologyData.f'_i_assoc, LeftHomologyData.f'_i]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem comp_mul_right (x y : α) : (· * x) ∘ (· * y) = (· * (y * x))

Proof state:
case h
α : Type u_1
inst✝ : Semigroup α
x y z : α
⊢ ((fun x_1 => x_1 * x) ∘ fun x => x * y) z = z * (y * x)

Tactic:
simp [mul_assoc]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Semigroup α
x y : α
⊢ ((fun x_1 => x_1 * x) ∘ fun x => x * y) = fun x_1 => x_1 * (y * x)

Tactic:
ext z

Result:
case h
α : Type u_1
inst✝ : Semigroup α
x y z : α
⊢ ((fun x_1 => x_1 * x) ∘ fun x => x * y) z = z * (y * x)
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
lemma IsHermitian.posSemidef_of_eigenvalues_nonneg [DecidableEq n] {A : Matrix n n 𝕜}
    (hA : IsHermitian A) (h : ∀ i : n, 0 ≤ hA.eigenvalues i) : PosSemidef A

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
h : ∀ (i : n), 0 ≤ hA.eigenvalues i
⊢ (↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ hA.eigenvalues) * star ↑hA.eigenvectorUnitary).PosSemidef

Tactic:
refine (posSemidef_diagonal_iff.mpr ?_).mul_mul_conjTranspose_same _

Result:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
h : ∀ (i : n), 0 ≤ hA.eigenvalues i
⊢ ∀ (i : n), 0 ≤ (RCLike.ofReal ∘ hA.eigenvalues) i

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
h : ∀ (i : n), 0 ≤ hA.eigenvalues i
⊢ ∀ (i : n), 0 ≤ (RCLike.ofReal ∘ hA.eigenvalues) i

Tactic:
simpa using h

Result:
no goals

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
h : ∀ (i : n), 0 ≤ hA.eigenvalues i
⊢ A.PosSemidef

Tactic:
rw [hA.spectral_theorem]

Result:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
h : ∀ (i : n), 0 ≤ hA.eigenvalues i
⊢ (↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ hA.eigenvalues) * star ↑hA.eigenvectorUnitary).PosSemidef
-- Mathlib/Order/Lattice.lean
theorem sup_eq_iff_inf_eq : a ⊔ b = b ↔ a ⊓ b = a

Proof state:
α : Type u
inst✝ : Lattice α
a b : α
⊢ a ⊔ b = b ↔ a ⊓ b = a

Tactic:
rw [sup_eq_right, ← inf_eq_left]

Result:
no goals
-- Mathlib/Data/Multiset/Nodup.lean
theorem Nodup.erase_eq_filter [DecidableEq α] (a : α) {s} :
    Nodup s → s.erase a = Multiset.filter (· ≠ a) s :=
  Quot.induction_on s fun _ d =>
    congr_arg ((↑) : List α → Multiset α) <| by simpa using List.Nodup.erase_eq_filter d a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
x✝ : List α
d : Nodup (Quot.mk (⇑(isSetoid α)) x✝)
⊢ x✝.erase a = List.filter (fun b => decide ((fun x => x ≠ a) b)) x✝

Tactic:
simpa using List.Nodup.erase_eq_filter d a

Result:
no goals