harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Polynomial/UniqueFactorization.lean
theorem Polynomial.exists_monic_irreducible_factor {F : Type*} [Field F] (f : F[X])
    (hu : ¬IsUnit f) : ∃ g : F[X], g.Monic ∧ Irreducible g ∧ g ∣ f

Proof state:
case neg.intro.intro
F : Type u_1
inst✝ : Field F
f : F[X]
hu : ¬IsUnit f
hf✝ : ¬f = 0
g : F[X]
hi : Irreducible g
hf : g ∣ f
ha : Associated g (g * C g.leadingCoeff⁻¹)
⊢ ∃ g, g.Monic ∧ Irreducible g ∧ g ∣ f

Tactic:
exact ⟨_, monic_mul_leadingCoeff_inv hi.ne_zero, ha.irreducible hi, ha.dvd_iff_dvd_left.1 hf⟩

Result:
no goals

Proof state:
case neg
F : Type u_1
inst✝ : Field F
f : F[X]
hu : ¬IsUnit f
hf : ¬f = 0
⊢ ∃ g, g.Monic ∧ Irreducible g ∧ g ∣ f

Tactic:
obtain ⟨g, hi, hf⟩ := WfDvdMonoid.exists_irreducible_factor hu hf

Result:
case neg.intro.intro
F : Type u_1
inst✝ : Field F
f : F[X]
hu : ¬IsUnit f
hf✝ : ¬f = 0
g : F[X]
hi : Irreducible g
hf : g ∣ f
⊢ ∃ g, g.Monic ∧ Irreducible g ∧ g ∣ f

Proof state:
F : Type u_1
inst✝ : Field F
f : F[X]
hu : ¬IsUnit f
⊢ ∃ g, g.Monic ∧ Irreducible g ∧ g ∣ f

Tactic:
by_cases hf : f = 0

Result:
case pos
F : Type u_1
inst✝ : Field F
f : F[X]
hu : ¬IsUnit f
hf : f = 0
⊢ ∃ g, g.Monic ∧ Irreducible g ∧ g ∣ f

case neg
F : Type u_1
inst✝ : Field F
f : F[X]
hu : ¬IsUnit f
hf : ¬f = 0
⊢ ∃ g, g.Monic ∧ Irreducible g ∧ g ∣ f

Proof state:
case neg.intro.intro
F : Type u_1
inst✝ : Field F
f : F[X]
hu : ¬IsUnit f
hf✝ : ¬f = 0
g : F[X]
hi : Irreducible g
hf : g ∣ f
⊢ ∃ g, g.Monic ∧ Irreducible g ∧ g ∣ f

Tactic:
have ha : Associated g (g * C g.leadingCoeff⁻¹) := associated_mul_unit_right _ _ <|
  isUnit_C.2 (leadingCoeff_ne_zero.2 hi.ne_zero).isUnit.inv

Result:
case neg.intro.intro
F : Type u_1
inst✝ : Field F
f : F[X]
hu : ¬IsUnit f
hf✝ : ¬f = 0
g : F[X]
hi : Irreducible g
hf : g ∣ f
ha : Associated g (g * C g.leadingCoeff⁻¹)
⊢ ∃ g, g.Monic ∧ Irreducible g ∧ g ∣ f

Proof state:
case pos
F : Type u_1
inst✝ : Field F
f : F[X]
hu : ¬IsUnit f
hf : f = 0
⊢ ∃ g, g.Monic ∧ Irreducible g ∧ g ∣ f

Tactic:
exact ⟨X, monic_X, irreducible_X, hf ▸ dvd_zero X⟩

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem mem_range {α} [Small.{u} α] {f : α → ZFSet.{u}} {x : ZFSet.{u}} :
    x ∈ range f ↔ x ∈ Set.range f :=
  Quotient.inductionOn x fun y => by
    constructor
    · rintro ⟨z, hz⟩
      exact ⟨(equivShrink α).symm z, Quotient.eq_mk_iff_out.2 hz.symm⟩
    · rintro ⟨z, hz⟩
      use equivShrink α z
      simpa [hz] using PSet.Equiv.symm (Quotient.mk_out y)

Proof state:
case mp.intro
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
y : PSet.{u}
z : (PSet.mk (Shrink.{u, u_1} α) (Quotient.out ∘ f ∘ ⇑(equivShrink α).symm)).Type
hz : y.Equiv ((PSet.mk (Shrink.{u, u_1} α) (Quotient.out ∘ f ∘ ⇑(equivShrink α).symm)).Func z)
⊢ ⟦y⟧ ∈ Set.range f

Tactic:
exact ⟨(equivShrink α).symm z, Quotient.eq_mk_iff_out.2 hz.symm⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
y : PSet.{u}
⊢ ⟦y⟧ ∈ range f ↔ ⟦y⟧ ∈ Set.range f

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
y : PSet.{u}
⊢ ⟦y⟧ ∈ range f → ⟦y⟧ ∈ Set.range f

case mpr
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
y : PSet.{u}
⊢ ⟦y⟧ ∈ Set.range f → ⟦y⟧ ∈ range f

Proof state:
case mp
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
y : PSet.{u}
⊢ ⟦y⟧ ∈ range f → ⟦y⟧ ∈ Set.range f

Tactic:
rintro ⟨z, hz⟩

Result:
case mp.intro
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
y : PSet.{u}
z : (PSet.mk (Shrink.{u, u_1} α) (Quotient.out ∘ f ∘ ⇑(equivShrink α).symm)).Type
hz : y.Equiv ((PSet.mk (Shrink.{u, u_1} α) (Quotient.out ∘ f ∘ ⇑(equivShrink α).symm)).Func z)
⊢ ⟦y⟧ ∈ Set.range f

Proof state:
case h
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
y : PSet.{u}
z : α
hz : f z = ⟦y⟧
⊢ y.Equiv ((PSet.mk (Shrink.{u, u_1} α) (Quotient.out ∘ f ∘ ⇑(equivShrink α).symm)).Func ((equivShrink α) z))

Tactic:
simpa [hz] using PSet.Equiv.symm (Quotient.mk_out y)

Result:
no goals

Proof state:
case mpr.intro
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
y : PSet.{u}
z : α
hz : f z = ⟦y⟧
⊢ ⟦y⟧ ∈ range f

Tactic:
use equivShrink α z

Result:
case h
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
y : PSet.{u}
z : α
hz : f z = ⟦y⟧
⊢ y.Equiv ((PSet.mk (Shrink.{u, u_1} α) (Quotient.out ∘ f ∘ ⇑(equivShrink α).symm)).Func ((equivShrink α) z))

Proof state:
case mpr
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
y : PSet.{u}
⊢ ⟦y⟧ ∈ Set.range f → ⟦y⟧ ∈ range f

Tactic:
rintro ⟨z, hz⟩

Result:
case mpr.intro
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
y : PSet.{u}
z : α
hz : f z = ⟦y⟧
⊢ ⟦y⟧ ∈ range f
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem HasFTaylorSeriesUpToOn.congr_series {q} (hp : HasFTaylorSeriesUpToOn n f p s)
    (hpq : ∀ m : ℕ, m ≤ n → EqOn (p · m) (q · m) s) :
    HasFTaylorSeriesUpToOn n f q s where
  zero_eq x hx

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
p q : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn n f p s
hpq : ∀ (m : ℕ), ↑m ≤ n → EqOn (fun x => p x m) (fun x => q x m) s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
⊢ ↑(m + 1) ≤ n

Tactic:
exact ENat.add_one_natCast_le_withTop_of_lt hm

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
p q : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn n f p s
hpq : ∀ (m : ℕ), ↑m ≤ n → EqOn (fun x => p x m) (fun x => q x m) s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
⊢ HasFDerivWithinAt (fun x => q x m) (q x m.succ).curryLeft s x

Tactic:
refine ((hp.fderivWithin m hm x hx).congr' (hpq m hm.le).symm hx).congr_fderiv ?_

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
p q : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn n f p s
hpq : ∀ (m : ℕ), ↑m ≤ n → EqOn (fun x => p x m) (fun x => q x m) s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
⊢ (p x m.succ).curryLeft = (q x m.succ).curryLeft

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
p q : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn n f p s
hpq : ∀ (m : ℕ), ↑m ≤ n → EqOn (fun x => p x m) (fun x => q x m) s
x : E
hx : x ∈ s
⊢ (q x 0).curry0 = f x

Tactic:
simp only [← (hpq 0 (zero_le n) hx), hp.zero_eq x hx]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
p q : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn n f p s
hpq : ∀ (m : ℕ), ↑m ≤ n → EqOn (fun x => p x m) (fun x => q x m) s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
⊢ (p x m.succ).curryLeft = (q x m.succ).curryLeft

Tactic:
refine congrArg _ (hpq (m + 1) ?_ hx)

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
p q : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn n f p s
hpq : ∀ (m : ℕ), ↑m ≤ n → EqOn (fun x => p x m) (fun x => q x m) s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
⊢ ↑(m + 1) ≤ n
-- Mathlib/Data/List/Sigma.lean
theorem of_mem_dlookup {a : α} {b : β a} :
    ∀ {l : List (Sigma β)}, b ∈ dlookup a l → Sigma.mk a b ∈ l
  | ⟨a', b'⟩ :: l, H => by
    by_cases h : a = a'
    · subst a'
      simp? at H says simp only [dlookup_cons_eq, Option.mem_def, Option.some.injEq] at H
      simp [H]
    · simp only [ne_eq, h, not_false_iff, dlookup_cons_ne] at H
      simp [of_mem_dlookup H]

Proof state:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
H : b ∈ dlookup a (⟨a', b'⟩ :: l)
h : ¬a = a'
⊢ ⟨a, b⟩ ∈ ⟨a', b'⟩ :: l

Tactic:
simp only [ne_eq, h, not_false_iff, dlookup_cons_ne] at H

Result:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
H : b ∈ dlookup a l
⊢ ⟨a, b⟩ ∈ ⟨a', b'⟩ :: l

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
b' : β a
H : b ∈ dlookup a (⟨a, b'⟩ :: l)
⊢ ⟨a, b⟩ ∈ ⟨a, b'⟩ :: l

Tactic:
simp only [dlookup_cons_eq, Option.mem_def, Option.some.injEq] at H

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
b' : β a
H : b' = b
⊢ ⟨a, b⟩ ∈ ⟨a, b'⟩ :: l

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
H : b ∈ dlookup a (⟨a', b'⟩ :: l)
⊢ ⟨a, b⟩ ∈ ⟨a', b'⟩ :: l

Tactic:
by_cases h : a = a'

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
H : b ∈ dlookup a (⟨a', b'⟩ :: l)
h : a = a'
⊢ ⟨a, b⟩ ∈ ⟨a', b'⟩ :: l

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
H : b ∈ dlookup a (⟨a', b'⟩ :: l)
h : ¬a = a'
⊢ ⟨a, b⟩ ∈ ⟨a', b'⟩ :: l

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
b' : β a
H : b ∈ dlookup a (⟨a, b'⟩ :: l)
⊢ ⟨a, b⟩ ∈ ⟨a, b'⟩ :: l

Tactic:
simp? at H says simp only [dlookup_cons_eq, Option.mem_def, Option.some.injEq] at H

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
b' : β a
H : b' = b
⊢ ⟨a, b⟩ ∈ ⟨a, b'⟩ :: l

Proof state:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
H : b ∈ dlookup a l
⊢ ⟨a, b⟩ ∈ ⟨a', b'⟩ :: l

Tactic:
simp [of_mem_dlookup H]

Result:
no goals

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
b' : β a
H : b' = b
⊢ ⟨a, b⟩ ∈ ⟨a, b'⟩ :: l

Tactic:
simp [H]

Result:
no goals

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
H : b ∈ dlookup a (⟨a', b'⟩ :: l)
h : a = a'
⊢ ⟨a, b⟩ ∈ ⟨a', b'⟩ :: l

Tactic:
subst a'

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
b' : β a
H : b ∈ dlookup a (⟨a, b'⟩ :: l)
⊢ ⟨a, b⟩ ∈ ⟨a, b'⟩ :: l
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem measurable_of_Ioi {f : δ → α} (hf : ∀ x, MeasurableSet (f ⁻¹' Ioi x)) : Measurable f

Proof state:
case h.e'_4
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ioi x)
⊢ mα = MeasurableSpace.generateFrom ?convert_2

Tactic:
exact BorelSpace.measurable_eq.trans (borel_eq_generateFrom_Ioi _)

Result:
no goals

Proof state:
case convert_4.intro
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ioi x)
x : α
⊢ MeasurableSet (f ⁻¹' Ioi x)

Tactic:
exact hf x

Result:
no goals

Proof state:
case convert_4
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ioi x)
⊢ ∀ t ∈ range Ioi, MeasurableSet (f ⁻¹' t)

Tactic:
rintro _ ⟨x, rfl⟩

Result:
case convert_4.intro
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ioi x)
x : α
⊢ MeasurableSet (f ⁻¹' Ioi x)

Proof state:
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ioi x)
⊢ Measurable f

Tactic:
convert measurable_generateFrom (α := δ) _

Result:
case h.e'_4
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ioi x)
⊢ mα = MeasurableSpace.generateFrom ?convert_2

case convert_2
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ioi x)
⊢ Set (Set α)

case convert_4
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ioi x)
⊢ ∀ t ∈ ?convert_2, MeasurableSet (f ⁻¹' t)
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
theorem rank_le {n : ℕ}
    (H : ∀ s : Finset M, (LinearIndependent R fun i : s => (i : M)) → s.card ≤ n) :
    Module.rank R M ≤ n

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n
⊢ ⨆ ι, #↑↑ι ≤ ↑n

Tactic:
apply ciSup_le'

Result:
case h
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n
⊢ ∀ (i : { s // LinearIndepOn R id s }), #↑↑i ≤ ↑n

Proof state:
case h
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n
⊢ ∀ (i : { s // LinearIndepOn R id s }), #↑↑i ≤ ↑n

Tactic:
rintro ⟨s, li⟩

Result:
case h.mk
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n
s : Set M
li : LinearIndepOn R id s
⊢ #↑↑⟨s, li⟩ ≤ ↑n

Proof state:
case h.mk
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n
s : Set M
li : LinearIndepOn R id s
⊢ #↑↑⟨s, li⟩ ≤ ↑n

Tactic:
exact linearIndependent_bounded_of_finset_linearIndependent_bounded H _ li

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n
⊢ Module.rank R M ≤ ↑n

Tactic:
rw [Module.rank_def]

Result:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n
⊢ ⨆ ι, #↑↑ι ≤ ↑n
-- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
theorem comp_differentiableAt_iff {f : G → E} {x : G} :
    DifferentiableAt 𝕜 (iso ∘ f) x ↔ DifferentiableAt 𝕜 f x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
x : G
⊢ DifferentiableAt 𝕜 (⇑iso ∘ f) x ↔ DifferentiableAt 𝕜 f x

Tactic:
rw [← differentiableWithinAt_univ, ← differentiableWithinAt_univ,
  iso.comp_differentiableWithinAt_iff]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem eq_adjoint_iff_basis_left {ι : Type*} (b : Basis ι 𝕜 E) (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E) :
    A = LinearMap.adjoint B ↔ ∀ i y, ⟪A (b i), y⟫ = ⟪b i, B y⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
ι : Type u_5
b : Basis ι 𝕜 E
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : ∀ (i : ι) (y : F), ⟪A (b i), y⟫_𝕜 = ⟪b i, B y⟫_𝕜
i : ι
y : F
⊢ ⟪A (b i), y⟫_𝕜 = ⟪(adjoint B) (b i), y⟫_𝕜

Tactic:
simp only [h i, adjoint_inner_left]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
ι : Type u_5
b : Basis ι 𝕜 E
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : ∀ (i : ι) (y : F), ⟪A (b i), y⟫_𝕜 = ⟪b i, B y⟫_𝕜
i : ι
⊢ A (b i) = (adjoint B) (b i)

Tactic:
exact ext_inner_right 𝕜 fun y => by simp only [h i, adjoint_inner_left]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
ι : Type u_5
b : Basis ι 𝕜 E
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
⊢ A = adjoint B ↔ ∀ (i : ι) (y : F), ⟪A (b i), y⟫_𝕜 = ⟪b i, B y⟫_𝕜

Tactic:
refine ⟨fun h x y => by rw [h, adjoint_inner_left], fun h => Basis.ext b fun i => ?_⟩

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
ι : Type u_5
b : Basis ι 𝕜 E
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : ∀ (i : ι) (y : F), ⟪A (b i), y⟫_𝕜 = ⟪b i, B y⟫_𝕜
i : ι
⊢ A (b i) = (adjoint B) (b i)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
ι : Type u_5
b : Basis ι 𝕜 E
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : A = adjoint B
x : ι
y : F
⊢ ⟪A (b x), y⟫_𝕜 = ⟪b x, B y⟫_𝕜

Tactic:
rw [h, adjoint_inner_left]

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/Three.lean
/-- We have that `η ^ 2 + η + 1 = 0`. -/
lemma eta_sq_add_eta_add_one : (η : 𝓞 K) ^ 2 + η + 1 = 0

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
⊢ ↑η ^ 2 + ↑η + 1 = 0

Tactic:
rw [eta_sq]

Result:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
⊢ -↑η - 1 + ↑η + 1 = 0

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
⊢ -↑η - 1 + ↑η + 1 = 0

Tactic:
ring

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Fold.lean
theorem foldRev_eq_finRange_foldr {α : Type u} (n : Nat) (f : (i : Nat) → i < n → α → α) (init : α) :
    foldRev n f init = (List.finRange n).foldr (fun ⟨i, h⟩ acc => f i h acc) init

Proof state:
case succ
α : Type u
n : Nat
ih :
  ∀ (f : (i : Nat) → i < n → α → α) (init : α),
    n.foldRev f init =
      List.foldr
        (fun x acc =>
          match x with
          | ⟨i, h⟩ => f i h acc)
        init (List.finRange n)
f : (i : Nat) → i < n + 1 → α → α
init : α
⊢ (n + 1).foldRev f init =
    List.foldr
      (fun x acc =>
        match x with
        | ⟨i, h⟩ => f i h acc)
      init (List.finRange (n + 1))

Tactic:
simp [ih, List.finRange_succ_last, List.foldr_map]

Result:
no goals

Proof state:
α : Type u
n : Nat
f : (i : Nat) → i < n → α → α
init : α
⊢ n.foldRev f init =
    List.foldr
      (fun x acc =>
        match x with
        | ⟨i, h⟩ => f i h acc)
      init (List.finRange n)

Tactic:
induction n generalizing init with
| zero => simp
| succ n ih => simp [ih, List.finRange_succ_last, List.foldr_map]

Result:
no goals

Proof state:
case zero
α : Type u
f : (i : Nat) → i < 0 → α → α
init : α
⊢ foldRev 0 f init =
    List.foldr
      (fun x acc =>
        match x with
        | ⟨i, h⟩ => f i h acc)
      init (List.finRange 0)

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/Bounded.lean
theorem diam_triple :
    Metric.diam ({x, y, z} : Set α) = max (max (dist x y) (dist x z)) (dist y z)

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y z : α
⊢ (edist x y ⊔ edist x z ⊔ edist y z).toReal = (edist x y).toReal ⊔ (edist x z).toReal ⊔ (edist y z).toReal

Tactic:
rw [ENNReal.toReal_max, ENNReal.toReal_max] <;> apply_rules [ne_of_lt, edist_lt_top, max_lt]

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y z : α
⊢ diam {x, y, z} = dist x y ⊔ dist x z ⊔ dist y z

Tactic:
simp only [Metric.diam, EMetric.diam_triple, dist_edist]

Result:
α : Type u
inst✝ : PseudoMetricSpace α
x y z : α
⊢ (edist x y ⊔ edist x z ⊔ edist y z).toReal = (edist x y).toReal ⊔ (edist x z).toReal ⊔ (edist y z).toReal
-- Mathlib/Algebra/Polynomial/Eval/Coeff.lean
theorem eval_natCast_map (f : R →+* S) (p : R[X]) (n : ℕ) :
    (p.map f).eval (n : S) = f (p.eval n)

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
⊢ eval (↑n) (map f p) = f (eval (↑n) p)

Tactic:
induction p using Polynomial.induction_on' with
| h_add p q hp hq =>
  simp only [hp, hq, Polynomial.map_add, RingHom.map_add, eval_add]
| h_monomial n r =>
  simp only [map_natCast f, eval_monomial, map_monomial, f.map_pow, f.map_mul]

Result:
no goals

Proof state:
case h_monomial
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
n✝ n : ℕ
r : R
⊢ eval (↑n✝) (map f ((monomial n) r)) = f (eval (↑n✝) ((monomial n) r))

Tactic:
simp only [map_natCast f, eval_monomial, map_monomial, f.map_pow, f.map_mul]

Result:
no goals

Proof state:
case h_add
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
n : ℕ
p q : R[X]
hp : eval (↑n) (map f p) = f (eval (↑n) p)
hq : eval (↑n) (map f q) = f (eval (↑n) q)
⊢ eval (↑n) (map f (p + q)) = f (eval (↑n) (p + q))

Tactic:
simp only [hp, hq, Polynomial.map_add, RingHom.map_add, eval_add]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Divisibility.lean
theorem dvdNotUnit_of_dvd_of_not_dvd {a b : α} (hd : a ∣ b) (hnd : ¬b ∣ a) : DvdNotUnit a b

Proof state:
case left
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ a ≠ 0

Tactic:
rintro rfl

Result:
case left
α : Type u_1
inst✝ : CommMonoidWithZero α
b : α
hd : 0 ∣ b
hnd : ¬b ∣ 0
⊢ False

Proof state:
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ DvdNotUnit a b

Tactic:
constructor

Result:
case left
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ a ≠ 0

case right
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ ∃ x, ¬IsUnit x ∧ b = a * x

Proof state:
case right
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ ∃ x, ¬IsUnit x ∧ b = a * x

Tactic:
rcases hd with ⟨c, rfl⟩

Result:
case right.intro
α : Type u_1
inst✝ : CommMonoidWithZero α
a c : α
hnd : ¬a * c ∣ a
⊢ ∃ x, ¬IsUnit x ∧ a * c = a * x

Proof state:
case right.intro
α : Type u_1
inst✝ : CommMonoidWithZero α
a c : α
hnd : ¬a * c ∣ a
⊢ ∃ x, ¬IsUnit x ∧ a * c = a * x

Tactic:
refine ⟨c, ?_, rfl⟩

Result:
case right.intro
α : Type u_1
inst✝ : CommMonoidWithZero α
a c : α
hnd : ¬a * c ∣ a
⊢ ¬IsUnit c

Proof state:
case left
α : Type u_1
inst✝ : CommMonoidWithZero α
b : α
hd : 0 ∣ b
hnd : ¬b ∣ 0
⊢ False

Tactic:
exact hnd (dvd_zero _)

Result:
no goals

Proof state:
case right.intro
α : Type u_1
inst✝ : CommMonoidWithZero α
a c : α
hnd : ¬a * c ∣ a
⊢ ¬IsUnit c

Tactic:
rintro ⟨u, rfl⟩

Result:
case right.intro.intro
α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
u : αˣ
hnd : ¬a * ↑u ∣ a
⊢ False

Proof state:
case right.intro.intro
α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
u : αˣ
hnd : ¬a * ↑u ∣ a
⊢ False

Tactic:
simp at hnd

Result:
no goals