harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem deriv_eq_id_of_nfp_eq_id (h : nfp f = id) : deriv f = id :=
  (IsNormal.eq_iff_zero_and_succ (isNormal_deriv _) IsNormal.refl).2 <| by simp [h]

Proof state:
f : Ordinal.{u} → Ordinal.{u}
h : nfp f = id
⊢ deriv f 0 = id 0 ∧ ∀ (a : Ordinal.{u}), deriv f a = id a → deriv f (succ a) = id (succ a)

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Filter.lean
theorem hasBasis_toFilteriUnion_top (l : IntegrationParams) (I : Box ι) :
    (l.toFilteriUnion I ⊤).HasBasis (fun r : ℝ≥0 → (ι → ℝ) → Ioi (0 : ℝ) => ∀ c, l.RCond (r c))
      fun r => { π | ∃ c, l.MemBaseSet I c (r c) π ∧ π.IsPartition }

Proof state:
ι : Type u_1
inst✝ : Fintype ι
l : IntegrationParams
I : Box ι
⊢ (toFilteriUnion I ⊤).HasBasis (fun r => ∀ (c : ℝ≥0), l.RCond (r c)) fun r =>
    {π | ∃ c, l.MemBaseSet I c (r c) π ∧ π.IsPartition}

Tactic:
simpa only [TaggedPrepartition.isPartition_iff_iUnion_eq, Prepartition.iUnion_top] using
  l.hasBasis_toFilteriUnion I ⊤

Result:
no goals
-- Mathlib/MeasureTheory/Function/Floor.lean
theorem MeasurableSet.image_fract [BorelSpace R] {s : Set R} (hs : MeasurableSet s) :
    MeasurableSet (Int.fract '' s)

Proof state:
R : Type u_2
inst✝⁵ : LinearOrderedRing R
inst✝⁴ : FloorRing R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : MeasurableSpace R
inst✝ : BorelSpace R
s : Set R
hs : MeasurableSet s
⊢ MeasurableSet (⋃ m, (fun x => x + ↑m) ⁻¹' s ∩ Ico 0 1)

Tactic:
exact MeasurableSet.iUnion fun m => (measurable_add_const _ hs).inter measurableSet_Ico

Result:
no goals

Proof state:
R : Type u_2
inst✝⁵ : LinearOrderedRing R
inst✝⁴ : FloorRing R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : MeasurableSpace R
inst✝ : BorelSpace R
s : Set R
hs : MeasurableSet s
⊢ MeasurableSet (Int.fract '' s)

Tactic:
simp only [Int.image_fract, sub_eq_add_neg, image_add_right']

Result:
R : Type u_2
inst✝⁵ : LinearOrderedRing R
inst✝⁴ : FloorRing R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : MeasurableSpace R
inst✝ : BorelSpace R
s : Set R
hs : MeasurableSet s
⊢ MeasurableSet (⋃ m, (fun x => x + ↑m) ⁻¹' s ∩ Ico 0 1)
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem opow_mul_add_lt_opow_mul_succ {b u w : Ordinal} (v : Ordinal) (hw : w < b ^ u) :
    b ^ u * v + w < b ^ u * succ v

Proof state:
b u w v : Ordinal.{u_1}
hw : w < b ^ u
⊢ b ^ u * v + w < b ^ u * succ v

Tactic:
rwa [mul_succ, add_lt_add_iff_left]

Result:
no goals
-- Mathlib/Topology/Separation/Hausdorff.lean
lemma compatible {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y]
    {f : X → Y} (hf : Continuous f) : letI _ := t2Setoid X
    ∀ (a b : X), a ≈ b → f a = f b

Proof state:
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
hf : Continuous f
⊢ t2Setoid X ≤ Setoid.ker f

Tactic:
exact sInf_le <| .of_injective_continuous
  (Setoid.ker_lift_injective _) (hf.quotient_lift fun _ _ ↦ id)

Result:
no goals

Proof state:
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
hf : Continuous f
⊢ ∀ (a b : X), a ≈ b → f a = f b

Tactic:
change t2Setoid X ≤ Setoid.ker f

Result:
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
hf : Continuous f
⊢ t2Setoid X ≤ Setoid.ker f
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem one_div_ne_zero {a : G₀} (h : a ≠ 0) : 1 / a ≠ 0

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
⊢ 1 / a ≠ 0

Tactic:
simpa only [one_div] using inv_ne_zero h

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem head_map {β : Type*} (v : Vector α (n + 1)) (f : α → β) : (v.map f).head = f v.head

Proof state:
case intro.intro
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (map f v).head = f v.head

Tactic:
rw [h, map_cons, head_cons, head_cons]

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
⊢ (map f v).head = f v.head

Tactic:
obtain ⟨a, v', h⟩ := Vector.exists_eq_cons v

Result:
case intro.intro
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (map f v).head = f v.head
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem complete'' : ∃ q : ℚ_[p], ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (f i - q : ℚ_[p]) < ε

Proof state:
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
x : ℚ_[p]
hx : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (x - ↑f i) < ε
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (x - ↑f i) < ε
i : ℕ
hi : i ≥ N
⊢ padicNormE (↑f i - x) < ε

Tactic:
rw [padicNormE.map_sub]

Result:
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
x : ℚ_[p]
hx : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (x - ↑f i) < ε
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (x - ↑f i) < ε
i : ℕ
hi : i ≥ N
⊢ padicNormE (x - ↑f i) < ε

Proof state:
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
x : ℚ_[p]
hx : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (x - ↑f i) < ε
⊢ ∃ q, ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (↑f i - q) < ε

Tactic:
refine ⟨x, fun ε hε => ?_⟩

Result:
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
x : ℚ_[p]
hx : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (x - ↑f i) < ε
ε : ℚ
hε : ε > 0
⊢ ∃ N, ∀ i ≥ N, padicNormE (↑f i - x) < ε

Proof state:
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
x : ℚ_[p]
hx : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (x - ↑f i) < ε
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (x - ↑f i) < ε
⊢ ∃ N, ∀ i ≥ N, padicNormE (↑f i - x) < ε

Tactic:
refine ⟨N, fun i hi => ?_⟩

Result:
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
x : ℚ_[p]
hx : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (x - ↑f i) < ε
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (x - ↑f i) < ε
i : ℕ
hi : i ≥ N
⊢ padicNormE (↑f i - x) < ε

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
⊢ ∃ q, ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (↑f i - q) < ε

Tactic:
obtain ⟨x, hx⟩ := complete' f

Result:
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
x : ℚ_[p]
hx : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (x - ↑f i) < ε
⊢ ∃ q, ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (↑f i - q) < ε

Proof state:
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
x : ℚ_[p]
hx : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (x - ↑f i) < ε
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (x - ↑f i) < ε
i : ℕ
hi : i ≥ N
⊢ padicNormE (x - ↑f i) < ε

Tactic:
exact hN i hi

Result:
no goals

Proof state:
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
x : ℚ_[p]
hx : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (x - ↑f i) < ε
ε : ℚ
hε : ε > 0
⊢ ∃ N, ∀ i ≥ N, padicNormE (↑f i - x) < ε

Tactic:
obtain ⟨N, hN⟩ := hx ε hε

Result:
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ⇑padicNormE
x : ℚ_[p]
hx : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (x - ↑f i) < ε
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ i ≥ N, padicNormE (x - ↑f i) < ε
⊢ ∃ N, ∀ i ≥ N, padicNormE (↑f i - x) < ε
-- Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
theorem Ideal.mul_add_mem_pow_succ_unique [IsDedekindDomain S] (hP : P ≠ ⊥)
    {i : ℕ} (a d d' e e' : S)
    (a_not_mem : a ∉ P ^ (i + 1)) (e_mem : e ∈ P ^ (i + 1)) (e'_mem : e' ∈ P ^ (i + 1))
    (h : a * d + e - (a * d' + e') ∈ P ^ (i + 1)) : d - d' ∈ P

Proof state:
case h.e'_5
S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a d d' e e' : S
a_not_mem : a ∉ P ^ (i + 1)
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : a * d + e - (a * d' + e') ∈ P ^ (i + 1)
⊢ a * (d - d') = a * d + e - (a * d' + e') + (e' - e)

Tactic:
ring

Result:
no goals

Proof state:
S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a d d' e e' : S
a_not_mem : a ∉ P ^ (i + 1)
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : a * d + e - (a * d' + e') ∈ P ^ (i + 1)
⊢ d - d' ∈ P

Tactic:
have h' : a * (d - d') ∈ P ^ (i + 1) := by
  convert Ideal.add_mem _ h (Ideal.sub_mem _ e'_mem e_mem) using 1
  ring

Result:
S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a d d' e e' : S
a_not_mem : a ∉ P ^ (i + 1)
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : a * d + e - (a * d' + e') ∈ P ^ (i + 1)
h' : a * (d - d') ∈ P ^ (i + 1)
⊢ d - d' ∈ P

Proof state:
S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a d d' e e' : S
a_not_mem : a ∉ P ^ (i + 1)
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : a * d + e - (a * d' + e') ∈ P ^ (i + 1)
h' : a * (d - d') ∈ P ^ (i + 1)
⊢ d - d' ∈ P

Tactic:
exact Ideal.mem_prime_of_mul_mem_pow hP a_not_mem h'

Result:
no goals

Proof state:
S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a d d' e e' : S
a_not_mem : a ∉ P ^ (i + 1)
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : a * d + e - (a * d' + e') ∈ P ^ (i + 1)
⊢ a * (d - d') ∈ P ^ (i + 1)

Tactic:
convert Ideal.add_mem _ h (Ideal.sub_mem _ e'_mem e_mem) using 1

Result:
case h.e'_5
S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
a d d' e e' : S
a_not_mem : a ∉ P ^ (i + 1)
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : a * d + e - (a * d' + e') ∈ P ^ (i + 1)
⊢ a * (d - d') = a * d + e - (a * d' + e') + (e' - e)
-- Mathlib/Data/Setoid/Partition.lean
theorem classes_ker_subset_fiber_set {β : Type*} (f : α → β) :
    (Setoid.ker f).classes ⊆ Set.range fun y => { x | f x = y }

Proof state:
case intro
α : Type u_1
β : Type u_2
f : α → β
x : α
⊢ ∃ y, {x | f x = y} = {x_1 | (ker f) x_1 x}

Tactic:
exact ⟨f x, rfl⟩

Result:
no goals

Proof state:
case intro
α : Type u_1
β : Type u_2
f : α → β
x : α
⊢ {x_1 | (ker f) x_1 x} ∈ Set.range fun y => {x | f x = y}

Tactic:
rw [Set.mem_range]

Result:
case intro
α : Type u_1
β : Type u_2
f : α → β
x : α
⊢ ∃ y, {x | f x = y} = {x_1 | (ker f) x_1 x}

Proof state:
α : Type u_1
β : Type u_2
f : α → β
⊢ (ker f).classes ⊆ Set.range fun y => {x | f x = y}

Tactic:
rintro s ⟨x, rfl⟩

Result:
case intro
α : Type u_1
β : Type u_2
f : α → β
x : α
⊢ {x_1 | (ker f) x_1 x} ∈ Set.range fun y => {x | f x = y}
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem integerSetTorsionSMul_stabilizer (a : integerSet K) :
    MulAction.stabilizer (torsion K) a = ⊥

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
ζ : ↥(torsion K)
hζ : ↑↑ζ * ↑(preimageOfMemIntegerSet a) = ↑(preimageOfMemIntegerSet a)
⊢ ↑(preimageOfMemIntegerSet a) ≠ 0

Tactic:
exact nonZeroDivisors.coe_ne_zero _

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
ζ : ↥(torsion K)
hζ : ζ ∈ MulAction.stabilizer (↥(torsion K)) a
⊢ ζ = 1

Tactic:
rwa [MulAction.mem_stabilizer_iff, Subtype.ext_iff, integerSetTorsionSMul_smul_coe,
  unitSMul_smul, ← mixedEmbedding_preimageOfMemIntegerSet, ← map_mul,
  (mixedEmbedding_injective K).eq_iff, ← map_mul, ← RingOfIntegers.ext_iff, mul_eq_right₀,
  Units.val_eq_one, OneMemClass.coe_eq_one] at hζ

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
ζ : ↥(torsion K)
hζ : ↑↑ζ * ↑(preimageOfMemIntegerSet a) = ↑(preimageOfMemIntegerSet a)
⊢ ↑(preimageOfMemIntegerSet a) ≠ 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
⊢ MulAction.stabilizer (↥(torsion K)) a = ⊥

Tactic:
refine (Subgroup.eq_bot_iff_forall _).mpr fun ζ hζ ↦ ?_

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
ζ : ↥(torsion K)
hζ : ζ ∈ MulAction.stabilizer (↥(torsion K)) a
⊢ ζ = 1
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Equal.lean
theorem BitVec.eq_sub_iff_add_eq (a b c : BitVec w) : (a == c + (~~~b + 1#w)) = (a + b == c)

Proof state:
w : Nat
a b c : BitVec w
⊢ a = c - b ↔ a + b = c

Tactic:
exact _root_.BitVec.eq_sub_iff_add_eq

Result:
no goals

Proof state:
w : Nat
a b c : BitVec w
⊢ (a == c + (~~~b + 1#w)) = (a + b == c)

Tactic:
rw [Bool.eq_iff_iff, beq_iff_eq, beq_iff_eq, ← BitVec.neg_eq_not_add, ← @BitVec.sub_toAdd]

Result:
w : Nat
a b c : BitVec w
⊢ a = c - b ↔ a + b = c
-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem dimH_univ (e : E ≃L[𝕜] F) : dimH (univ : Set E) = dimH (univ : Set F)

Proof state:
𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] F
⊢ dimH univ = dimH univ

Tactic:
rw [← e.dimH_preimage, preimage_univ]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
lemma acyclic_of_isZero (hK : IsZero K) :
    K.Acyclic

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
hK : IsZero K
⊢ K.Acyclic

Tactic:
rw [acyclic_iff]

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
hK : IsZero K
⊢ ∀ (i : ι), K.ExactAt i

Proof state:
case h
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
hK : IsZero K
i : ι
⊢ IsZero (K.sc i).X₂

Tactic:
exact (eval _ _ i).map_isZero hK

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
hK : IsZero K
i : ι
⊢ K.ExactAt i

Tactic:
apply ShortComplex.exact_of_isZero_X₂

Result:
case h
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
hK : IsZero K
i : ι
⊢ IsZero (K.sc i).X₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
hK : IsZero K
⊢ ∀ (i : ι), K.ExactAt i

Tactic:
intro i

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
hK : IsZero K
i : ι
⊢ K.ExactAt i
-- Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean
theorem liftIsometry_symm_apply (l : (⨂[𝕜] i, E i) →L[𝕜] F) :
    (liftIsometry 𝕜 E F).symm l = l.compContinuousMultilinearMap (tprodL 𝕜)

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)
F : Type uF
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
l : (⨂[𝕜] (i : ι), E i) →L[𝕜] F
m : (i : ι) → E i
⊢ ((liftEquiv 𝕜 E F).symm l) m = (l.compContinuousMultilinearMap (tprodL 𝕜)) m

Tactic:
simp only [liftEquiv_symm_apply, lift_symm, MultilinearMap.coe_mkContinuous,
  LinearMap.compMultilinearMap_apply, ContinuousLinearMap.coe_coe,
  ContinuousLinearMap.compContinuousMultilinearMap_coe, Function.comp_apply, 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)
F : Type uF
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
l : (⨂[𝕜] (i : ι), E i) →L[𝕜] F
⊢ (liftIsometry 𝕜 E F).symm l = l.compContinuousMultilinearMap (tprodL 𝕜)

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)
F : Type uF
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
l : (⨂[𝕜] (i : ι), E i) →L[𝕜] F
m : (i : ι) → E i
⊢ ((liftIsometry 𝕜 E F).symm l) m = (l.compContinuousMultilinearMap (tprodL 𝕜)) m

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)
F : Type uF
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
l : (⨂[𝕜] (i : ι), E i) →L[𝕜] F
m : (i : ι) → E i
⊢ ((liftIsometry 𝕜 E F).symm l) m = (l.compContinuousMultilinearMap (tprodL 𝕜)) m

Tactic:
change (liftEquiv 𝕜 E F).symm l 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)
F : Type uF
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
l : (⨂[𝕜] (i : ι), E i) →L[𝕜] F
m : (i : ι) → E i
⊢ ((liftEquiv 𝕜 E F).symm l) m = (l.compContinuousMultilinearMap (tprodL 𝕜)) m
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem C_eq_S_sub_X_mul_S (n : ℤ) : C R n = 2 * S R n - X * S R (n - 1)

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ C R n = 2 * S R n - X * S R (n - 1)

Tactic:
linear_combination (norm := ring_nf) - S_eq_X_mul_S_add_C R (n - 1)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem leadingCoeff_add_of_degree_lt' (h : degree q < degree p) :
    leadingCoeff (p + q) = leadingCoeff p

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.degree < p.degree
⊢ (q + p).leadingCoeff = p.leadingCoeff

Tactic:
exact leadingCoeff_add_of_degree_lt h

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.degree < p.degree
⊢ (p + q).leadingCoeff = p.leadingCoeff

Tactic:
rw [add_comm]

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.degree < p.degree
⊢ (q + p).leadingCoeff = p.leadingCoeff
-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
theorem iSupLift_comp_inclusion {i : ι} (h : K i ≤ T) :
    (iSupLift K dir f hf T hT).comp (inclusion h) = f i

Proof state:
case h
R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : NonUnitalSubalgebra R A
hT : T = iSup K
i : ι
h : K i ≤ T
x✝ : ↥(K i)
⊢ ((iSupLift K dir f hf T hT).comp (inclusion h)) x✝ = (f i) x✝

Tactic:
simp only [NonUnitalAlgHom.comp_apply, iSupLift_inclusion]

Result:
no goals

Proof state:
R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : NonUnitalSubalgebra R A
hT : T = iSup K
i : ι
h : K i ≤ T
⊢ (iSupLift K dir f hf T hT).comp (inclusion h) = f i

Tactic:
ext

Result:
case h
R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : NonUnitalSubalgebra R A
hT : T = iSup K
i : ι
h : K i ≤ T
x✝ : ↥(K i)
⊢ ((iSupLift K dir f hf T hT).comp (inclusion h)) x✝ = (f i) x✝
-- Mathlib/Data/Set/Basic.lean
theorem ite_left (s t : Set α) : s.ite s t = s ∪ t

Proof state:
α : Type u
s t : Set α
⊢ s.ite s t = s ∪ t

Tactic:
simp [Set.ite]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem not_eq_of_eq_false {a : Prop} (h : a = False) : (Not a) = True

Proof state:
a : Prop
h : a = False
⊢ (¬a) = True

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Analysis/Complex/TaylorSeries.lean
/-- A function that is complex differentiable on the complex plane is given by evaluating
its Taylor series at any point `c`. -/
lemma taylorSeries_eq_of_entire' {f : ℂ → ℂ} (hf : Differentiable ℂ f) :
    ∑' n : ℕ, (n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z

Proof state:
case h.e'_2.h.e'_5.h
c z : ℂ
f : ℂ → ℂ
hf : Differentiable ℂ f
n : ℕ
⊢ (↑n !)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c

Tactic:
rw [mul_right_comm, smul_eq_mul, smul_eq_mul, mul_assoc]

Result:
no goals

Proof state:
c z : ℂ
f : ℂ → ℂ
hf : Differentiable ℂ f
⊢ ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z

Tactic:
convert taylorSeries_eq_of_entire hf c z using 3 with n

Result:
case h.e'_2.h.e'_5.h
c z : ℂ
f : ℂ → ℂ
hf : Differentiable ℂ f
n : ℕ
⊢ (↑n !)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c
-- Mathlib/Data/Fintype/Sets.lean
theorem toFinset_subset_toFinset [Fintype s] [Fintype t] : s.toFinset ⊆ t.toFinset ↔ s ⊆ t

Proof state:
α : Type u_1
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
⊢ s.toFinset ⊆ t.toFinset ↔ s ⊆ t

Tactic:
simp [Finset.subset_iff, Set.subset_def]

Result:
no goals
-- Mathlib/Analysis/Convex/Topology.lean
theorem segment_subset_closure_openSegment : [x -[𝕜] y] ⊆ closure (openSegment 𝕜 x y)

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝⁸ : LinearOrderedRing 𝕜
inst✝⁷ : DenselyOrdered 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : OrderTopology 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : ContinuousAdd E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
x y : E
⊢ [x-[𝕜]y] ⊆ closure (openSegment 𝕜 x y)

Tactic:
rw [segment_eq_image, openSegment_eq_image, ← closure_Ioo (zero_ne_one' 𝕜)]

Result:
𝕜 : Type u_2
E : Type u_3
inst✝⁸ : LinearOrderedRing 𝕜
inst✝⁷ : DenselyOrdered 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : OrderTopology 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : ContinuousAdd E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
x y : E
⊢ (fun θ => (1 - θ) • x + θ • y) '' closure (Ioo 0 1) ⊆ closure ((fun θ => (1 - θ) • x + θ • y) '' Ioo 0 1)

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝⁸ : LinearOrderedRing 𝕜
inst✝⁷ : DenselyOrdered 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : OrderTopology 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : ContinuousAdd E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
x y : E
⊢ Continuous fun θ => (1 - θ) • x + θ • y

Tactic:
fun_prop

Result:
no goals

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝⁸ : LinearOrderedRing 𝕜
inst✝⁷ : DenselyOrdered 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : OrderTopology 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : ContinuousAdd E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
x y : E
⊢ (fun θ => (1 - θ) • x + θ • y) '' closure (Ioo 0 1) ⊆ closure ((fun θ => (1 - θ) • x + θ • y) '' Ioo 0 1)

Tactic:
exact image_closure_subset_closure_image (by fun_prop)

Result:
no goals
-- Mathlib/Data/Finset/Preimage.lean
theorem image_preimage_of_bij [DecidableEq β] (f : α → β) (s : Finset β)
    (hf : Set.BijOn f (f ⁻¹' ↑s) ↑s) : image f (preimage s f hf.injOn) = s :=
  Finset.coe_inj.1 <| by simpa using hf.image_eq

Proof state:
α : Type u
β : Type v
inst✝ : DecidableEq β
f : α → β
s : Finset β
hf : BijOn f (f ⁻¹' ↑s) ↑s
⊢ ↑(image f (s.preimage f ⋯)) = ↑s

Tactic:
simpa using hf.image_eq

Result:
no goals
-- Mathlib/Topology/MetricSpace/Isometry.lean
theorem ediam_image (hf : Isometry f) (s : Set α) : EMetric.diam (f '' s) = EMetric.diam s :=
  eq_of_forall_ge_iff fun d => by simp only [EMetric.diam_le_iff, forall_mem_image, hf.edist_eq]

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : Isometry f
s : Set α
d : ℝ≥0∞
⊢ EMetric.diam (f '' s) ≤ d ↔ EMetric.diam s ≤ d

Tactic:
simp only [EMetric.diam_le_iff, forall_mem_image, hf.edist_eq]

Result:
no goals