harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/Block.lean
theorem blockTriangular_stdBasisMatrix' {i j : m} (hij : b j ≤ b i) (c : R) :
    BlockTriangular (stdBasisMatrix i j c) (toDual ∘ b) :=
  blockTriangular_stdBasisMatrix (by exact toDual_le_toDual.mpr hij) _

Proof state:
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq m
i j : m
hij : b j ≤ b i
c : R
⊢ (⇑toDual ∘ b) i ≤ (⇑toDual ∘ b) j

Tactic:
exact toDual_le_toDual.mpr hij

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addXYZ_of_Z_ne_zero {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z ≠ Q x * P z) : W.addXYZ P Q = W.addZ P Q •
      ![W.toAffine.addX (P x / P z) (Q x / Q z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)), 1]

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
hZ : IsUnit (W.addZ P Q)
⊢ W.addXYZ P Q =
    W.addZ P Q •
      ![(toAffine W).addX (P x / P z) (Q x / Q z) ((toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        (toAffine W).addY (P x / P z) (Q x / Q z) (P y / P z)
          ((toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1]

Tactic:
erw [addXYZ, smul_fin3, ← addX_of_Z_ne_zero hP hQ hPz hQz hx, hZ.mul_div_cancel,
  ← addY_of_Z_ne_zero hP hQ hPz hQz hx, hZ.mul_div_cancel, mul_one]

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
⊢ W.addXYZ P Q =
    W.addZ P Q •
      ![(toAffine W).addX (P x / P z) (Q x / Q z) ((toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        (toAffine W).addY (P x / P z) (Q x / Q z) (P y / P z)
          ((toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1]

Tactic:
have hZ : IsUnit <| W.addZ P Q := isUnit_addZ_of_X_ne hP hQ hx

Result:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
hZ : IsUnit (W.addZ P Q)
⊢ W.addXYZ P Q =
    W.addZ P Q •
      ![(toAffine W).addX (P x / P z) (Q x / Q z) ((toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        (toAffine W).addY (P x / P z) (Q x / Q z) (P y / P z)
          ((toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1]
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem le_of_mul_le_mul_right {a b c : Int} (w : b * a ≤ c * a) (h : 0 < a) : b ≤ c

Proof state:
a b c : Int
w : b * a ≤ c * a
h : 0 < a
⊢ b ≤ c

Tactic:
rw [Int.mul_comm b, Int.mul_comm c] at w

Result:
a b c : Int
w : a * b ≤ a * c
h : 0 < a
⊢ b ≤ c

Proof state:
a b c : Int
w : a * b ≤ a * c
h : 0 < a
⊢ b ≤ c

Tactic:
exact le_of_mul_le_mul_left w h

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem diam_Ico {a b : ℝ} (h : a ≤ b) : Metric.diam (Ico a b) = b - a

Proof state:
a b : ℝ
h : a ≤ b
⊢ Metric.diam (Ico a b) = b - a

Tactic:
simp [Metric.diam, ENNReal.toReal_ofReal (sub_nonneg.2 h)]

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem filter_eq_indicator : ⇑(f.filter p) = Set.indicator { x | p x } f

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
p : α → Prop
inst✝ : DecidablePred p
f : α →₀ M
⊢ ⇑(filter p f) = {x | p x}.indicator ⇑f

Tactic:
ext

Result:
case h
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
p : α → Prop
inst✝ : DecidablePred p
f : α →₀ M
x✝ : α
⊢ (filter p f) x✝ = {x | p x}.indicator (⇑f) x✝

Proof state:
case h
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
p : α → Prop
inst✝ : DecidablePred p
f : α →₀ M
x✝ : α
⊢ (filter p f) x✝ = {x | p x}.indicator (⇑f) x✝

Tactic:
simp [filter_apply, Set.indicator_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basis.lean
@[simp]
lemma Basis.baseChange_apply (b : Basis ι R M) (i) :
    b.baseChange S i = 1 ⊗ₜ b i

Proof state:
R : Type u_1
M : Type u_3
ι : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_7
inst✝¹ : Semiring S
inst✝ : Algebra R S
b : Basis ι R M
i : ι
⊢ (baseChange S b) i = 1 ⊗ₜ[R] b i

Tactic:
simp [Basis.baseChange, Basis.tensorProduct]

Result:
no goals
-- Mathlib/Data/Matrix/Rank.lean
/-- Right multiplying by an invertible matrix does not change the rank -/
@[simp]
lemma rank_mul_eq_left_of_isUnit_det [DecidableEq n]
    (A : Matrix n n R) (B : Matrix m n R) (hA : IsUnit A.det) :
    (B * A).rank = B.rank

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix n n R
B : Matrix m n R
hA : IsUnit A.det
⊢ (B * A).rank = B.rank

Tactic:
suffices Function.Surjective A.mulVecLin by
  rw [rank, mulVecLin_mul, LinearMap.range_comp_of_range_eq_top _
    (LinearMap.range_eq_top.mpr this), ← rank]

Result:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix n n R
B : Matrix m n R
hA : IsUnit A.det
⊢ Function.Surjective ⇑A.mulVecLin

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix n n R
B : Matrix m n R
hA : IsUnit A.det
v : n → R
⊢ ∃ a, A.mulVecLin a = v

Tactic:
exact ⟨(A⁻¹).mulVecLin v, by simp [mul_nonsing_inv _ hA]⟩

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix n n R
B : Matrix m n R
hA : IsUnit A.det
this : Function.Surjective ⇑A.mulVecLin
⊢ (B * A).rank = B.rank

Tactic:
rw [rank, mulVecLin_mul, LinearMap.range_comp_of_range_eq_top _
  (LinearMap.range_eq_top.mpr this), ← rank]

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix n n R
B : Matrix m n R
hA : IsUnit A.det
v : n → R
⊢ A.mulVecLin (A⁻¹.mulVecLin v) = v

Tactic:
simp [mul_nonsing_inv _ hA]

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix n n R
B : Matrix m n R
hA : IsUnit A.det
⊢ Function.Surjective ⇑A.mulVecLin

Tactic:
intro v

Result:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix n n R
B : Matrix m n R
hA : IsUnit A.det
v : n → R
⊢ ∃ a, A.mulVecLin a = v
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma pow_lt_self_of_lt_one₀ (h₀ : 0 < a) (h₁ : a < 1) (hn : 1 < n) : a ^ n < a

Proof state:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : PartialOrder M₀
a : M₀
n : ℕ
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulStrictMono M₀
inst✝ : MulPosStrictMono M₀
h₀ : 0 < a
h₁ : a < 1
hn : 1 < n
⊢ a ^ n < a

Tactic:
simpa only [pow_one] using pow_lt_pow_right_of_lt_one₀ h₀ h₁ hn

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
theorem semilength_insidePart_lt : p.insidePart.semilength < p.semilength

Proof state:
p : DyckWord
h : p ≠ 0
⊢ p.insidePart.semilength < p.semilength

Tactic:
have := semilength_insidePart_add_semilength_outsidePart_add_one h

Result:
p : DyckWord
h : p ≠ 0
this : p.insidePart.semilength + p.outsidePart.semilength + 1 = p.semilength
⊢ p.insidePart.semilength < p.semilength

Proof state:
p : DyckWord
h : p ≠ 0
this : p.insidePart.semilength + p.outsidePart.semilength + 1 = p.semilength
⊢ p.insidePart.semilength < p.semilength

Tactic:
omega

Result:
no goals
-- Mathlib/Topology/Instances/AddCircle.lean
theorem toIcoMod_eventuallyEq_toIocMod (hx : (x : 𝕜 ⧸ zmultiples p) ≠ a) :
    toIcoMod hp a =ᶠ[𝓝 x] toIocMod hp a :=
  IsOpen.mem_nhds
      (by
        rw [Ico_eq_locus_Ioc_eq_iUnion_Ioo]
        exact isOpen_iUnion fun i => isOpen_Ioo) <|
    (not_modEq_iff_toIcoMod_eq_toIocMod hp).1 <| not_modEq_iff_ne_mod_zmultiples.2 hx

Proof state:
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ↑x ≠ ↑a
⊢ IsOpen (⋃ z, Ioo (a + z • p) (a + p + z • p))

Tactic:
exact isOpen_iUnion fun i => isOpen_Ioo

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ↑x ≠ ↑a
⊢ IsOpen {x | (fun x => toIcoMod hp a x = toIocMod hp a x) x}

Tactic:
rw [Ico_eq_locus_Ioc_eq_iUnion_Ioo]

Result:
𝕜 : Type u_1
inst✝³ : LinearOrderedAddCommGroup 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ↑x ≠ ↑a
⊢ IsOpen (⋃ z, Ioo (a + z • p) (a + p + z • p))
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
theorem basicOpen_mul (f g : A) : basicOpen 𝒜 (f * g) = basicOpen 𝒜 f ⊓ basicOpen 𝒜 g :=
  TopologicalSpace.Opens.ext <| by simp [zeroLocus_singleton_mul]

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f g : A
⊢ ↑(basicOpen 𝒜 (f * g)) = ↑(basicOpen 𝒜 f ⊓ basicOpen 𝒜 g)

Tactic:
simp [zeroLocus_singleton_mul]

Result:
no goals
-- Mathlib/Dynamics/Ergodic/Ergodic.lean
theorem prob_eq_zero_or_one [IsProbabilityMeasure μ] (hf : PreErgodic f μ) (hs : MeasurableSet s)
    (hs' : f ⁻¹' s = s) : μ s = 0 ∨ μ s = 1

Proof state:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
hf : PreErgodic f μ
hs : MeasurableSet s
hs' : f ⁻¹' s = s
⊢ μ s = 0 ∨ μ s = 1

Tactic:
simpa [hs] using hf.measure_self_or_compl_eq_zero hs hs'

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_singleton [MeasurableSingletonClass α] {μ : Measure α} (f : α → E) (a : α) :
    ∫ a in {a}, f a ∂μ = (μ {a}).toReal • f a

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
f : α → E
a : α
⊢ ∫ (a : α) in {a}, f a ∂μ = (μ {a}).toReal • f a

Tactic:
simp only [Measure.restrict_singleton, integral_smul_measure, integral_dirac]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey?_eq_none [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a : α}
    (h : containsKey a l = false) : getKey? a l = none

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a : α
h : containsKey a l = false
⊢ getKey? a l = none

Tactic:
rwa [← Option.not_isSome_iff_eq_none, ← containsKey_eq_isSome_getKey?, Bool.not_eq_true]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/If.lean
theorem go_get {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (discr : Ref aig)
    (lhs rhs : RefVec aig w) (s : RefVec aig curr) :
    ∀ (idx : Nat) (hidx : idx < curr),
      (go aig curr hcurr discr lhs rhs s).vec.get idx (by omega)
        =
      (s.get idx hidx).cast (by apply go_le_size)

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
discr : aig.Ref
lhs rhs : aig.RefVec w
s : aig.RefVec curr
idx : Nat
hidx : idx < curr
⊢ aig.decls.size ≤ (go aig curr hcurr discr lhs rhs s).aig.decls.size

Tactic:
apply go_le_size

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
discr : aig.Ref
lhs rhs : aig.RefVec w
s : aig.RefVec curr
idx : Nat
hidx : idx < curr
⊢ idx < w

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
discr : aig.Ref
lhs rhs : aig.RefVec w
s : aig.RefVec curr
idx : Nat
hidx : idx < curr
⊢ (go aig curr hcurr discr lhs rhs s).vec.get idx ⋯ = (s.get idx hidx).cast ⋯

Tactic:
apply go_get_aux

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
discr : aig.Ref
lhs rhs : aig.RefVec w
s : aig.RefVec curr
⊢ ∀ (idx : Nat) (hidx : idx < curr), (go aig curr hcurr discr lhs rhs s).vec.get idx ⋯ = (s.get idx hidx).cast ⋯

Tactic:
intro idx hidx

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
discr : aig.Ref
lhs rhs : aig.RefVec w
s : aig.RefVec curr
idx : Nat
hidx : idx < curr
⊢ (go aig curr hcurr discr lhs rhs s).vec.get idx ⋯ = (s.get idx hidx).cast ⋯
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem kahler_rightAngleRotation_right (x y : E) :
    o.kahler x (J y) = Complex.I * o.kahler x y

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ -↑((o.areaForm x) y) + ↑(inner x y) * Complex.I = Complex.I * (↑(inner x y) + ↑((o.areaForm x) y) * Complex.I)

Tactic:
linear_combination -ω x y * Complex.I_sq

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ (o.kahler x) (o.rightAngleRotation y) = Complex.I * (o.kahler x) y

Tactic:
simp only [o.areaForm_rightAngleRotation_right, o.inner_rightAngleRotation_right,
  o.kahler_apply_apply, Complex.ofReal_neg, Complex.real_smul]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ -↑((o.areaForm x) y) + ↑(inner x y) * Complex.I = Complex.I * (↑(inner x y) + ↑((o.areaForm x) y) * Complex.I)
-- Mathlib/Data/Real/Irrational.lean
theorem Transcendental.irrational {r : ℝ} (tr : Transcendental ℚ r) : Irrational r

Proof state:
case intro
a : ℚ
tr : Transcendental ℚ ↑a
⊢ False

Tactic:
exact tr (isAlgebraic_algebraMap a)

Result:
no goals

Proof state:
r : ℝ
tr : Transcendental ℚ r
⊢ Irrational r

Tactic:
rintro ⟨a, rfl⟩

Result:
case intro
a : ℚ
tr : Transcendental ℚ ↑a
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem countP_singleton (a : α) : countP p [a] = if p a then 1 else 0

Proof state:
α : Type u_1
p : α → Bool
a : α
⊢ countP p [a] = if p a = true then 1 else 0

Tactic:
simp [countP_cons]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma Even.sub_odd (ha : Even a) (hb : Odd b) : Odd (a - b)

Proof state:
α : Type u_2
inst✝ : Ring α
a b : α
ha : Even a
hb : Odd b
⊢ Odd (a + -b)

Tactic:
exact ha.add_odd hb.neg

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Ring α
a b : α
ha : Even a
hb : Odd b
⊢ Odd (a - b)

Tactic:
rw [sub_eq_add_neg]

Result:
α : Type u_2
inst✝ : Ring α
a b : α
ha : Even a
hb : Odd b
⊢ Odd (a + -b)
-- Mathlib/Data/DFinsupp/Multiset.lean
theorem toDFinsupp_singleton (a : α) : toDFinsupp {a} = DFinsupp.single a 1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
⊢ toDFinsupp {a} = DFinsupp.single a 1

Tactic:
rw [← replicate_one, toDFinsupp_replicate]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Restrict.lean
@[simp]
lemma Scheme.homOfLE_rfl (X : Scheme.{u}) (U : X.Opens) : X.homOfLE (refl U) = 𝟙 _

Proof state:
X : Scheme
U : X.Opens
⊢ X.homOfLE ⋯ = 𝟙 ↑U

Tactic:
rw [← cancel_mono U.ι, Scheme.homOfLE_ι, Category.id_comp]

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
/-- Binary strict **rearrangement inequality**. -/
lemma smul_add_smul_lt_smul_add_smul (ha : a₁ < a₂) (hb : b₁ < b₂) :
    a₁ • b₂ + a₂ • b₁ < a₁ • b₁ + a₂ • b₂

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : StrictOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a₁ : α
b₁ b₂ : β
hb : b₁ < b₂
a : α
ha₀ : 0 < a
ha : a₁ < a₁ + a
⊢ a₁ • b₁ + (a₁ • b₂ + a • b₁) < a₁ • b₁ + (a₁ • b₂ + a • b₂)

Tactic:
gcongr

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : StrictOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ < a₂
hb : b₁ < b₂
⊢ a₁ • b₂ + a₂ • b₁ < a₁ • b₁ + a₂ • b₂

Tactic:
obtain ⟨a, ha₀, rfl⟩ := lt_iff_exists_pos_add.1 ha

Result:
case intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : StrictOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a₁ : α
b₁ b₂ : β
hb : b₁ < b₂
a : α
ha₀ : 0 < a
ha : a₁ < a₁ + a
⊢ a₁ • b₂ + (a₁ + a) • b₁ < a₁ • b₁ + (a₁ + a) • b₂

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : StrictOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a₁ : α
b₁ b₂ : β
hb : b₁ < b₂
a : α
ha₀ : 0 < a
ha : a₁ < a₁ + a
⊢ a₁ • b₂ + (a₁ + a) • b₁ < a₁ • b₁ + (a₁ + a) • b₂

Tactic:
rw [add_smul, add_smul, add_left_comm]

Result:
case intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : StrictOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a₁ : α
b₁ b₂ : β
hb : b₁ < b₂
a : α
ha₀ : 0 < a
ha : a₁ < a₁ + a
⊢ a₁ • b₁ + (a₁ • b₂ + a • b₁) < a₁ • b₁ + (a₁ • b₂ + a • b₂)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filter_push_of_neg {p : α → Bool} {a : α} {l : Array α}
    (h : ¬p a) (w : stop = l.size + 1) :
    (l.push a).filter p 0 stop = l.filter p

Proof state:
α : Type u_1
p : α → Bool
a : α
l : Array α
h : ¬p a = true
⊢ filter p (l.push a) 0 (l.size + 1) = filter p l

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
p : α → Bool
a : α
h : ¬p a = true
l : List α
⊢ filter p ({ toList := l }.push a) 0 ({ toList := l }.size + 1) = filter p { toList := l }

Proof state:
case mk
α : Type u_1
p : α → Bool
a : α
h : ¬p a = true
l : List α
⊢ filter p ({ toList := l }.push a) 0 ({ toList := l }.size + 1) = filter p { toList := l }

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
stop : Nat
p : α → Bool
a : α
l : Array α
h : ¬p a = true
w : stop = l.size + 1
⊢ filter p (l.push a) 0 stop = filter p l

Tactic:
subst w

Result:
α : Type u_1
p : α → Bool
a : α
l : Array α
h : ¬p a = true
⊢ filter p (l.push a) 0 (l.size + 1) = filter p l
-- Mathlib/Order/LiminfLimsup.lean
theorem iInf_le_liminf {f : Filter β} {u : β → α} : ⨅ n, u n ≤ liminf u f :=
  le_liminf_of_le (by isBoundedDefault) (Eventually.of_forall (iInf_le u))

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
u : β → α
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f u

Tactic:
isBoundedDefault

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
theorem convexBodyLT_neg_mem (x : mixedSpace K) (hx : x ∈ (convexBodyLT K f)) :
    -x ∈ (convexBodyLT K f)

Proof state:
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
x : mixedSpace K
hx :
  (∀ (a : InfinitePlace K) (b : a.IsReal), |x.1 ⟨a, b⟩| < ↑(f a)) ∧
    ∀ (a : InfinitePlace K) (b : a.IsComplex), ‖x.2 ⟨a, b⟩‖ < ↑(f a)
⊢ (∀ (a : InfinitePlace K) (b : a.IsReal), |x.1 ⟨a, b⟩| < ↑(f a)) ∧
    ∀ (a : InfinitePlace K) (b : a.IsComplex), ‖x.2 ⟨a, b⟩‖ < ↑(f a)

Tactic:
exact hx

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
x : mixedSpace K
hx : x ∈ convexBodyLT K f
⊢ -x ∈ convexBodyLT K f

Tactic:
simp only [Set.mem_prod, Prod.fst_neg, Set.mem_pi, Set.mem_univ, Pi.neg_apply,
  mem_ball_zero_iff, norm_neg, Real.norm_eq_abs, forall_true_left, Subtype.forall,
  Prod.snd_neg] at hx ⊢

Result:
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
x : mixedSpace K
hx :
  (∀ (a : InfinitePlace K) (b : a.IsReal), |x.1 ⟨a, b⟩| < ↑(f a)) ∧
    ∀ (a : InfinitePlace K) (b : a.IsComplex), ‖x.2 ⟨a, b⟩‖ < ↑(f a)
⊢ (∀ (a : InfinitePlace K) (b : a.IsReal), |x.1 ⟨a, b⟩| < ↑(f a)) ∧
    ∀ (a : InfinitePlace K) (b : a.IsComplex), ‖x.2 ⟨a, b⟩‖ < ↑(f a)
-- Mathlib/CategoryTheory/Monoidal/Braided/Opposite.lean
@[simp] lemma op_tensorμ {C : Type*} [Category C] [MonoidalCategory C]
    [BraidedCategory C] (X Y W Z : C) :
    (tensorμ X W Y Z).op = tensorμ (op X) (op Y) (op W) (op Z)

Proof state:
C : Type u_2
inst✝² : Category.{u_3, u_2} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y W Z : C
⊢ (tensorμ X W Y Z).op = tensorμ (op X) (op Y) (op W) (op Z)

Tactic:
simp only [op_tensorObj, tensorμ, op_comp, op_inv_associator, op_whiskerLeft, op_hom_associator,
  op_whiskerRight, op_hom_braiding, Category.assoc]

Result:
no goals
-- Mathlib/Tactic/NormNum/BigOperators.lean
lemma Finset.range_zero' {n : ℕ} (pn : NormNum.IsNat n 0) :
    Finset.range n = {}

Proof state:
n : ℕ
pn : NormNum.IsNat n 0
⊢ Finset.range n = ∅

Tactic:
rw [pn.out, Nat.cast_zero, Finset.range_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem push_eq_push {a b : α} {xs ys : Vector α n} : xs.push a = ys.push b ↔ a = b ∧ xs = ys

Proof state:
case mp
α : Type u_1
n : Nat
a b : α
xs ys : Vector α n
⊢ xs.push a = ys.push b → a = b ∧ xs = ys

Tactic:
intro h

Result:
case mp
α : Type u_1
n : Nat
a b : α
xs ys : Vector α n
h : xs.push a = ys.push b
⊢ a = b ∧ xs = ys

Proof state:
case mpr
α : Type u_1
n : Nat
a b : α
xs ys : Vector α n
⊢ a = b ∧ xs = ys → xs.push a = ys.push b

Tactic:
rintro ⟨rfl, rfl⟩

Result:
case mpr.intro
α : Type u_1
n : Nat
a : α
xs : Vector α n
⊢ xs.push a = xs.push a

Proof state:
α : Type u_1
n : Nat
a b : α
xs ys : Vector α n
⊢ xs.push a = ys.push b ↔ a = b ∧ xs = ys

Tactic:
constructor

Result:
case mp
α : Type u_1
n : Nat
a b : α
xs ys : Vector α n
⊢ xs.push a = ys.push b → a = b ∧ xs = ys

case mpr
α : Type u_1
n : Nat
a b : α
xs ys : Vector α n
⊢ a = b ∧ xs = ys → xs.push a = ys.push b

Proof state:
case mp
α : Type u_1
n : Nat
a b : α
xs ys : Vector α n
h : xs.push a = ys.push b
⊢ a = b ∧ xs = ys

Tactic:
exact ⟨back_eq_of_push_eq h, pop_eq_of_push_eq h⟩

Result:
no goals

Proof state:
case mpr.intro
α : Type u_1
n : Nat
a : α
xs : Vector α n
⊢ xs.push a = xs.push a

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem one_lt_succ_succ (a : Fin n) : (1 : Fin (n + 2)) < a.succ.succ

Proof state:
n✝ n : Nat
a : Fin (n + 1)
⊢ 1 < a.succ.succ

Tactic:
rw [← succ_zero_eq_one, succ_lt_succ_iff]

Result:
n✝ n : Nat
a : Fin (n + 1)
⊢ 0 < a.succ

Proof state:
n✝ n : Nat
a : Fin (n + 1)
⊢ 0 < a.succ

Tactic:
exact succ_pos a

Result:
no goals

Proof state:
n : Nat
a : Fin n
⊢ 1 < a.succ.succ

Tactic:
let n+1 := n

Result:
n✝ n : Nat
a : Fin (n + 1)
⊢ 1 < a.succ.succ
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem restrict_empty : v.restrict ∅ = 0 :=
  ext fun i hi => by
    rw [restrict_apply v MeasurableSet.empty hi, Set.inter_empty, v.empty, zero_apply]

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ ↑(v.restrict ∅) i = ↑0 i

Tactic:
rw [restrict_apply v MeasurableSet.empty hi, Set.inter_empty, v.empty, zero_apply]

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem ascFactorial_le_pow_add (n : ℕ) : ∀ k : ℕ, (n+1).ascFactorial k ≤ (n + k) ^ k
  | 0 => by rw [ascFactorial_zero, Nat.pow_zero]
  | k + 1 => by
    rw [ascFactorial_succ, Nat.pow_succ, Nat.mul_comm, ← Nat.add_assoc, Nat.add_right_comm n 1 k]
    exact Nat.mul_le_mul_right _
      (Nat.le_trans (ascFactorial_le_pow_add _ k) (Nat.pow_le_pow_left (le_succ _) _))

Proof state:
n k : ℕ
⊢ (n + 1).ascFactorial (k + 1) ≤ (n + (k + 1)) ^ (k + 1)

Tactic:
rw [ascFactorial_succ, Nat.pow_succ, Nat.mul_comm, ← Nat.add_assoc, Nat.add_right_comm n 1 k]

Result:
n k : ℕ
⊢ (n + 1).ascFactorial k * (n + k + 1) ≤ (n + k + 1) ^ k * (n + k + 1)

Proof state:
n k : ℕ
⊢ (n + 1).ascFactorial k * (n + k + 1) ≤ (n + k + 1) ^ k * (n + k + 1)

Tactic:
exact Nat.mul_le_mul_right _
  (Nat.le_trans (ascFactorial_le_pow_add _ k) (Nat.pow_le_pow_left (le_succ _) _))

Result:
no goals

Proof state:
n : ℕ
⊢ (n + 1).ascFactorial 0 ≤ (n + 0) ^ 0

Tactic:
rw [ascFactorial_zero, Nat.pow_zero]

Result:
no goals