harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/MorphismProperty/Representable.lean
/-- Two morphisms `a b : c ⟶ hf.pullback g` are equal if
* Their compositions (in `C`) with `hf.snd g : hf.pullback  ⟶ X` are equal.
* The compositions of `F.map a` and `F.map b` with `hf.fst g` are equal. -/
@[ext 100]
lemma hom_ext [Faithful F] {c : C} {a b : c ⟶ hf.pullback g}
    (h₁ : F.map a ≫ hf.fst g = F.map b ≫ hf.fst g)
    (h₂ : a ≫ hf.snd g = b ≫ hf.snd g) : a = b :=
  F.map_injective <|
    PullbackCone.IsLimit.hom_ext (hf.isPullback g).isLimit h₁ (by simpa using F.congr_map h₂)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : D
f : X ⟶ Y
hf : F.relativelyRepresentable f
a✝ : C
g : F.obj a✝ ⟶ Y
inst✝ : F.Faithful
c : C
a b : c ⟶ hf.pullback g
h₁ : F.map a ≫ hf.fst g = F.map b ≫ hf.fst g
h₂ : a ≫ hf.snd g = b ≫ hf.snd g
⊢ F.map a ≫ ⋯.cone.snd = F.map b ≫ ⋯.cone.snd

Tactic:
simpa using F.congr_map h₂

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
lemma Topology.IsInducing.isCompact_preimage_iff {f : X → Y} (hf : IsInducing f) {K : Set Y}
    (Kf : K ⊆ range f) : IsCompact (f ⁻¹' K) ↔ IsCompact K

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
K : Set Y
Kf : K ⊆ range f
⊢ IsCompact (f ⁻¹' K) ↔ IsCompact K

Tactic:
rw [hf.isCompact_iff, image_preimage_eq_of_subset Kf]

Result:
no goals
-- Mathlib/Analysis/Complex/Hadamard.lean
/-- The transformation on ℂ that is used for `scale` maps the strip ``re ⁻¹' (l, u)``
  to the strip ``re ⁻¹' (0, 1)``. -/
lemma scale_id_mem_verticalStrip_of_mem_verticalStrip {l u : ℝ} (hul : l < u) {z : ℂ}
    (hz : z ∈ verticalStrip 0 1) : l + z * (u - l) ∈ verticalStrip l u

Proof state:
case intro
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 < z.re
hz₂ : z.re < 1
⊢ l + z.re * (u - l) < u

Tactic:
rw [add_comm, ← sub_lt_sub_iff_right l, add_sub_assoc, sub_self, add_zero]

Result:
case intro
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 < z.re
hz₂ : z.re < 1
⊢ z.re * (u - l) < u - l

Proof state:
l u : ℝ
hul : l < u
z : ℂ
hz : 0 < z.re ∧ z.re < 1
⊢ ↑l + z * (↑u - ↑l) ∈ verticalStrip l u

Tactic:
simp only [verticalStrip, mem_preimage, add_re, ofReal_re, mul_re, sub_re, sub_im, ofReal_im,
  sub_self, mul_zero, sub_zero, mem_Ioo, lt_add_iff_pos_right]

Result:
l u : ℝ
hul : l < u
z : ℂ
hz : 0 < z.re ∧ z.re < 1
⊢ 0 < z.re * (u - l) ∧ l + z.re * (u - l) < u

Proof state:
case intro
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 < z.re
hz₂ : z.re < 1
⊢ z.re * (u - l) < u - l

Tactic:
nth_rewrite 2 [← one_mul (u - l)]

Result:
case intro
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 < z.re
hz₂ : z.re < 1
⊢ z.re * (u - l) < 1 * (u - l)

Proof state:
case intro
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 < z.re
hz₂ : z.re < 1
⊢ z.re * (u - l) < 1 * (u - l)

Tactic:
gcongr

Result:
case intro.a0
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 < z.re
hz₂ : z.re < 1
⊢ 0 < u - l

Proof state:
l u : ℝ
hul : l < u
z : ℂ
hz : 0 < z.re ∧ z.re < 1
⊢ 0 < z.re * (u - l) ∧ l + z.re * (u - l) < u

Tactic:
obtain ⟨hz₁, hz₂⟩ := hz

Result:
case intro
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 < z.re
hz₂ : z.re < 1
⊢ 0 < z.re * (u - l) ∧ l + z.re * (u - l) < u

Proof state:
case intro.a0
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 < z.re
hz₂ : z.re < 1
⊢ 0 < u - l

Tactic:
simp only [sub_pos]

Result:
case intro.a0
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 < z.re
hz₂ : z.re < 1
⊢ l < u

Proof state:
case intro
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 < z.re
hz₂ : z.re < 1
⊢ 0 < z.re * (u - l) ∧ l + z.re * (u - l) < u

Tactic:
simp only [hz₁, mul_pos_iff_of_pos_left, sub_pos, hul, true_and]

Result:
case intro
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 < z.re
hz₂ : z.re < 1
⊢ l + z.re * (u - l) < u

Proof state:
l u : ℝ
hul : l < u
z : ℂ
hz : z ∈ verticalStrip 0 1
⊢ ↑l + z * (↑u - ↑l) ∈ verticalStrip l u

Tactic:
simp only [verticalStrip, mem_preimage, mem_Ioo] at hz

Result:
l u : ℝ
hul : l < u
z : ℂ
hz : 0 < z.re ∧ z.re < 1
⊢ ↑l + z * (↑u - ↑l) ∈ verticalStrip l u

Proof state:
case intro.a0
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 < z.re
hz₂ : z.re < 1
⊢ l < u

Tactic:
exact hul

Result:
no goals
-- Mathlib/Order/ModularLattice.lean
theorem covBy_sup_of_inf_covBy_of_inf_covBy_right : a ⊓ b ⋖ a → a ⊓ b ⋖ b → b ⋖ a ⊔ b

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsWeakUpperModularLattice α
a b : α
⊢ a ⊓ b ⋖ a → a ⊓ b ⋖ b → b ⋖ a ⊔ b

Tactic:
rw [inf_comm, sup_comm]

Result:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsWeakUpperModularLattice α
a b : α
⊢ b ⊓ a ⋖ a → b ⊓ a ⋖ b → b ⋖ b ⊔ a

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsWeakUpperModularLattice α
a b : α
⊢ b ⊓ a ⋖ a → b ⊓ a ⋖ b → b ⋖ b ⊔ a

Tactic:
exact fun ha hb => covBy_sup_of_inf_covBy_of_inf_covBy_left hb ha

Result:
no goals
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem Basis.ofZLatticeBasis_apply (i : ι) :
    b.ofZLatticeBasis K L i = b i

Proof state:
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_3
hs : IsZLattice K L
b : Basis ι ℤ ↥L
i : ι
⊢ (ofZLatticeBasis K L b) i = ↑(b i)

Tactic:
simp [Basis.ofZLatticeBasis]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem forIn'_yield_eq_foldlM [Monad m] [LawfulMonad m]
    (l : List α) (f : (a : α) → a ∈ l → β → m γ) (g : (a : α) → a ∈ l → β → γ → β) (init : β) :
    forIn' l init (fun a m b => (fun c => .yield (g a m b c)) <$> f a m b) =
      l.attach.foldlM (fun b ⟨a, m⟩ => g a m b <$> f a m b) init

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (a : α) → a ∈ l → β → m γ
g : (a : α) → a ∈ l → β → γ → β
init : β
⊢ ForInStep.value <$>
      List.foldlM
        (fun b x =>
          match b with
          | ForInStep.yield b => (fun c => ForInStep.yield (g x.val ⋯ b c)) <$> f x.val ⋯ b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l.attach =
    List.foldlM (fun b x => g x.val ⋯ b <$> f x.val ⋯ b) init l.attach

Tactic:
generalize l.attach = l'

Result:
m : Type u_1 → Type u_2
α : Type u_3
β γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (a : α) → a ∈ l → β → m γ
g : (a : α) → a ∈ l → β → γ → β
init : β
l' : List { x // x ∈ l }
⊢ ForInStep.value <$>
      List.foldlM
        (fun b x =>
          match b with
          | ForInStep.yield b => (fun c => ForInStep.yield (g x.val ⋯ b c)) <$> f x.val ⋯ b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l' =
    List.foldlM (fun b x => g x.val ⋯ b <$> f x.val ⋯ b) init l'

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (a : α) → a ∈ l → β → m γ
g : (a : α) → a ∈ l → β → γ → β
init : β
⊢ (forIn' l init fun a m_1 b => (fun c => ForInStep.yield (g a m_1 b c)) <$> f a m_1 b) =
    List.foldlM
      (fun b x =>
        match x with
        | ⟨a, m_1⟩ => g a m_1 b <$> f a m_1 b)
      init l.attach

Tactic:
simp only [forIn'_eq_foldlM]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (a : α) → a ∈ l → β → m γ
g : (a : α) → a ∈ l → β → γ → β
init : β
⊢ ForInStep.value <$>
      List.foldlM
        (fun b x =>
          match b with
          | ForInStep.yield b => (fun c => ForInStep.yield (g x.val ⋯ b c)) <$> f x.val ⋯ b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l.attach =
    List.foldlM (fun b x => g x.val ⋯ b <$> f x.val ⋯ b) init l.attach

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : (a : α) → a ∈ l → β → m γ
g : (a : α) → a ∈ l → β → γ → β
init : β
l' : List { x // x ∈ l }
⊢ ForInStep.value <$>
      List.foldlM
        (fun b x =>
          match b with
          | ForInStep.yield b => (fun c => ForInStep.yield (g x.val ⋯ b c)) <$> f x.val ⋯ b
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l' =
    List.foldlM (fun b x => g x.val ⋯ b <$> f x.val ⋯ b) init l'

Tactic:
induction l' generalizing init <;> simp_all

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem map_vecMul [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (M : Matrix n m R)
    (v : n → R) (i : m) : f ((v ᵥ* M) i) =  ((f ∘ v) ᵥ* M.map f) i

Proof state:
m : Type u_2
n : Type u_3
R : Type u_7
S : Type u_8
inst✝² : Fintype n
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
M : Matrix n m R
v : n → R
i : m
⊢ f ((v ᵥ* M) i) = (⇑f ∘ v ᵥ* M.map ⇑f) i

Tactic:
simp only [Matrix.vecMul, Matrix.map_apply, RingHom.map_dotProduct, Function.comp_def]

Result:
no goals
-- Mathlib/Analysis/Complex/Hadamard.lean
/-- A technical lemma relating the bounds given by the three lines lemma on a general strip
to the bounds for its scaled version on the strip ``re ⁻¹' [0, 1]`. -/
lemma interpStrip_scale (f : ℂ → E) {l u : ℝ} (hul: l < u) (z : ℂ)  : interpStrip (scale f l u)
    ((z - ↑l) / (↑u - ↑l)) = interpStrip' f l u z

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
z : ℂ
⊢ (if sSupNormIm (scale f l u) 0 = 0 ∨ sSupNormIm (scale f l u) 1 = 0 then 0
    else
      ↑(sSupNormIm (scale f l u) 0) ^ (1 - (z - ↑l) / (↑u - ↑l)) *
        ↑(sSupNormIm (scale f l u) 1) ^ ((z - ↑l) / (↑u - ↑l))) =
    if sSupNormIm f l = 0 ∨ sSupNormIm f u = 0 then 0
    else ↑(sSupNormIm f l) ^ (1 - (z - ↑l) / (↑u - ↑l)) * ↑(sSupNormIm f u) ^ ((z - ↑l) / (↑u - ↑l))

Tactic:
simp_rw [sSupNormIm_scale_left f hul, sSupNormIm_scale_right f hul]

Result:
no goals

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
z : ℂ
⊢ interpStrip (scale f l u) ((z - ↑l) / (↑u - ↑l)) = interpStrip' f l u z

Tactic:
simp only [interpStrip, interpStrip']

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
z : ℂ
⊢ (if sSupNormIm (scale f l u) 0 = 0 ∨ sSupNormIm (scale f l u) 1 = 0 then 0
    else
      ↑(sSupNormIm (scale f l u) 0) ^ (1 - (z - ↑l) / (↑u - ↑l)) *
        ↑(sSupNormIm (scale f l u) 1) ^ ((z - ↑l) / (↑u - ↑l))) =
    if sSupNormIm f l = 0 ∨ sSupNormIm f u = 0 then 0
    else ↑(sSupNormIm f l) ^ (1 - (z - ↑l) / (↑u - ↑l)) * ↑(sSupNormIm f u) ^ ((z - ↑l) / (↑u - ↑l))
-- Mathlib/Data/Complex/Exponential.lean
theorem exp_1_approx_succ_eq {n} {a₁ b₁ : ℝ} {m : ℕ} (en : n + 1 = m) {rm : ℝ} (er : ↑m = rm)
    (h : |exp 1 - expNear m 1 ((a₁ - 1) * rm)| ≤ |1| ^ m / m.factorial * (b₁ * rm)) :
    |exp 1 - expNear n 1 a₁| ≤ |1| ^ n / n.factorial * b₁

Proof state:
n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
h : |rexp 1 - expNear m 1 ((a₁ - 1) * ↑m)| ≤ |1| ^ m / ↑m.factorial * (b₁ * ↑m)
⊢ ¬m = 0

Tactic:
omega

Result:
no goals

Proof state:
n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
h : |rexp 1 - expNear m 1 ((a₁ - 1) * ↑m)| ≤ |1| ^ m / ↑m.factorial * (b₁ * ↑m)
⊢ ↑m ≠ 0

Tactic:
norm_cast

Result:
n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
h : |rexp 1 - expNear m 1 ((a₁ - 1) * ↑m)| ≤ |1| ^ m / ↑m.factorial * (b₁ * ↑m)
⊢ ¬m = 0

Proof state:
n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
h : |rexp 1 - expNear m 1 ((a₁ - 1) * ↑m)| ≤ |1| ^ m / ↑m.factorial * (b₁ * ↑m)
⊢ |1 + 1 / ↑m * ((a₁ - 1) * ↑m) - a₁| ≤ b₁ - |1| / ↑m * (b₁ * ↑m)

Tactic:
field_simp [show (m : ℝ) ≠ 0 by norm_cast; omega]

Result:
no goals

Proof state:
n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
h : |rexp 1 - expNear m 1 ((a₁ - 1) * ↑m)| ≤ |1| ^ m / ↑m.factorial * (b₁ * ↑m)
⊢ |rexp 1 - expNear n 1 a₁| ≤ |1| ^ n / ↑n.factorial * b₁

Tactic:
refine exp_approx_succ _ en _ _ ?_ h

Result:
n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
h : |rexp 1 - expNear m 1 ((a₁ - 1) * ↑m)| ≤ |1| ^ m / ↑m.factorial * (b₁ * ↑m)
⊢ |1 + 1 / ↑m * ((a₁ - 1) * ↑m) - a₁| ≤ b₁ - |1| / ↑m * (b₁ * ↑m)

Proof state:
n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
rm : ℝ
er : ↑m = rm
h : |rexp 1 - expNear m 1 ((a₁ - 1) * rm)| ≤ |1| ^ m / ↑m.factorial * (b₁ * rm)
⊢ |rexp 1 - expNear n 1 a₁| ≤ |1| ^ n / ↑n.factorial * b₁

Tactic:
subst er

Result:
n : ℕ
a₁ b₁ : ℝ
m : ℕ
en : n + 1 = m
h : |rexp 1 - expNear m 1 ((a₁ - 1) * ↑m)| ≤ |1| ^ m / ↑m.factorial * (b₁ * ↑m)
⊢ |rexp 1 - expNear n 1 a₁| ≤ |1| ^ n / ↑n.factorial * b₁
-- Mathlib/Order/SuccPred/Basic.lean
theorem pred_le_pred_of_not_isMin_of_le (ha : ¬IsMin a) (hb : ¬IsMin b) :
    a ≤ b → pred a ≤ pred b

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
hb : ¬IsMin b
⊢ a ≤ b → pred a < b

Tactic:
apply pred_lt_of_not_isMin_of_le ha

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
hb : ¬IsMin b
⊢ a ≤ b → pred a ≤ pred b

Tactic:
rw [le_pred_iff_of_not_isMin hb]

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
hb : ¬IsMin b
⊢ a ≤ b → pred a < b
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem collinear_iff_finrank_le_one {s : Set P} [FiniteDimensional k (vectorSpan k s)] :
    Collinear k s ↔ finrank k (vectorSpan k s) ≤ 1

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k ↥(vectorSpan k s)
⊢ Collinear k s ↔ finrank k ↥(vectorSpan k s) ≤ 1

Tactic:
have h := collinear_iff_rank_le_one k s

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k ↥(vectorSpan k s)
h : Collinear k s ↔ Module.rank k ↥(vectorSpan k s) ≤ 1
⊢ Collinear k s ↔ finrank k ↥(vectorSpan k s) ≤ 1

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k ↥(vectorSpan k s)
h : Collinear k s ↔ Module.rank k ↥(vectorSpan k s) ≤ 1
⊢ Collinear k s ↔ finrank k ↥(vectorSpan k s) ≤ 1

Tactic:
rw [← finrank_eq_rank] at h

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k ↥(vectorSpan k s)
h : Collinear k s ↔ ↑(finrank k ↥(vectorSpan k s)) ≤ 1
⊢ Collinear k s ↔ finrank k ↥(vectorSpan k s) ≤ 1

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
s : Set P
inst✝ : FiniteDimensional k ↥(vectorSpan k s)
h : Collinear k s ↔ ↑(finrank k ↥(vectorSpan k s)) ≤ 1
⊢ Collinear k s ↔ finrank k ↥(vectorSpan k s) ≤ 1

Tactic:
exact mod_cast h

Result:
no goals
-- Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean
theorem tprodL_coe : (tprodL 𝕜).toMultilinearMap = tprod 𝕜 (s := E)

Proof state:
case H
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
m : (i : ι) → E i
⊢ (tprodL 𝕜).toMultilinearMap m = (tprod 𝕜) m

Tactic:
simp only [ContinuousMultilinearMap.coe_coe, tprodL_toFun]

Result:
no goals

Proof state:
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
⊢ (tprodL 𝕜).toMultilinearMap = tprod 𝕜

Tactic:
ext m

Result:
case H
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
m : (i : ι) → E i
⊢ (tprodL 𝕜).toMultilinearMap m = (tprod 𝕜) m
-- Mathlib/Topology/Instances/NNReal/Lemmas.lean
theorem nhds_zero : 𝓝 (0 : ℝ≥0) = ⨅ (a : ℝ≥0) (_ : a ≠ 0), 𝓟 (Iio a) :=
  nhds_bot_order.trans <| by simp only [bot_lt_iff_ne_bot]; rfl

Proof state:
⊢ ⨅ l, ⨅ (_ : ⊥ < l), 𝓟 (Set.Iio l) = ⨅ a, ⨅ (_ : a ≠ 0), 𝓟 (Set.Iio a)

Tactic:
simp only [bot_lt_iff_ne_bot]

Result:
⊢ ⨅ l, ⨅ (_ : l ≠ ⊥), 𝓟 (Set.Iio l) = ⨅ a, ⨅ (_ : a ≠ 0), 𝓟 (Set.Iio a)

Proof state:
⊢ ⨅ l, ⨅ (_ : l ≠ ⊥), 𝓟 (Set.Iio l) = ⨅ a, ⨅ (_ : a ≠ 0), 𝓟 (Set.Iio a)

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean
theorem Even.strictConvexOn_pow {n : ℕ} (hn : Even n) (h : n ≠ 0) :
    StrictConvexOn ℝ Set.univ fun x : ℝ => x ^ n

Proof state:
n : ℕ
hn : Even n
h : n ≠ 0
⊢ StrictConvexOn ℝ univ fun x => x ^ n

Tactic:
apply StrictMono.strictConvexOn_univ_of_deriv (continuous_pow n)

Result:
n : ℕ
hn : Even n
h : n ≠ 0
⊢ StrictMono (deriv fun a => a ^ n)

Proof state:
n : ℕ
hn : Even n
h : 0 < n
⊢ StrictMono fun x => ↑n * x ^ (n - 1)

Tactic:
exact StrictMono.const_mul (Odd.strictMono_pow <| Nat.Even.sub_odd h hn <| Nat.odd_iff.2 rfl)
  (Nat.cast_pos.2 h)

Result:
no goals

Proof state:
n : ℕ
hn : Even n
h : n ≠ 0
⊢ StrictMono (deriv fun a => a ^ n)

Tactic:
rw [deriv_pow']

Result:
n : ℕ
hn : Even n
h : n ≠ 0
⊢ StrictMono fun x => ↑n * x ^ (n - 1)

Proof state:
n : ℕ
hn : Even n
h : n ≠ 0
⊢ StrictMono fun x => ↑n * x ^ (n - 1)

Tactic:
replace h := Nat.pos_of_ne_zero h

Result:
n : ℕ
hn : Even n
h : 0 < n
⊢ StrictMono fun x => ↑n * x ^ (n - 1)
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
/-- Similar to `rank_quotient_add_rank_le` but for `finrank` and a finite `M`. -/
lemma Module.finrank_quotient_add_finrank_le (N : Submodule R M) :
    finrank R (M ⧸ N) + finrank R N ≤ finrank R M

Proof state:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
⊢ finrank R (M ⧸ N) + finrank R ↥N ≤ finrank R M

Tactic:
haveI := nontrivial_of_invariantBasisNumber R

Result:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
this : Nontrivial R
⊢ finrank R (M ⧸ N) + finrank R ↥N ≤ finrank R M

Proof state:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
this : Nontrivial R
⊢ finrank R (M ⧸ N) + finrank R ↥N ≤ finrank R M

Tactic:
have := rank_quotient_add_rank_le N

Result:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
this✝ : Nontrivial R
this : Module.rank R (M ⧸ N) + Module.rank R ↥N ≤ Module.rank R M
⊢ finrank R (M ⧸ N) + finrank R ↥N ≤ finrank R M

Proof state:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
this✝ : Nontrivial R
this : Module.rank R (M ⧸ N) + Module.rank R ↥N ≤ Module.rank R M
⊢ finrank R (M ⧸ N) + finrank R ↥N ≤ finrank R M

Tactic:
rw [← finrank_eq_rank R M, ← finrank_eq_rank R, ← N.finrank_eq_rank] at this

Result:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
this✝ : Nontrivial R
this : ↑(finrank R (M ⧸ N)) + ↑(finrank R ↥N) ≤ ↑(finrank R M)
⊢ finrank R (M ⧸ N) + finrank R ↥N ≤ finrank R M

Proof state:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
this✝ : Nontrivial R
this : ↑(finrank R (M ⧸ N)) + ↑(finrank R ↥N) ≤ ↑(finrank R M)
⊢ finrank R (M ⧸ N) + finrank R ↥N ≤ finrank R M

Tactic:
exact mod_cast this

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean
theorem universallyClosed_eq : @UniversallyClosed = universally (topologically @IsClosedMap)

Proof state:
⊢ @UniversallyClosed = (topologically @IsClosedMap).universally

Tactic:
ext X Y f

Result:
case h.h.h.a
X Y : Scheme
f : X ⟶ Y
⊢ UniversallyClosed f ↔ (topologically @IsClosedMap).universally f

Proof state:
case h.h.h.a
X Y : Scheme
f : X ⟶ Y
⊢ UniversallyClosed f ↔ (topologically @IsClosedMap).universally f

Tactic:
rw [universallyClosed_iff]

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Nat.lean
theorem nonneg_of_normalize_eq_self {z : ℤ} (hz : normalize z = z) : 0 ≤ z

Proof state:
case neg
z : ℤ
hz : -z = z
h : ¬0 ≤ z
⊢ 0 ≤ z

Tactic:
omega

Result:
no goals

Proof state:
case neg
z : ℤ
hz : normalize z = z
h : ¬0 ≤ z
⊢ 0 ≤ z

Tactic:
rw [normalize_of_nonpos (le_of_not_le h)] at hz

Result:
case neg
z : ℤ
hz : -z = z
h : ¬0 ≤ z
⊢ 0 ≤ z

Proof state:
case pos
z : ℤ
hz : normalize z = z
h : 0 ≤ z
⊢ 0 ≤ z

Tactic:
exact h

Result:
no goals

Proof state:
z : ℤ
hz : normalize z = z
⊢ 0 ≤ z

Tactic:
by_cases h : 0 ≤ z

Result:
case pos
z : ℤ
hz : normalize z = z
h : 0 ≤ z
⊢ 0 ≤ z

case neg
z : ℤ
hz : normalize z = z
h : ¬0 ≤ z
⊢ 0 ≤ z
-- Mathlib/Data/Set/NAry.lean
theorem image2_image_left (f : γ → β → δ) (g : α → γ) :
    image2 f (g '' s) t = image2 (fun a b => f (g a) b) s t

Proof state:
case h
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
s : Set α
t : Set β
f : γ → β → δ
g : α → γ
x✝ : δ
⊢ x✝ ∈ image2 f (g '' s) t ↔ x✝ ∈ image2 (fun a b => f (g a) b) s t

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
s : Set α
t : Set β
f : γ → β → δ
g : α → γ
⊢ image2 f (g '' s) t = image2 (fun a b => f (g a) b) s t

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
s : Set α
t : Set β
f : γ → β → δ
g : α → γ
x✝ : δ
⊢ x✝ ∈ image2 f (g '' s) t ↔ x✝ ∈ image2 (fun a b => f (g a) b) s t
-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Lemmas.lean
theorem eq_true_of_find?_eq_some {p : Fin n → Bool} (h : find? p = some i) : p i = true

Proof state:
n : Nat
i✝ : Fin n
p : Fin n → Bool
h : find? p = some i✝
i : Fin n
hi : Option.guard (fun i => p i = true) i = some i✝
⊢ p i✝ = true

Tactic:
simp only [Option.guard] at hi

Result:
n : Nat
i✝ : Fin n
p : Fin n → Bool
h : find? p = some i✝
i : Fin n
hi : (if p i = true then some i else none) = some i✝
⊢ p i✝ = true

Proof state:
case isTrue
n : Nat
i✝ : Fin n
p : Fin n → Bool
h : find? p = some i✝
i : Fin n
h✝ : p i = true
hi : some i = some i✝
⊢ p i✝ = true

Tactic:
cases hi

Result:
case isTrue.refl
n : Nat
i : Fin n
p : Fin n → Bool
h : find? p = some i
h✝ : p i = true
⊢ p i = true

Proof state:
case isTrue.refl
n : Nat
i : Fin n
p : Fin n → Bool
h : find? p = some i
h✝ : p i = true
⊢ p i = true

Tactic:
assumption

Result:
no goals

Proof state:
n : Nat
i✝ : Fin n
p : Fin n → Bool
h : find? p = some i✝
i : Fin n
hi : (if p i = true then some i else none) = some i✝
⊢ p i✝ = true

Tactic:
split at hi

Result:
case isTrue
n : Nat
i✝ : Fin n
p : Fin n → Bool
h : find? p = some i✝
i : Fin n
h✝ : p i = true
hi : some i = some i✝
⊢ p i✝ = true

case isFalse
n : Nat
i✝ : Fin n
p : Fin n → Bool
h : find? p = some i✝
i : Fin n
h✝ : ¬p i = true
hi : none = some i✝
⊢ p i✝ = true

Proof state:
case isFalse
n : Nat
i✝ : Fin n
p : Fin n → Bool
h : find? p = some i✝
i : Fin n
h✝ : ¬p i = true
hi : none = some i✝
⊢ p i✝ = true

Tactic:
contradiction

Result:
no goals
-- Mathlib/Order/Filter/CardinalInter.lean
theorem EventuallyLE.cardinal_bInter {S : Set ι} (hS : #S < c)
    {s t : ∀ i ∈ S, Set α} (h : ∀ i hi, s i hi ≤ᶠ[l] t i hi) :
    ⋂ i ∈ S, s i ‹_› ≤ᶠ[l] ⋂ i ∈ S, t i ‹_›

Proof state:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
S : Set ι
hS : #↑S < c
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋂ i, ⋂ (h : i ∈ S), s i h ≤ᶠ[l] ⋂ i, ⋂ (h : i ∈ S), t i h

Tactic:
simp only [biInter_eq_iInter]

Result:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
S : Set ι
hS : #↑S < c
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋂ x, s ↑x ⋯ ≤ᶠ[l] ⋂ x, t ↑x ⋯

Proof state:
ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
S : Set ι
hS : #↑S < c
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋂ x, s ↑x ⋯ ≤ᶠ[l] ⋂ x, t ↑x ⋯

Tactic:
exact EventuallyLE.cardinal_iInter hS fun i => h i i.2

Result:
no goals
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem dist_self (x : ∀ n, E n) : dist x x = 0

Proof state:
E : ℕ → Type u_1
x : (n : ℕ) → E n
⊢ dist x x = 0

Tactic:
simp [dist]

Result:
no goals