harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/TypeVec.lean
theorem lastFun_toSubtype {α} (p : α ⟹ «repeat» (n + 1) Prop) :
    lastFun (toSubtype p) = _root_.id

Proof state:
case h.mk
n : ℕ
α : TypeVec.{u_1} (n + 1)
p : α ⟹ «repeat» (n + 1) Prop
val✝ : α Fin2.fz
property✝ : ofRepeat (p Fin2.fz val✝)
⊢ lastFun (toSubtype p) ⟨val✝, property✝⟩ = _root_.id ⟨val✝, property✝⟩

Tactic:
simp [dropFun, *]

Result:
case h.mk
n : ℕ
α : TypeVec.{u_1} (n + 1)
p : α ⟹ «repeat» (n + 1) Prop
val✝ : α Fin2.fz
property✝ : ofRepeat (p Fin2.fz val✝)
⊢ lastFun (toSubtype p) ⟨val✝, property✝⟩ = ⟨val✝, property✝⟩

Proof state:
n : ℕ
α : TypeVec.{u_1} (n + 1)
p : α ⟹ «repeat» (n + 1) Prop
⊢ lastFun (toSubtype p) = _root_.id

Tactic:
ext i : 2

Result:
case h
n : ℕ
α : TypeVec.{u_1} (n + 1)
p : α ⟹ «repeat» (n + 1) Prop
i : last fun i => { x // ofRepeat (p i x) }
⊢ lastFun (toSubtype p) i = _root_.id i

Proof state:
case h
n : ℕ
α : TypeVec.{u_1} (n + 1)
p : α ⟹ «repeat» (n + 1) Prop
i : last fun i => { x // ofRepeat (p i x) }
⊢ lastFun (toSubtype p) i = _root_.id i

Tactic:
induction i

Result:
case h.mk
n : ℕ
α : TypeVec.{u_1} (n + 1)
p : α ⟹ «repeat» (n + 1) Prop
val✝ : α Fin2.fz
property✝ : ofRepeat (p Fin2.fz val✝)
⊢ lastFun (toSubtype p) ⟨val✝, property✝⟩ = _root_.id ⟨val✝, property✝⟩

Proof state:
case h.mk
n : ℕ
α : TypeVec.{u_1} (n + 1)
p : α ⟹ «repeat» (n + 1) Prop
val✝ : α Fin2.fz
property✝ : ofRepeat (p Fin2.fz val✝)
⊢ lastFun (toSubtype p) ⟨val✝, property✝⟩ = ⟨val✝, property✝⟩

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean
/-- If `κ` is a suitable cardinal for the small object argument for `I : MorphismProperty C`,
then the class `I.rlp.llp` is exactly the class of morphisms that are retracts
of transfinite compositions of pushouts of coproducts of maps in `I`. -/
lemma llp_rlp_of_isCardinalForSmallObjectArgument :
    I.rlp.llp =
      (transfiniteCompositions.{w} (coproducts.{w} I).pushouts).retracts

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
⊢ ((coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape κ.ord.toType).retracts ≤
    (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} I).pushouts).retracts

Tactic:
apply retracts_monotone

Result:
case a
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
⊢ (coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape κ.ord.toType ≤
    transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} I).pushouts

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
⊢ I.rlp.llp = (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} I).pushouts).retracts

Tactic:
refine le_antisymm ?_
  (retracts_transfiniteComposition_pushouts_coproducts_le_llp_rlp I)

Result:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
⊢ I.rlp.llp ≤ (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} I).pushouts).retracts

Proof state:
case a
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
⊢ (coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape κ.ord.toType ≤
    transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} I).pushouts

Tactic:
apply transfiniteCompositionsOfShape_le_transfiniteCompositions

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
⊢ I.rlp.llp ≤ (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} I).pushouts).retracts

Tactic:
rw [llp_rlp_of_isCardinalForSmallObjectArgument' I κ]

Result:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
⊢ ((coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape κ.ord.toType).retracts ≤
    (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} I).pushouts).retracts
-- Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
theorem IsBoundedBilinearMap.isBigO (h : IsBoundedBilinearMap 𝕜 f) :
    f =O[⊤] fun p : E × F => ‖p.1‖ * ‖p.2‖ :=
  let ⟨C, _, hC⟩ := h.bound
  Asymptotics.IsBigO.of_bound C <|
    Filter.Eventually.of_forall fun ⟨x, y⟩ => by simpa [mul_assoc] using hC x y

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
C : ℝ
left✝ : C > 0
hC : ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖
x✝ : E × F
x : E
y : F
⊢ ‖f (x, y)‖ ≤ C * ‖‖(x, y).1‖ * ‖(x, y).2‖‖

Tactic:
simpa [mul_assoc] using hC x y

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem closedBall_add_closedBall_subset (p : Seminorm 𝕜 E) (r₁ r₂ : ℝ) (x₁ x₂ : E) :
    p.closedBall (x₁ : E) r₁ + p.closedBall (x₂ : E) r₂ ⊆ p.closedBall (x₁ + x₂) (r₁ + r₂)

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x₁ x₂ y₁ : E
hy₁ : y₁ ∈ p.closedBall x₁ r₁
y₂ : E
hy₂ : y₂ ∈ p.closedBall x₂ r₂
⊢ (fun x1 x2 => x1 + x2) y₁ y₂ ∈ p.closedBall (x₁ + x₂) (r₁ + r₂)

Tactic:
rw [mem_closedBall, add_sub_add_comm]

Result:
case intro.intro.intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x₁ x₂ y₁ : E
hy₁ : y₁ ∈ p.closedBall x₁ r₁
y₂ : E
hy₂ : y₂ ∈ p.closedBall x₂ r₂
⊢ p (y₁ - x₁ + (y₂ - x₂)) ≤ r₁ + r₂

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x₁ x₂ : E
⊢ p.closedBall x₁ r₁ + p.closedBall x₂ r₂ ⊆ p.closedBall (x₁ + x₂) (r₁ + r₂)

Tactic:
rintro x ⟨y₁, hy₁, y₂, hy₂, rfl⟩

Result:
case intro.intro.intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x₁ x₂ y₁ : E
hy₁ : y₁ ∈ p.closedBall x₁ r₁
y₂ : E
hy₂ : y₂ ∈ p.closedBall x₂ r₂
⊢ (fun x1 x2 => x1 + x2) y₁ y₂ ∈ p.closedBall (x₁ + x₂) (r₁ + r₂)

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
r₁ r₂ : ℝ
x₁ x₂ y₁ : E
hy₁ : y₁ ∈ p.closedBall x₁ r₁
y₂ : E
hy₂ : y₂ ∈ p.closedBall x₂ r₂
⊢ p (y₁ - x₁ + (y₂ - x₂)) ≤ r₁ + r₂

Tactic:
exact (map_add_le_add p _ _).trans (add_le_add hy₁ hy₂)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.lean
theorem blastArithShiftRight.go_decl_eq (aig : AIG α) (distance : AIG.RefVec aig n) (curr : Nat)
    (acc : AIG.RefVec aig w) :
    ∀ (idx : Nat) (h1) (h2),
        (go aig distance curr acc).aig.decls[idx]'h2 = aig.decls[idx]'h1

Proof state:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
n w : Nat
aig : AIG α
distance : aig.RefVec n
curr : Nat
acc : aig.RefVec w
res : AIG.RefVecEntry α w
h✝ : curr < n - 1
hgo :
  go (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig (distance.cast ⋯) (curr + 1)
      (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).vec =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size)
    (h2 :
      idx <
        (go (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig (distance.cast ⋯) (curr + 1)
                (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).vec).aig.decls.size),
    (go (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig (distance.cast ⋯) (curr + 1)
              (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).vec).aig.decls[idx] =
      aig.decls[idx]

Tactic:
intros

Result:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
n w : Nat
aig : AIG α
distance : aig.RefVec n
curr : Nat
acc : aig.RefVec w
res : AIG.RefVecEntry α w
h✝ : curr < n - 1
hgo :
  go (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig (distance.cast ⋯) (curr + 1)
      (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).vec =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig (distance.cast ⋯) (curr + 1)
            (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).vec).aig.decls.size
⊢ (go (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig (distance.cast ⋯) (curr + 1)
            (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).vec).aig.decls[idx✝] =
    aig.decls[idx✝]
-- Mathlib/Topology/Order/LeftRightNhds.lean
theorem Filter.Tendsto.add_atTop {C : α} (hf : Tendsto f l (𝓝 C)) (hg : Tendsto g l atTop) :
    Tendsto (fun x => f x + g x) l atTop

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
⊢ Tendsto (fun x => f x + g x) l atTop

Tactic:
nontriviality α

Result:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
a✝ : Nontrivial α
⊢ Tendsto (fun x => f x + g x) l atTop

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
a✝ : Nontrivial α
C' : α
hC' : C' < C
⊢ ∀ᶠ (x : β) in l, C' ≤ f x

Tactic:
exact (hf.eventually (lt_mem_nhds hC')).mono fun x => le_of_lt

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
a✝ : Nontrivial α
⊢ Tendsto (fun x => f x + g x) l atTop

Tactic:
obtain ⟨C', hC'⟩ : ∃ C', C' < C := exists_lt C

Result:
case intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
a✝ : Nontrivial α
C' : α
hC' : C' < C
⊢ Tendsto (fun x => f x + g x) l atTop

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
a✝ : Nontrivial α
C' : α
hC' : C' < C
⊢ Tendsto (fun x => f x + g x) l atTop

Tactic:
refine tendsto_atTop_add_left_of_le' _ C' ?_ hg

Result:
case intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
a✝ : Nontrivial α
C' : α
hC' : C' < C
⊢ ∀ᶠ (x : β) in l, C' ≤ f x
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_alter_eq_self_of_not_mem [LawfulBEq α] {k : α} {f : Option β → Option β}
    (h : m.WF) (h₁ : k ∉ m) (h₂ : (f (Const.get? m k)).isNone) :
    (Const.alter m k f).size = m.size

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝ : LawfulBEq α
k : α
f : Option β → Option β
h : m.WF
⊢ m.contains k = false → (f (get? m k)).isNone = true → (alter m k f).size = m.size

Tactic:
simp_to_raw using Raw₀.Const.size_alter_eq_self_of_not_mem

Result:
no goals

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝ : LawfulBEq α
k : α
f : Option β → Option β
h : m.WF
h₁ : ¬k ∈ m
h₂ : (f (get? m k)).isNone = true
⊢ (alter m k f).size = m.size

Tactic:
revert h₁ h₂

Result:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝ : LawfulBEq α
k : α
f : Option β → Option β
h : m.WF
⊢ ¬k ∈ m → (f (get? m k)).isNone = true → (alter m k f).size = m.size

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝ : LawfulBEq α
k : α
f : Option β → Option β
h : m.WF
⊢ ¬k ∈ m → (f (get? m k)).isNone = true → (alter m k f).size = m.size

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝ : LawfulBEq α
k : α
f : Option β → Option β
h : m.WF
⊢ m.contains k = false → (f (get? m k)).isNone = true → (alter m k f).size = m.size
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addZ_smul (P Q : Fin 3 → R) (u v : R) : addZ (u • P) (v • Q) = (u * v) ^ 2 * addZ P Q

Proof state:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
u v : R
⊢ addZ (u • P) (v • Q) = (u * v) ^ 2 * addZ P Q

Tactic:
simp only [addZ, smul_fin3_ext]

Result:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
u v : R
⊢ u ^ 2 * P x * (v * Q z) ^ 2 - v ^ 2 * Q x * (u * P z) ^ 2 = (u * v) ^ 2 * (P x * Q z ^ 2 - Q x * P z ^ 2)

Proof state:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
u v : R
⊢ u ^ 2 * P x * (v * Q z) ^ 2 - v ^ 2 * Q x * (u * P z) ^ 2 = (u * v) ^ 2 * (P x * Q z ^ 2 - Q x * P z ^ 2)

Tactic:
ring1

Result:
no goals
-- Mathlib/Algebra/Polynomial/RingDivision.lean
theorem Monic.neg_one_pow_natDegree_mul_comp_neg_X {p : R[X]} (hp : p.Monic) :
    ((-1) ^ p.natDegree * p.comp (-X)).Monic

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
hp : p.Monic
⊢ ((-1) ^ p.natDegree * p.comp (-X)).leadingCoeff = 1

Tactic:
calc
  ((-1) ^ p.natDegree * p.comp (-X)).leadingCoeff =
      (p.comp (-X) * C ((-1) ^ p.natDegree)).leadingCoeff := by
    simp [mul_comm]
  _ = 1 := by
    apply monic_mul_C_of_leadingCoeff_mul_eq_one
    simp [← pow_add, hp]

Result:
no goals

Proof state:
case hp
R : Type u
inst✝ : CommRing R
p : R[X]
hp : p.Monic
⊢ (p.comp (-X)).leadingCoeff * (-1) ^ p.natDegree = 1

Tactic:
simp [← pow_add, hp]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
hp : p.Monic
⊢ (p.comp (-X) * C ((-1) ^ p.natDegree)).leadingCoeff = 1

Tactic:
apply monic_mul_C_of_leadingCoeff_mul_eq_one

Result:
case hp
R : Type u
inst✝ : CommRing R
p : R[X]
hp : p.Monic
⊢ (p.comp (-X)).leadingCoeff * (-1) ^ p.natDegree = 1

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
hp : p.Monic
⊢ ((-1) ^ p.natDegree * p.comp (-X)).Monic

Tactic:
simp only [Monic]

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
hp : p.Monic
⊢ ((-1) ^ p.natDegree * p.comp (-X)).leadingCoeff = 1

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
hp : p.Monic
⊢ ((-1) ^ p.natDegree * p.comp (-X)).leadingCoeff = (p.comp (-X) * C ((-1) ^ p.natDegree)).leadingCoeff

Tactic:
simp [mul_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/Projectivization/Basic.lean
theorem submodule_injective :
    Function.Injective (Projectivization.submodule : ℙ K V → Submodule K V) := fun u v h ↦ by
  induction u using ind with | h u hu =>
  induction v using ind with | h v hv =>
  rw [submodule_mk, submodule_mk, Submodule.span_singleton_eq_span_singleton] at h
  exact ((mk_eq_mk_iff K v u hv hu).2 h).symm

Proof state:
case h.h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u : V
hu : u ≠ 0
v : V
hv : v ≠ 0
h : ∃ z, z • u = v
⊢ mk K u hu = mk K v hv

Tactic:
exact ((mk_eq_mk_iff K v u hv hu).2 h).symm

Result:
no goals

Proof state:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : ℙ K V
h : u.submodule = v.submodule
⊢ u = v

Tactic:
induction u using ind with | h u hu =>
induction v using ind with | h v hv =>
rw [submodule_mk, submodule_mk, Submodule.span_singleton_eq_span_singleton] at h
exact ((mk_eq_mk_iff K v u hv hu).2 h).symm

Result:
no goals

Proof state:
case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
u : V
hu : u ≠ 0
h : (mk K u hu).submodule = v.submodule
⊢ mk K u hu = v

Tactic:
induction v using ind with | h v hv =>
rw [submodule_mk, submodule_mk, Submodule.span_singleton_eq_span_singleton] at h
exact ((mk_eq_mk_iff K v u hv hu).2 h).symm

Result:
no goals

Proof state:
case h.h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u : V
hu : u ≠ 0
v : V
hv : v ≠ 0
h : (mk K u hu).submodule = (mk K v hv).submodule
⊢ mk K u hu = mk K v hv

Tactic:
rw [submodule_mk, submodule_mk, Submodule.span_singleton_eq_span_singleton] at h

Result:
case h.h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u : V
hu : u ≠ 0
v : V
hv : v ≠ 0
h : ∃ z, z • u = v
⊢ mk K u hu = mk K v hv
-- Mathlib/CategoryTheory/Opposites.lean
theorem unop_inv {X Y : Cᵒᵖ} (f : X ⟶ Y) [IsIso f] : (inv f).unop = inv f.unop

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : IsIso f
⊢ (inv f).unop = inv f.unop

Tactic:
apply IsIso.eq_inv_of_hom_inv_id

Result:
case hom_inv_id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : IsIso f
⊢ f.unop ≫ (inv f).unop = 𝟙 (unop Y)

Proof state:
case hom_inv_id
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : IsIso f
⊢ f.unop ≫ (inv f).unop = 𝟙 (unop Y)

Tactic:
rw [← unop_comp, IsIso.inv_hom_id, unop_id]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
@[to_additive]
lemma Submonoid.orderOf_le_card {G : Type*} [Group G] (s : Submonoid G) (hs : (s : Set G).Finite)
    {x} (hx : x ∈ s) : orderOf x ≤ Nat.card s

Proof state:
G : Type u_6
inst✝ : Group G
s : Submonoid G
hs : (↑s).Finite
x : G
hx : x ∈ s
⊢ orderOf x ≤ Nat.card ↥s

Tactic:
rw [← Nat.card_submonoidPowers]

Result:
G : Type u_6
inst✝ : Group G
s : Submonoid G
hs : (↑s).Finite
x : G
hx : x ∈ s
⊢ Nat.card ↥(powers x) ≤ Nat.card ↥s

Proof state:
G : Type u_6
inst✝ : Group G
s : Submonoid G
hs : (↑s).Finite
x : G
hx : x ∈ s
⊢ Nat.card ↥(powers x) ≤ Nat.card ↥s

Tactic:
exact Nat.card_mono hs <| powers_le.2 hx

Result:
no goals
-- Mathlib/Topology/Order/LeftRightNhds.lean
theorem TFAE_mem_nhdsGT {a b : α} (hab : a < b) (s : Set α) :
    TFAE [s ∈ 𝓝[>] a,
      s ∈ 𝓝[Ioc a b] a,
      s ∈ 𝓝[Ioo a b] a,
      ∃ u ∈ Ioc a b, Ioo a u ⊆ s,
      ∃ u ∈ Ioi a, Ioo a u ⊆ s]

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : (∃ u ∈ Ioc a b, Ioo a u ⊆ s) → ∃ u ∈ Ioi a, Ioo a u ⊆ s
tfae_5_to_1 : (∃ u ∈ Ioi a, Ioo a u ⊆ s) → s ∈ 𝓝[>] a
⊢ [s ∈ 𝓝[>] a, s ∈ 𝓝[Ioc a b] a, s ∈ 𝓝[Ioo a b] a, ∃ u ∈ Ioc a b, Ioo a u ⊆ s, ∃ u ∈ Ioi a, Ioo a u ⊆ s].TFAE

Tactic:
tfae_have 1 → 4
| h => by
  rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.1 h with ⟨v, va, hv⟩
  rcases exists_Ico_subset_of_mem_nhds' va hab with ⟨u, au, hu⟩
  exact ⟨u, au, fun x hx => hv ⟨hu ⟨le_of_lt hx.1, hx.2⟩, hx.1⟩⟩

Result:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : (∃ u ∈ Ioc a b, Ioo a u ⊆ s) → ∃ u ∈ Ioi a, Ioo a u ⊆ s
tfae_5_to_1 : (∃ u ∈ Ioi a, Ioo a u ⊆ s) → s ∈ 𝓝[>] a
tfae_1_to_4 : s ∈ 𝓝[>] a → ∃ u ∈ Ioc a b, Ioo a u ⊆ s
⊢ [s ∈ 𝓝[>] a, s ∈ 𝓝[Ioc a b] a, s ∈ 𝓝[Ioo a b] a, ∃ u ∈ Ioc a b, Ioo a u ⊆ s, ∃ u ∈ Ioi a, Ioo a u ⊆ s].TFAE
-- Mathlib/Data/ENNReal/Inv.lean
theorem div_lt_of_lt_mul' (h : a < b * c) : a / b < c :=
  div_lt_of_lt_mul <| by rwa [mul_comm]

Proof state:
a b c : ℝ≥0∞
h : a < b * c
⊢ a < c * b

Tactic:
rwa [mul_comm]

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
theorem one_sub_div_pow_le_exp_neg {n : ℕ} {t : ℝ} (ht' : t ≤ n) : (1 - t / n) ^ n ≤ exp (-t)

Proof state:
case hab
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ 1 - t / ↑n ≤ rexp (-(t / ↑n))

Tactic:
exact one_sub_le_exp_neg _

Result:
no goals

Proof state:
case inl
t : ℝ
ht' : t ≤ ↑0
⊢ (1 - t / ↑0) ^ 0 ≤ rexp (-t)

Tactic:
simp

Result:
case inl
t : ℝ
ht' : t ≤ ↑0
⊢ t ≤ 0

Proof state:
case ha
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ 0 ≤ 1 - t / ↑n

Tactic:
exact sub_nonneg.2 <| div_le_one_of_le₀ ht' n.cast_nonneg

Result:
no goals

Proof state:
n : ℕ
t : ℝ
ht' : t ≤ ↑n
⊢ (1 - t / ↑n) ^ n ≤ rexp (-t)

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Result:
case inl
t : ℝ
ht' : t ≤ ↑0
⊢ (1 - t / ↑0) ^ 0 ≤ rexp (-t)

case inr
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ (1 - t / ↑n) ^ n ≤ rexp (-t)

Proof state:
case inl
t : ℝ
ht' : t ≤ ↑0
⊢ t ≤ 0

Tactic:
rwa [Nat.cast_zero] at ht'

Result:
no goals

Proof state:
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ (1 - t / ↑n) ^ n ≤ rexp (-(t / ↑n)) ^ n

Tactic:
gcongr

Result:
case ha
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ 0 ≤ 1 - t / ↑n

case hab
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ 1 - t / ↑n ≤ rexp (-(t / ↑n))

Proof state:
case h
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ ↑n ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ rexp (-(t / ↑n)) ^ n = rexp (-t)

Tactic:
rw [← Real.exp_nat_mul, mul_neg, mul_comm, div_mul_cancel₀]

Result:
case h
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ ↑n ≠ 0