harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
private lemma uniformity_eq_seminorm :
    𝓤 (ContinuousMultilinearMap 𝕜 E G) = ⨅ r > 0, 𝓟 {f | ‖f.1 - f.2‖ < r}

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
c : 𝕜
hc : 1 < ‖c‖
hc₀ : 0 < ‖c‖
f : ContinuousMultilinearMap 𝕜 E G
hf : ∀ (x : (i : ι) → E i), ‖x‖ ≤ ‖c‖ → ‖f x‖ ≤ 1
x : (i : ι) → E i
hcx : ∀ (i : ι), ‖c‖ / ‖c‖ ≤ ‖x i‖
hx : ∀ (i : ι), ‖x i‖ < ‖c‖
⊢ 1 = ∏ i : ι, 1

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Sum.lean
@[simp] lemma toRight_cons_inr (hb) :
    (cons (inr b) u hb).toRight = cons b u.toRight (by simpa)

Proof state:
case h
α : Type u_1
β : Type u_2
b : β
u : Finset (α ⊕ β)
hb : inr b ∉ u
y : β
⊢ y ∈ (cons (inr b) u hb).toRight ↔ y ∈ cons b u.toRight ⋯

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
s₁ s₂ : Finset α
t₁ t₂ : Finset β
a : α
b : β
x : α ⊕ β
u v : Finset (α ⊕ β)
hb : inr b ∉ u
⊢ b ∉ u.toRight

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
b : β
u : Finset (α ⊕ β)
hb : inr b ∉ u
⊢ (cons (inr b) u hb).toRight = cons b u.toRight ⋯

Tactic:
ext y

Result:
case h
α : Type u_1
β : Type u_2
b : β
u : Finset (α ⊕ β)
hb : inr b ∉ u
y : β
⊢ y ∈ (cons (inr b) u hb).toRight ↔ y ∈ cons b u.toRight ⋯
-- Mathlib/CategoryTheory/FintypeCat.lean
lemma uSwitchEquiv_symm_naturality {X Y : FintypeCat.{u}} (f : X ⟶ Y) (x : X) :
    uSwitch.map f (X.uSwitchEquiv.symm x) = Y.uSwitchEquiv.symm (f x)

Proof state:
X Y : FintypeCat
f : X ⟶ Y
x : X.carrier
⊢ uSwitch.map f (X.uSwitchEquiv.symm x) = Y.uSwitchEquiv.symm (f x)

Tactic:
rw [← Equiv.apply_eq_iff_eq_symm_apply, ← uSwitchEquiv_naturality f,
  Equiv.apply_symm_apply]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem norm_eq_zero_iff {f : lp E p} : ‖f‖ = 0 ↔ f = 0

Proof state:
case inr.inr.h.h
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
hf : (fun i => ‖↑f i‖ ^ p.toReal) = 0
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal
i : α
⊢ ↑f i = ↑0 i

Tactic:
have : f i = 0 ∧ p.toReal ≠ 0 := by
  simpa [Real.rpow_eq_zero_iff_of_nonneg (norm_nonneg (f i))] using congr_fun hf i

Result:
case inr.inr.h.h
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
hf : (fun i => ‖↑f i‖ ^ p.toReal) = 0
this✝ : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal
i : α
this : ↑f i = 0 ∧ p.toReal ≠ 0
⊢ ↑f i = ↑0 i

Proof state:
case inl.h.h
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E 0)
h : ‖f‖ = 0
i : α
this✝ : {i | ¬↑f i = 0} = ∅
this : (¬↑f i = 0) = False
⊢ ↑f i = ↑0 i

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ ‖0‖ = 0

Tactic:
exact norm_zero

Result:
no goals

Proof state:
case inr.inl.inr.h.h
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ⊤)
h : ‖f‖ = 0
_i : Nonempty α
H : IsLUB (Set.range fun i => ‖↑f i‖) 0
i : α
this : ‖↑f i‖ = 0
⊢ ↑f i = ↑0 i

Tactic:
simpa using this

Result:
no goals

Proof state:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
hf : HasSum (fun i => ‖↑f i‖ ^ p.toReal) 0
⊢ f = 0

Tactic:
have : ∀ i, 0 ≤ ‖f i‖ ^ p.toReal := fun i => Real.rpow_nonneg (norm_nonneg _) _

Result:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
hf : HasSum (fun i => ‖↑f i‖ ^ p.toReal) 0
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal
⊢ f = 0
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc]
lemma comm (h : HomologyMapData φ h₁ h₂) :
    h.left.φH ≫ h₂.iso.hom = h₁.iso.hom ≫ h.right.φH

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
h : HomologyMapData φ h₁ h₂
⊢ h.left.φH ≫ h₂.iso.hom = h₁.iso.hom ≫ h.right.φH

Tactic:
simp only [← cancel_epi h₁.left.π, ← cancel_mono h₂.right.ι, assoc,
  LeftHomologyMapData.commπ_assoc, HomologyData.comm, LeftHomologyMapData.commi_assoc,
  RightHomologyMapData.commι, HomologyData.comm_assoc, RightHomologyMapData.commp]

Result:
no goals
-- Mathlib/Algebra/EuclideanDomain/Basic.lean
theorem mod_eq_zero {a b : R} : a % b = 0 ↔ b ∣ a :=
  ⟨fun h => by
    rw [← div_add_mod a b, h, add_zero]
    exact dvd_mul_right _ _, fun ⟨c, e⟩ => by
    rw [e, ← add_left_cancel_iff, div_add_mod, add_zero]
    haveI := Classical.dec
    by_cases b0 : b = 0
    · simp only [b0, zero_mul]
    · rw [mul_div_cancel_left₀ _ b0]⟩

Proof state:
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
⊢ b * c = b * (b * c / b)

Tactic:
by_cases b0 : b = 0

Result:
case pos
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
b0 : b = 0
⊢ b * c = b * (b * c / b)

case neg
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
b0 : ¬b = 0
⊢ b * c = b * (b * c / b)

Proof state:
case pos
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
b0 : b = 0
⊢ b * c = b * (b * c / b)

Tactic:
simp only [b0, zero_mul]

Result:
no goals

Proof state:
R : Type u
inst✝ : EuclideanDomain R
a b : R
h : a % b = 0
⊢ b ∣ b * (a / b)

Tactic:
exact dvd_mul_right _ _

Result:
no goals

Proof state:
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
⊢ b * c = b * (b * c / b)

Tactic:
haveI := Classical.dec

Result:
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
⊢ b * c = b * (b * c / b)

Proof state:
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
⊢ a % b = 0

Tactic:
rw [e, ← add_left_cancel_iff, div_add_mod, add_zero]

Result:
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
⊢ b * c = b * (b * c / b)

Proof state:
R : Type u
inst✝ : EuclideanDomain R
a b : R
h : a % b = 0
⊢ b ∣ a

Tactic:
rw [← div_add_mod a b, h, add_zero]

Result:
R : Type u
inst✝ : EuclideanDomain R
a b : R
h : a % b = 0
⊢ b ∣ b * (a / b)

Proof state:
case neg
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
b0 : ¬b = 0
⊢ b * c = b * (b * c / b)

Tactic:
rw [mul_div_cancel_left₀ _ b0]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean
theorem Basis.le_span {J : Set M} (v : Basis ι R M) (hJ : span R J = ⊤) : #(range v) ≤ #J

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
inst✝ : RankCondition R
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
this✝ : Nontrivial R
val✝ : Infinite ↑J
S : ↑J → Set ι := fun j => ↑(v.repr ↑j).support
S' : ↑J → Set M := fun j => ⇑v '' S j
hs : range ⇑v ⊆ ⋃ j, S' j
IJ : #↑J < #↑(range ⇑v)
this : #↑(⋃ j, S' j) < #↑(range ⇑v)
⊢ False

Tactic:
exact not_le_of_lt this ⟨Set.embeddingOfSubset _ _ hs⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldl_append {β : Type _} (f : β → α → β) (b) (l l' : Array α) :
    (l ++ l').foldl f b = l'.foldl f (l.foldl f b)

Proof state:
α : Type u_1
β : Type u_2
f : β → α → β
b : β
l l' : Array α
⊢ foldl f b (l ++ l') = foldl f (foldl f b l) l'

Tactic:
simp [foldl_eq_foldlM]

Result:
no goals
-- Mathlib/NumberTheory/FLT/Three.lean
/-- Given `S' : Solution'`, then `S'.a` and `S'.b` are both congruent to `1` modulo `λ ^ 4` or are
both congruent to `-1`. -/
lemma a_cube_b_cube_congr_one_or_neg_one :
    λ ^ 4 ∣ S'.a ^ 3 - 1 ∧ λ ^ 4 ∣ S'.b ^ 3 + 1 ∨ λ ^ 4 ∣ S'.a ^ 3 + 1 ∧ λ ^ 4 ∣ S'.b ^ 3 - 1

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ✝
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (↑3 ^ 1)
⊢ ↑S'.u * ((hζ✝.toInteger - 1) * z) ^ 3 - (hζ✝.toInteger - 1) ^ 4 * x - (hζ✝.toInteger - 1) ^ 4 * y =
    S'.a ^ 3 + S'.b ^ 3 - (S'.a ^ 3 - 1) - (S'.b ^ 3 - 1)

Tactic:
rw [← hx, ← hy, ← hz, ← S'.H]

Result:
no goals

Proof state:
case intro.inr.intro.inr.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = λ * z
x : 𝓞 K
hx : S'.a ^ 3 + 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = λ ^ 4 * y
⊢ False

Tactic:
replace hζ : IsPrimitiveRoot ζ ((3 : ℕ+) ^ 1) := by rwa [pow_one]

Result:
case intro.inr.intro.inr.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ✝
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 + 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (↑3 ^ 1)
⊢ False

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ✝
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 + 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 + 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (↑3 ^ 1)
⊢ (hζ.toInteger - 1) * ((hζ✝.toInteger - 1) ^ 3 * (x + y) - ↑S'.u * (hζ✝.toInteger - 1) ^ 2 * z ^ 3) =
    (hζ✝.toInteger - 1) ^ 4 * x + (hζ✝.toInteger - 1) ^ 4 * y - ↑S'.u * ((hζ✝.toInteger - 1) * z) ^ 3

Tactic:
ring

Result:
no goals

Proof state:
case intro.inl.intro.inl.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = λ * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = λ ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = λ ^ 4 * y
⊢ False

Tactic:
replace hζ : IsPrimitiveRoot ζ ((3 : ℕ+) ^ 1) := by rwa [pow_one]

Result:
case intro.inl.intro.inl.intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ✝
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
z : 𝓞 K
hz : S'.c = (hζ✝.toInteger - 1) * z
x : 𝓞 K
hx : S'.a ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * x
y : 𝓞 K
hy : S'.b ^ 3 - 1 = (hζ✝.toInteger - 1) ^ 4 * y
hζ : IsPrimitiveRoot ζ (↑3 ^ 1)
⊢ False
-- Mathlib/Data/Set/Card.lean
theorem eq_insert_of_ncard_eq_succ {n : ℕ} (h : s.ncard = n + 1) :
    ∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n

Proof state:
case intro.intro.intro.intro.refine_1
α : Type u_1
s : Set α
hsf : s.Finite
a : α
t : Finset α
hat : a ∉ t
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
⊢ insert a ↑t = s

Tactic:
simp [Set.ext_iff, hts]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
n : ℕ
h : s.ncard = n + 1
hsf : s.Finite
⊢ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n

Tactic:
rw [ncard_eq_toFinset_card _ hsf, Finset.card_eq_succ] at h

Result:
α : Type u_1
s : Set α
n : ℕ
hsf : s.Finite
h : ∃ a t, a ∉ t ∧ insert a t = hsf.toFinset ∧ t.card = n
⊢ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n

Proof state:
case intro.intro.intro.intro
α : Type u_1
s : Set α
hsf : s.Finite
a : α
t : Finset α
hat : a ∉ t
hts : insert a t = hsf.toFinset
⊢ ∃ a t_1, a ∉ t_1 ∧ insert a t_1 = s ∧ t_1.ncard = t.card

Tactic:
simp only [Finset.ext_iff, Finset.mem_insert, Finite.mem_toFinset] at hts

Result:
case intro.intro.intro.intro
α : Type u_1
s : Set α
hsf : s.Finite
a : α
t : Finset α
hat : a ∉ t
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
⊢ ∃ a t_1, a ∉ t_1 ∧ insert a t_1 = s ∧ t_1.ncard = t.card

Proof state:
case intro.intro.intro.intro.refine_2
α : Type u_1
s : Set α
hsf : s.Finite
a : α
t : Finset α
hat : a ∉ t
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
⊢ (↑t).ncard = t.card

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_1
s : Set α
hsf : s.Finite
a : α
t : Finset α
hat : a ∉ t
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
⊢ ∃ a t_1, a ∉ t_1 ∧ insert a t_1 = s ∧ t_1.ncard = t.card

Tactic:
refine ⟨a, t, hat, ?_, ?_⟩

Result:
case intro.intro.intro.intro.refine_1
α : Type u_1
s : Set α
hsf : s.Finite
a : α
t : Finset α
hat : a ∉ t
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
⊢ insert a ↑t = s

case intro.intro.intro.intro.refine_2
α : Type u_1
s : Set α
hsf : s.Finite
a : α
t : Finset α
hat : a ∉ t
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
⊢ (↑t).ncard = t.card

Proof state:
α : Type u_1
s : Set α
n : ℕ
hsf : s.Finite
h : ∃ a t, a ∉ t ∧ insert a t = hsf.toFinset ∧ t.card = n
⊢ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n

Tactic:
obtain ⟨a, t, hat, hts, rfl⟩ := h

Result:
case intro.intro.intro.intro
α : Type u_1
s : Set α
hsf : s.Finite
a : α
t : Finset α
hat : a ∉ t
hts : insert a t = hsf.toFinset
⊢ ∃ a t_1, a ∉ t_1 ∧ insert a t_1 = s ∧ t_1.ncard = t.card

Proof state:
α : Type u_1
s : Set α
n : ℕ
h : s.ncard = n + 1
⊢ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n

Tactic:
have hsf := finite_of_ncard_pos (n.zero_lt_succ.trans_eq h.symm)

Result:
α : Type u_1
s : Set α
n : ℕ
h : s.ncard = n + 1
hsf : s.Finite
⊢ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n
-- Mathlib/CategoryTheory/Shift/Basic.lean
lemma shiftFunctorAdd_zero_add_hom_app (a : A) (X : C) :
    (shiftFunctorAdd C 0 a).hom.app X =
    eqToHom (by dsimp; rw [zero_add]) ≫ ((shiftFunctorZero C A).inv.app X)⟦a⟧'

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctor C (0 + a)).obj X = (shiftFunctor C a).obj X

Tactic:
rw [zero_add]

Result:
no goals

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctor C (0 + a)).obj X = (shiftFunctor C a).obj ((𝟭 C).obj X)

Tactic:
dsimp

Result:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctor C (0 + a)).obj X = (shiftFunctor C a).obj X

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctorAdd C 0 a).hom.app X = eqToHom ⋯ ≫ (shiftFunctor C a).map ((shiftFunctorZero C A).inv.app X)

Tactic:
simp [← shiftFunctorAdd'_zero_add_hom_app, shiftFunctorAdd']

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean
theorem tsub_tsub_tsub_cancel_right (h : c ≤ b) : a - c - (b - c) = a - b

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
h : c ≤ b
⊢ a - c - (b - c) = a - b

Tactic:
rw [tsub_tsub, add_tsub_cancel_of_le h]

Result:
no goals
-- Mathlib/Topology/Order/UpperLowerSetTopology.lean
lemma upperSet_le_upper {t₁ t₂ : TopologicalSpace α} [@Topology.IsUpperSet α t₁ _]
    [@Topology.IsUpper α t₂ _] : t₁ ≤ t₂ := fun s hs => by
  rw [@isOpen_iff_isUpperSet α _ t₁]
  exact IsUpper.isUpperSet_of_isOpen hs

Proof state:
α : Type u_1
inst✝² : Preorder α
t₁ t₂ : TopologicalSpace α
inst✝¹ : Topology.IsUpperSet α
inst✝ : IsUpper α
s : Set α
hs : IsOpen s
⊢ IsOpen s

Tactic:
rw [@isOpen_iff_isUpperSet α _ t₁]

Result:
α : Type u_1
inst✝² : Preorder α
t₁ t₂ : TopologicalSpace α
inst✝¹ : Topology.IsUpperSet α
inst✝ : IsUpper α
s : Set α
hs : IsOpen s
⊢ IsUpperSet s

Proof state:
α : Type u_1
inst✝² : Preorder α
t₁ t₂ : TopologicalSpace α
inst✝¹ : Topology.IsUpperSet α
inst✝ : IsUpper α
s : Set α
hs : IsOpen s
⊢ IsUpperSet s

Tactic:
exact IsUpper.isUpperSet_of_isOpen hs

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem CPolynomialOn.fderiv (h : CPolynomialOn 𝕜 f s) :
    CPolynomialOn 𝕜 (fderiv 𝕜 f) s

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
y : E
hy : y ∈ s
⊢ CPolynomialAt 𝕜 (_root_.fderiv 𝕜 f) y

Tactic:
rcases h y hy with ⟨p, r, n, hp⟩

Result:
case intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
y : E
hy : y ∈ s
p : FormalMultilinearSeries 𝕜 E F
r : ℕ
n : ℝ≥0∞
hp : HasFiniteFPowerSeriesOnBall f p y r n
⊢ CPolynomialAt 𝕜 (_root_.fderiv 𝕜 f) y

Proof state:
case intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
y : E
hy : y ∈ s
p : FormalMultilinearSeries 𝕜 E F
r : ℕ
n : ℝ≥0∞
hp : HasFiniteFPowerSeriesOnBall f p y r n
⊢ CPolynomialAt 𝕜 (_root_.fderiv 𝕜 f) y

Tactic:
exact hp.fderiv'.cPolynomialAt

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
⊢ CPolynomialOn 𝕜 (_root_.fderiv 𝕜 f) s

Tactic:
intro y hy

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
y : E
hy : y ∈ s
⊢ CPolynomialAt 𝕜 (_root_.fderiv 𝕜 f) y
-- Mathlib/CategoryTheory/Shift/CommShift.lean
lemma of_isIso [IsIso τ] [NatTrans.CommShift τ A] :
    NatTrans.CommShift (inv τ) A

Proof state:
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_7, u_1} C
inst✝⁷ : Category.{u_6, u_2} D
F₁ F₂ : C ⥤ D
τ : F₁ ⟶ F₂
A : Type u_5
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
inst✝⁴ : HasShift D A
inst✝³ : F₁.CommShift A
inst✝² : F₂.CommShift A
inst✝¹ : IsIso τ
inst✝ : CommShift τ A
this : CommShift (asIso τ).hom A
⊢ CommShift (asIso τ).inv A

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_7, u_1} C
inst✝⁷ : Category.{u_6, u_2} D
F₁ F₂ : C ⥤ D
τ : F₁ ⟶ F₂
A : Type u_5
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
inst✝⁴ : HasShift D A
inst✝³ : F₁.CommShift A
inst✝² : F₂.CommShift A
inst✝¹ : IsIso τ
inst✝ : CommShift τ A
this : CommShift (asIso τ).hom A
⊢ CommShift (inv τ) A

Tactic:
change NatTrans.CommShift (asIso τ).inv A

Result:
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_7, u_1} C
inst✝⁷ : Category.{u_6, u_2} D
F₁ F₂ : C ⥤ D
τ : F₁ ⟶ F₂
A : Type u_5
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
inst✝⁴ : HasShift D A
inst✝³ : F₁.CommShift A
inst✝² : F₂.CommShift A
inst✝¹ : IsIso τ
inst✝ : CommShift τ A
this : CommShift (asIso τ).hom A
⊢ CommShift (asIso τ).inv A

Proof state:
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_7, u_1} C
inst✝⁷ : Category.{u_6, u_2} D
F₁ F₂ : C ⥤ D
τ : F₁ ⟶ F₂
A : Type u_5
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
inst✝⁴ : HasShift D A
inst✝³ : F₁.CommShift A
inst✝² : F₂.CommShift A
inst✝¹ : IsIso τ
inst✝ : CommShift τ A
⊢ CommShift (asIso τ).hom A

Tactic:
assumption

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_7, u_1} C
inst✝⁷ : Category.{u_6, u_2} D
F₁ F₂ : C ⥤ D
τ : F₁ ⟶ F₂
A : Type u_5
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
inst✝⁴ : HasShift D A
inst✝³ : F₁.CommShift A
inst✝² : F₂.CommShift A
inst✝¹ : IsIso τ
inst✝ : CommShift τ A
⊢ CommShift (inv τ) A

Tactic:
haveI : NatTrans.CommShift (asIso τ).hom A := by assumption

Result:
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_7, u_1} C
inst✝⁷ : Category.{u_6, u_2} D
F₁ F₂ : C ⥤ D
τ : F₁ ⟶ F₂
A : Type u_5
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
inst✝⁴ : HasShift D A
inst✝³ : F₁.CommShift A
inst✝² : F₂.CommShift A
inst✝¹ : IsIso τ
inst✝ : CommShift τ A
this : CommShift (asIso τ).hom A
⊢ CommShift (inv τ) A
-- Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
theorem sup_mem_closed_subalgebra (A : Subalgebra ℝ C(X, ℝ)) (h : IsClosed (A : Set C(X, ℝ)))
    (f g : A) : (f : C(X, ℝ)) ⊔ (g : C(X, ℝ)) ∈ A

Proof state:
case h.e'_4.h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : ↥A
⊢ IsClosed ↑A.toSubsemiring

Tactic:
exact h

Result:
no goals

Proof state:
case h.e'_4.h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : ↥A
⊢ ↑A = ↑A.topologicalClosure

Tactic:
symm

Result:
case h.e'_4.h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : ↥A
⊢ ↑A.topologicalClosure = ↑A

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : ↥A
⊢ ↑f ⊔ ↑g ∈ A

Tactic:
convert sup_mem_subalgebra_closure A f g

Result:
case h.e'_4
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : ↥A
⊢ A = A.topologicalClosure

Proof state:
case h.e'_4.h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : ↥A
⊢ ↑A.topologicalClosure = ↑A

Tactic:
erw [closure_eq_iff_isClosed]

Result:
case h.e'_4.h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : ↥A
⊢ IsClosed ↑A.toSubsemiring

Proof state:
case h.e'_4
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : ↥A
⊢ A = A.topologicalClosure

Tactic:
apply SetLike.ext'

Result:
case h.e'_4.h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
h : IsClosed ↑A
f g : ↥A
⊢ ↑A = ↑A.topologicalClosure