harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/InnerProductSpace/Orthogonal.lean
theorem IsOrtho.comap (f : E →ₗᵢ[𝕜] F) {U V : Submodule 𝕜 F} (h : U ⟂ V) :
    U.comap f ⟂ V.comap f

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
h : ∀ u ∈ U, ∀ v ∈ V, inner u v = 0
u : E
hu : f u ∈ U
v : E
hv : f v ∈ V
⊢ inner (f u) (f v) = 0

Tactic:
exact h _ hu _ hv

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
h : U ⟂ V
⊢ Submodule.comap f U ⟂ Submodule.comap f V

Tactic:
rw [isOrtho_iff_inner_eq] at *

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
h : ∀ u ∈ U, ∀ v ∈ V, inner u v = 0
⊢ ∀ u ∈ Submodule.comap f U, ∀ v ∈ Submodule.comap f V, inner u v = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
h : ∀ u ∈ U, ∀ v ∈ V, inner u v = 0
⊢ ∀ (u : E), f u ∈ U → ∀ (v : E), f v ∈ V → inner (f u) (f v) = 0

Tactic:
intro u hu v hv

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
h : ∀ u ∈ U, ∀ v ∈ V, inner u v = 0
u : E
hu : f u ∈ U
v : E
hv : f v ∈ V
⊢ inner (f u) (f v) = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
h : ∀ u ∈ U, ∀ v ∈ V, inner u v = 0
⊢ ∀ u ∈ Submodule.comap f U, ∀ v ∈ Submodule.comap f V, inner u v = 0

Tactic:
simp_rw [mem_comap, ← f.inner_map_map]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
h : ∀ u ∈ U, ∀ v ∈ V, inner u v = 0
⊢ ∀ (u : E), f u ∈ U → ∀ (v : E), f v ∈ V → inner (f u) (f v) = 0
-- Mathlib/Order/Filter/Ring.lean
theorem EventuallyLE.mul_le_mul' [Mul β] [Preorder β] [MulLeftMono β]
    [MulRightMono β] {l : Filter α} {f₁ f₂ g₁ g₂ : α → β}
    (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) : f₁ * g₁ ≤ᶠ[l] f₂ * g₂

Proof state:
α : Type u
β : Type v
inst✝³ : Mul β
inst✝² : Preorder β
inst✝¹ : MulLeftMono β
inst✝ : MulRightMono β
l : Filter α
f₁ f₂ g₁ g₂ : α → β
hf : f₁ ≤ᶠ[l] f₂
hg : g₁ ≤ᶠ[l] g₂
⊢ f₁ * g₁ ≤ᶠ[l] f₂ * g₂

Tactic:
filter_upwards [hf, hg] with x hfx hgx using _root_.mul_le_mul' hfx hgx

Result:
no goals
-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem inverse_graph : (inverse f).graph = f.graph.map (LinearEquiv.prodComm R E F)

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
hf : LinearMap.ker f.toFun = ⊥
⊢ f.inverse.graph = Submodule.map (LinearEquiv.prodComm R E F) f.graph

Tactic:
rw [inverse, Submodule.toLinearPMap_graph_eq _ (mem_inverse_graph_snd_eq_zero hf)]

Result:
no goals
-- Mathlib/GroupTheory/Congruence/Defs.lean
theorem conGen_le {r : M → M → Prop} {c : Con M} (h : ∀ x y, r x y → c x y) :
    conGen r ≤ c

Proof state:
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
c : Con M
h : ∀ (x y : M), r x y → c x y
⊢ conGen r ≤ c

Tactic:
rw [conGen_eq]

Result:
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
c : Con M
h : ∀ (x y : M), r x y → c x y
⊢ sInf {s | ∀ (x y : M), r x y → s x y} ≤ c

Proof state:
M : Type u_1
inst✝ : Mul M
r : M → M → Prop
c : Con M
h : ∀ (x y : M), r x y → c x y
⊢ sInf {s | ∀ (x y : M), r x y → s x y} ≤ c

Tactic:
exact sInf_le h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem wfImp_containsThenInsert [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
    (h : Raw.WFImp m.1) {a : α} {b : β a} : Raw.WFImp (m.containsThenInsert a b).2.1

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ Raw.WFImp (m.containsThenInsert a b).snd.val

Tactic:
rw [containsThenInsert_eq_insertₘ]

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ Raw.WFImp (m.insertₘ a b).val

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ Raw.WFImp (m.insertₘ a b).val

Tactic:
exact wfImp_insertₘ h

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Exhaustion.lean
@[simp]
lemma measure_compl_sigmaFiniteSetWRT (hμν : μ ≪ ν) [SigmaFinite μ] [SFinite ν] :
    ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ⊤
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
i : ℕ
h_ne_zero : ¬μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = 0
⊢ False

Tactic:
have h_zero_top := measure_eq_top_of_subset_compl_sigmaFiniteSetWRT
  (Set.inter_subset_left : (μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i ⊆ _) ?_

Result:
case refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ⊤
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
i : ℕ
h_ne_zero : ¬μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = 0
h_zero_top : μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = ⊤
⊢ False

case refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ⊤
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
i : ℕ
h_ne_zero : ¬μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = 0
⊢ ν ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) ≠ 0
-- Mathlib/AlgebraicGeometry/Restrict.lean
theorem pullbackRestrictIsoRestrict_hom_ι {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) :
    (pullbackRestrictIsoRestrict f U).hom ≫ (f ⁻¹ᵁ U).ι = pullback.fst f _

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (pullbackRestrictIsoRestrict f U).hom ≫ (f ⁻¹ᵁ U).ι = pullback.fst f U.ι

Tactic:
delta pullbackRestrictIsoRestrict

Result:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (IsOpenImmersion.isoOfRangeEq (pullback.fst f U.ι) (f ⁻¹ᵁ U).ι ⋯).hom ≫ (f ⁻¹ᵁ U).ι = pullback.fst f U.ι

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (IsOpenImmersion.isoOfRangeEq (pullback.fst f U.ι) (f ⁻¹ᵁ U).ι ⋯).hom ≫ (f ⁻¹ᵁ U).ι = pullback.fst f U.ι

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem angle_smul_right_of_pos (x y : V) {r : ℝ} (hr : 0 < r) : angle x (r • y) = angle x y

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
r : ℝ
hr : 0 < r
⊢ arccos (inner x (r • y) / (‖x‖ * ‖r • y‖)) = arccos (inner x y / (‖x‖ * ‖y‖))

Tactic:
rw [inner_smul_right, norm_smul, Real.norm_eq_abs, abs_of_nonneg (le_of_lt hr), ← mul_assoc,
  mul_comm _ r, mul_assoc, mul_div_mul_left _ _ (ne_of_gt hr)]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
r : ℝ
hr : 0 < r
⊢ angle x (r • y) = angle x y

Tactic:
unfold angle

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
r : ℝ
hr : 0 < r
⊢ arccos (inner x (r • y) / (‖x‖ * ‖r • y‖)) = arccos (inner x y / (‖x‖ * ‖y‖))
-- Mathlib/FieldTheory/Tower.lean
theorem right [hf : Module.Finite F A] : Module.Finite K A :=
  let ⟨⟨b, hb⟩⟩ := hf
  ⟨⟨b, Submodule.restrictScalars_injective F _ _ <| by
    rw [Submodule.restrictScalars_top, eq_top_iff, ← hb, Submodule.span_le]
    exact Submodule.subset_span⟩⟩

Proof state:
F : Type u
K : Type v
A : Type w
inst✝⁶ : Semiring F
inst✝⁵ : Semiring K
inst✝⁴ : Module F K
inst✝³ : AddCommMonoid A
inst✝² : Module K A
inst✝¹ : Module F A
inst✝ : IsScalarTower F K A
hf : Module.Finite F A
b : Finset A
hb : span F ↑b = ⊤
⊢ restrictScalars F (span K ↑b) = restrictScalars F ⊤

Tactic:
rw [Submodule.restrictScalars_top, eq_top_iff, ← hb, Submodule.span_le]

Result:
F : Type u
K : Type v
A : Type w
inst✝⁶ : Semiring F
inst✝⁵ : Semiring K
inst✝⁴ : Module F K
inst✝³ : AddCommMonoid A
inst✝² : Module K A
inst✝¹ : Module F A
inst✝ : IsScalarTower F K A
hf : Module.Finite F A
b : Finset A
hb : span F ↑b = ⊤
⊢ ↑b ⊆ ↑(restrictScalars F (span K ↑b))

Proof state:
F : Type u
K : Type v
A : Type w
inst✝⁶ : Semiring F
inst✝⁵ : Semiring K
inst✝⁴ : Module F K
inst✝³ : AddCommMonoid A
inst✝² : Module K A
inst✝¹ : Module F A
inst✝ : IsScalarTower F K A
hf : Module.Finite F A
b : Finset A
hb : span F ↑b = ⊤
⊢ ↑b ⊆ ↑(restrictScalars F (span K ↑b))

Tactic:
exact Submodule.subset_span

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Map.lean
theorem map_smul {R : Type*} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞]
    (c : R) (μ : Measure α) (f : α → β) : (c • μ).map f = c • μ.map f

Proof state:
case pos.e_a
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_4
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ : Measure α
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
hf : AEMeasurable f μ
hfc : AEMeasurable f (c • μ)
⊢ AEMeasurable.mk f hfc =ᶠ[ae μ] AEMeasurable.mk f hf

Tactic:
exact EventuallyEq.trans ((ae_smul_measure_iff hc).1 hfc.ae_eq_mk.symm) hf.ae_eq_mk

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_4
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ : Measure α
f : α → β
c : ℝ≥0∞
⊢ map f (c • μ) = c • map f μ

Tactic:
rcases eq_or_ne c 0 with (rfl | hc)

Result:
case inl
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_4
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ : Measure α
f : α → β
⊢ map f (0 • μ) = 0 • map f μ

case inr
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_4
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ : Measure α
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
⊢ map f (c • μ) = c • map f μ
-- Mathlib/Data/Vector/Basic.lean
theorem eraseIdx_insertIdx' {v : Vector α (n + 1)} :
    ∀ {i : Fin (n + 1)} {j : Fin (n + 2)},
      eraseIdx (j.succAbove i) (insertIdx a j v) = insertIdx a (i.predAbove j) (eraseIdx i v)
  | ⟨i, hi⟩, ⟨j, hj⟩ => by
    dsimp [insertIdx, eraseIdx, Fin.succAbove, Fin.predAbove]
    rw [Subtype.mk_eq_mk]
    simp only [Fin.lt_iff_val_lt_val]
    split_ifs with hij
    · rcases Nat.exists_eq_succ_of_ne_zero
        (Nat.pos_iff_ne_zero.1 (lt_of_le_of_lt (Nat.zero_le _) hij)) with ⟨j, rfl⟩
      rw [← List.insertIdx_eraseIdx_of_ge]
      · simp; rfl
      · simpa
      · simpa [Nat.lt_succ_iff] using hij
    · dsimp
      rw [← List.insertIdx_eraseIdx_of_le i j _ _ _]
      · rfl
      · simpa
      · simpa [not_lt] using hij

Proof state:
case pos.intro
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ List.insertIdx j a ((↑v).eraseIdx ↑⟨i, ⋯⟩) =
    List.insertIdx (↑(⟨j.succ, hj⟩.pred ⋯)) a
      ↑(match v with
        | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)

Tactic:
simp

Result:
case pos.intro
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j.succ < n + 2
hij : i < j.succ
⊢ List.insertIdx j a ((↑v).eraseIdx i) =
    List.insertIdx j a
      ↑(match v with
        | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)

Proof state:
case neg
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ (List.insertIdx j a ↑v).eraseIdx ↑⟨i + 1, ⋯⟩ =
    List.insertIdx (↑(⟨j, hj⟩.castPred ⋯)) a
      ↑(match v with
        | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)

Tactic:
dsimp

Result:
case neg
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ (List.insertIdx j a ↑v).eraseIdx (i + 1) =
    List.insertIdx j a
      ↑(match v with
        | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lex/Lemmas.lean
theorem _root_.List.lex_toArray [BEq α] (lt : α → α → Bool) (l₁ l₂ : List α) :
    l₁.toArray.lex l₂.toArray lt = l₁.lex l₂ lt

Proof state:
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
l₁ l₂ : List α
⊢ l₁.toArray.lex l₂.toArray lt = l₁.lex l₂ lt

Tactic:
induction l₁ generalizing l₂ with
| nil => cases l₂ <;> simp [lex, Id.run]
| cons x l₁ ih =>
  cases l₂ with
  | nil => simp [lex, Id.run]
  | cons y l₂ =>
    rw [List.toArray_cons, List.toArray_cons y, cons_lex_cons, List.lex, ih]

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
x : α
l₁ : List α
ih : ∀ (l₂ : List α), l₁.toArray.lex l₂.toArray lt = l₁.lex l₂ lt
l₂ : List α
⊢ (x :: l₁).toArray.lex l₂.toArray lt = (x :: l₁).lex l₂ lt

Tactic:
cases l₂ with
| nil => simp [lex, Id.run]
| cons y l₂ =>
  rw [List.toArray_cons, List.toArray_cons y, cons_lex_cons, List.lex, ih]

Result:
no goals

Proof state:
case cons.nil
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
x : α
l₁ : List α
ih : ∀ (l₂ : List α), l₁.toArray.lex l₂.toArray lt = l₁.lex l₂ lt
⊢ (x :: l₁).toArray.lex #[] lt = (x :: l₁).lex [] lt

Tactic:
simp [lex, Id.run]

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
l₂ : List α
⊢ #[].lex l₂.toArray lt = [].lex l₂ lt

Tactic:
cases l₂ <;> simp [lex, Id.run]

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
x : α
l₁ : List α
ih : ∀ (l₂ : List α), l₁.toArray.lex l₂.toArray lt = l₁.lex l₂ lt
y : α
l₂ : List α
⊢ (x :: l₁).toArray.lex (y :: l₂).toArray lt = (x :: l₁).lex (y :: l₂) lt

Tactic:
rw [List.toArray_cons, List.toArray_cons y, cons_lex_cons, List.lex, ih]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean
theorem opNorm_subsingleton [Subsingleton E] : ‖f‖ = 0

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
inst✝ : Subsingleton E
⊢ ‖f‖ ≤ 0

Tactic:
apply opNorm_le_bound _ rfl.ge

Result:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
inst✝ : Subsingleton E
⊢ ∀ (x : E), ‖f x‖ ≤ 0 * ‖x‖

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
inst✝ : Subsingleton E
x : E
⊢ ‖f x‖ ≤ 0 * ‖x‖

Tactic:
simp [Subsingleton.elim x 0]

Result:
no goals

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
inst✝ : Subsingleton E
⊢ ∀ (x : E), ‖f x‖ ≤ 0 * ‖x‖

Tactic:
intro x

Result:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
inst✝ : Subsingleton E
x : E
⊢ ‖f x‖ ≤ 0 * ‖x‖

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
inst✝ : Subsingleton E
⊢ ‖f‖ = 0

Tactic:
refine le_antisymm ?_ (norm_nonneg _)

Result:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁷ : SeminormedAddCommGroup E
inst✝⁶ : SeminormedAddCommGroup F
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NontriviallyNormedField 𝕜₂
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
inst✝ : Subsingleton E
⊢ ‖f‖ ≤ 0
-- Mathlib/CategoryTheory/Limits/Constructions/Equalizers.lean
theorem pushoutInl_eq_pushout_inr (F : WalkingParallelPair ⥤ C) :
    pushoutInl F = pushout.inr _ _

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
⊢ pushoutInl F =
    pushout.inr (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
      (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right))

Tactic:
convert (whisker_eq Limits.coprod.inl pushout.condition :
  (_ : F.obj _ ⟶ constructCoequalizer _) = _) <;> simp

Result:
no goals
-- Mathlib/Data/Matrix/ConjTranspose.lean
theorem star_dotProduct_star : star v ⬝ᵥ star w = star (w ⬝ᵥ v)

Proof state:
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : NonUnitalSemiring α
inst✝ : StarRing α
v w : m → α
⊢ star v ⬝ᵥ star w = star (w ⬝ᵥ v)

Tactic:
simp [dotProduct]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Fin.lean
theorem Equiv.Perm.decomposeFin_symm_apply_succ {n : ℕ} (e : Perm (Fin n)) (p : Fin (n + 1))
    (x : Fin n) : Equiv.Perm.decomposeFin.symm (p, e) x.succ = swap 0 p (e x).succ

Proof state:
case refine_2
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x i : Fin n
⊢ (decomposeFin.symm (i.succ, e)) x.succ = (swap 0 i.succ) (e x).succ

Tactic:
by_cases h : i = e x

Result:
case pos
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x i : Fin n
h : i = e x
⊢ (decomposeFin.symm (i.succ, e)) x.succ = (swap 0 i.succ) (e x).succ

case neg
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x i : Fin n
h : ¬i = e x
⊢ (decomposeFin.symm (i.succ, e)) x.succ = (swap 0 i.succ) (e x).succ

Proof state:
case neg
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x i : Fin n
h : ¬i = e x
⊢ (decomposeFin.symm (i.succ, e)) x.succ = (swap 0 i.succ) (e x).succ

Tactic:
simp [h, Fin.succ_ne_zero, Equiv.Perm.decomposeFin, EquivFunctor.map,
  swap_apply_def, Ne.symm h]

Result:
no goals

Proof state:
case pos
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x i : Fin n
h : i = e x
⊢ (decomposeFin.symm (i.succ, e)) x.succ = (swap 0 i.succ) (e x).succ

Tactic:
simp [h, Equiv.Perm.decomposeFin, EquivFunctor.map]

Result:
no goals

Proof state:
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x : Fin n
⊢ (decomposeFin.symm (p, e)) x.succ = (swap 0 p) (e x).succ

Tactic:
refine Fin.cases ?_ ?_ p

Result:
case refine_1
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x : Fin n
⊢ (decomposeFin.symm (0, e)) x.succ = (swap 0 0) (e x).succ

case refine_2
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x : Fin n
⊢ ∀ (i : Fin n), (decomposeFin.symm (i.succ, e)) x.succ = (swap 0 i.succ) (e x).succ

Proof state:
case refine_2
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x : Fin n
⊢ ∀ (i : Fin n), (decomposeFin.symm (i.succ, e)) x.succ = (swap 0 i.succ) (e x).succ

Tactic:
intro i

Result:
case refine_2
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x i : Fin n
⊢ (decomposeFin.symm (i.succ, e)) x.succ = (swap 0 i.succ) (e x).succ

Proof state:
case refine_1
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x : Fin n
⊢ (decomposeFin.symm (0, e)) x.succ = (swap 0 0) (e x).succ

Tactic:
simp [Equiv.Perm.decomposeFin, EquivFunctor.map]

Result:
no goals
-- Mathlib/Data/Nat/Pairing.lean
theorem unpair_lt {n : ℕ} (n1 : 1 ≤ n) : (unpair n).1 < n

Proof state:
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
⊢ (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1 < n

Tactic:
by_cases h : n - s * s < s <;> simp [s, h, ↓reduceIte]

Result:
case pos
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : n - s * s < s
⊢ n - n.sqrt * n.sqrt < n

case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : ¬n - s * s < s
⊢ n.sqrt < n

Proof state:
case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : s ≤ n - s * s
s0 : 0 < s
⊢ n.sqrt < n

Tactic:
exact lt_of_le_of_lt h (Nat.sub_lt n1 (Nat.mul_pos s0 s0))

Result:
no goals

Proof state:
case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : s ≤ n - s * s
⊢ n.sqrt < n

Tactic:
have s0 : 0 < s := sqrt_pos.2 n1

Result:
case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : s ≤ n - s * s
s0 : 0 < s
⊢ n.sqrt < n

Proof state:
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
⊢ (unpair n).1 < n

Tactic:
simp only [unpair, Nat.sub_le_iff_le_add]

Result:
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
⊢ (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1 < n

Proof state:
case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : ¬n - s * s < s
⊢ n.sqrt < n

Tactic:
simp only [not_lt] at h

Result:
case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : s ≤ n - s * s
⊢ n.sqrt < n

Proof state:
n : ℕ
n1 : 1 ≤ n
⊢ (unpair n).1 < n

Tactic:
let s := sqrt n

Result:
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
⊢ (unpair n).1 < n

Proof state:
case pos
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : n - s * s < s
⊢ n - n.sqrt * n.sqrt < n

Tactic:
exact lt_of_lt_of_le h (sqrt_le_self _)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem card_roots_sub_C {p : R[X]} {a : R} (hp0 : 0 < degree p) :
    (Multiset.card (p - C a).roots : WithBot ℕ) ≤ degree p :=
  calc
    (Multiset.card (p - C a).roots : WithBot ℕ) ≤ degree (p - C a) :=
      card_roots <| mt sub_eq_zero.1 fun h => not_le_of_gt hp0 <| h.symm ▸ degree_C_le
    _ = degree p

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a : R
hp0 : 0 < p.degree
⊢ (p - C a).degree = p.degree

Tactic:
rw [sub_eq_add_neg, ← C_neg]

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a : R
hp0 : 0 < p.degree
⊢ (p + C (-a)).degree = p.degree

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a : R
hp0 : 0 < p.degree
⊢ (p + C (-a)).degree = p.degree

Tactic:
exact degree_add_C hp0

Result:
no goals
-- Mathlib/Tactic/NormNum/RealSqrt.lean
lemma isNat_realSqrt_neg {x : ℝ} {nx : ℕ} (h : IsInt x (Int.negOfNat nx)) :
    IsNat √x (nat_lit 0) := ⟨by simp [Real.sqrt_eq_zero', h.out]⟩

Proof state:
x : ℝ
nx : ℕ
h : IsInt x (Int.negOfNat nx)
⊢ √x = ↑0

Tactic:
simp [Real.sqrt_eq_zero', h.out]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldl_map (f : β₁ → β₂) (g : α → β₂ → α) (l : Vector β₁ n) (init : α) :
    (l.map f).foldl g init = l.foldl (fun x y => g x (f y)) init

Proof state:
β₁ : Type u_1
β₂ : Type u_2
α : Type u_3
n : Nat
f : β₁ → β₂
g : α → β₂ → α
l : Vector β₁ n
init : α
⊢ foldl g init (map f l) = foldl (fun x y => g x (f y)) init l

Tactic:
cases l

Result:
case mk
β₁ : Type u_1
β₂ : Type u_2
α : Type u_3
n : Nat
f : β₁ → β₂
g : α → β₂ → α
init : α
toArray✝ : Array β₁
size_toArray✝ : toArray✝.size = n
⊢ foldl g init (map f { toArray := toArray✝, size_toArray := size_toArray✝ }) =
    foldl (fun x y => g x (f y)) init { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk
β₁ : Type u_1
β₂ : Type u_2
α : Type u_3
n : Nat
f : β₁ → β₂
g : α → β₂ → α
init : α
toArray✝ : Array β₁
size_toArray✝ : toArray✝.size = n
⊢ foldl g init (map f { toArray := toArray✝, size_toArray := size_toArray✝ }) =
    foldl (fun x y => g x (f y)) init { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp [Array.foldl_map']

Result:
no goals