harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
theorem carrier.zero_mem : (0 : A) ∈ carrier f_deg q := fun i => by
  convert Submodule.zero_mem q.1 using 1
  rw [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk,
    HomogeneousLocalization.val_zero]; simp_rw [map_zero, zero_pow hm.ne']
  convert Localization.mk_zero (S := Submonoid.powers f) _ using 1

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
i : ℕ
⊢ HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) 0 ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } ∈ q.asIdeal

Tactic:
convert Submodule.zero_mem q.1 using 1

Result:
case h.e'_5
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
i : ℕ
⊢ HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) 0 ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } = 0

Proof state:
case h.e'_5
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
i : ℕ
⊢ Localization.mk ↑{ deg := m * i, num := ⟨(proj 𝒜 i) 0 ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.num
      ⟨↑{ deg := m * i, num := ⟨(proj 𝒜 i) 0 ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.den, ⋯⟩ =
    0

Tactic:
simp_rw [map_zero, zero_pow hm.ne']

Result:
case h.e'_5
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
i : ℕ
⊢ Localization.mk 0 ⟨f ^ i, ⋯⟩ = 0

Proof state:
case h.e'_5
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
i : ℕ
⊢ Localization.mk 0 ⟨f ^ i, ⋯⟩ = 0

Tactic:
convert Localization.mk_zero (S := Submonoid.powers f) _ using 1

Result:
no goals

Proof state:
case h.e'_5
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
i : ℕ
⊢ HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) 0 ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } = 0

Tactic:
rw [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk,
  HomogeneousLocalization.val_zero]

Result:
case h.e'_5
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
i : ℕ
⊢ Localization.mk ↑{ deg := m * i, num := ⟨(proj 𝒜 i) 0 ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.num
      ⟨↑{ deg := m * i, num := ⟨(proj 𝒜 i) 0 ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }.den, ⋯⟩ =
    0
-- Mathlib/SetTheory/Ordinal/Veblen.lean
theorem veblenWith_veblenWith_of_lt (h : o₁ < o₂) (a : Ordinal) :
    veblenWith f o₁ (veblenWith f o₂ a) = veblenWith f o₂ a

Proof state:
case H
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ : Ordinal.{u}
hf : IsNormal f
h : o₁ < o₂
a : Ordinal.{u}
x : ↑(Set.Iio o₂) := ⟨o₁, h⟩
⊢ IsNormal (veblenWith f ↑x)

Tactic:
exact hf.veblenWith x

Result:
no goals

Proof state:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ : Ordinal.{u}
hf : IsNormal f
h : o₁ < o₂
a : Ordinal.{u}
⊢ veblenWith f o₁ (veblenWith f o₂ a) = veblenWith f o₂ a

Tactic:
let x : Set.Iio _ := ⟨o₁, h⟩

Result:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ : Ordinal.{u}
hf : IsNormal f
h : o₁ < o₂
a : Ordinal.{u}
x : ↑(Set.Iio o₂) := ⟨o₁, h⟩
⊢ veblenWith f o₁ (veblenWith f o₂ a) = veblenWith f o₂ a

Proof state:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ : Ordinal.{u}
hf : IsNormal f
h : o₁ < o₂
a : Ordinal.{u}
x : ↑(Set.Iio o₂) := ⟨o₁, h⟩
⊢ veblenWith f o₁ (veblenWith f o₂ a) = veblenWith f o₂ a

Tactic:
rw [veblenWith_of_ne_zero f h.bot_lt.ne',
  derivFamily_fp (f := fun y : Set.Iio o₂ ↦ veblenWith f y.1) (i := x)]

Result:
case H
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ : Ordinal.{u}
hf : IsNormal f
h : o₁ < o₂
a : Ordinal.{u}
x : ↑(Set.Iio o₂) := ⟨o₁, h⟩
⊢ IsNormal (veblenWith f ↑x)
-- Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean
theorem ArithmeticFunction.LSeries_zeta_eulerProduct_exp_log {s : ℂ} (hs : 1 < s.re) :
    exp (∑' p : Nat.Primes, -Complex.log (1 - p ^ (-s))) = L 1 s

Proof state:
s : ℂ
hs : 1 < s.re
⊢ cexp (∑' (p : Primes), -Complex.log (1 - ↑↑p ^ (-s))) = L 1 s

Tactic:
convert modOne_eq_one (R := ℂ) ▸
  DirichletCharacter.LSeries_eulerProduct_exp_log (1 : DirichletCharacter ℂ 1) hs using 7

Result:
case h.e'_2.h.e'_1.h.e'_5.h.h.e'_3.h.e'_1.h.e'_6
s : ℂ
hs : 1 < s.re
x✝ : Primes
⊢ ↑↑x✝ ^ (-s) = 1 ↑↑x✝ * ↑↑x✝ ^ (-s)

Proof state:
case h.e'_2.h.e'_1.h.e'_5.h.h.e'_3.h.e'_1.h.e'_6
s : ℂ
hs : 1 < s.re
x✝ : Primes
⊢ ↑↑x✝ ^ (-s) = 1 ↑↑x✝ * ↑↑x✝ ^ (-s)

Tactic:
rw [MulChar.one_apply <| isUnit_of_subsingleton _, one_mul]

Result:
no goals
-- Mathlib/LinearAlgebra/Isomorphisms.lean
theorem quotientInfEquivSupQuotient_injective (p p' : Submodule R M) :
    Function.Injective (quotientInfToSupQuotient p p')

Proof state:
case h'
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ ker (subToSupQuotient p p') ≤ comap p.subtype (p ⊓ p')

Tactic:
rw [ker_comp, ker_mkQ]

Result:
case h'
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ comap (inclusion ⋯) (comap (p ⊔ p').subtype p') ≤ comap p.subtype (p ⊓ p')

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ Function.Injective ⇑(quotientInfToSupQuotient p p')

Tactic:
rw [← ker_eq_bot, quotientInfToSupQuotient, ker_liftQ_eq_bot]

Result:
case h'
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ ker (subToSupQuotient p p') ≤ comap p.subtype (p ⊓ p')

Proof state:
case h'
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ comap (inclusion ⋯) (comap (p ⊔ p').subtype p') ≤ comap p.subtype (p ⊓ p')

Tactic:
exact fun ⟨x, hx1⟩ hx2 => ⟨hx1, hx2⟩

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem isBasis_affine_open (X : Scheme) : Opens.IsBasis X.affineOpens

Proof state:
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hU : x ∈ ↑U
⊢ ∃ U' ∈ X.affineOpens, x ∈ U' ∧ U' ≤ U

Tactic:
obtain ⟨S, hS, hxS, hSU⟩ := X.affineBasisCover_is_basis.exists_subset_of_mem_open hU U.isOpen

Result:
case intro.intro.intro
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hU : x ∈ ↑U
S : Set ↑↑X.toPresheafedSpace
hS : S ∈ {x | ∃ a, x = Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map a).base)}
hxS : x ∈ S
hSU : S ⊆ ↑U
⊢ ∃ U' ∈ X.affineOpens, x ∈ U' ∧ U' ≤ U

Proof state:
case intro.intro.intro.intro
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hU : x ∈ ↑U
i : X.affineBasisCover.J
hxS : x ∈ Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map i).base)
hSU : Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map i).base) ⊆ ↑U
⊢ { carrier := Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map i).base), is_open' := ⋯ } ∈ X.affineOpens

Tactic:
exact isAffineOpen_opensRange _

Result:
no goals

Proof state:
X : Scheme
⊢ Opens.IsBasis X.affineOpens

Tactic:
rw [Opens.isBasis_iff_nbhd]

Result:
X : Scheme
⊢ ∀ {U : Opens ↑↑X.toPresheafedSpace} {x : ↑↑X.toPresheafedSpace}, x ∈ U → ∃ U' ∈ X.affineOpens, x ∈ U' ∧ U' ≤ U

Proof state:
case intro.intro.intro
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hU : x ∈ ↑U
S : Set ↑↑X.toPresheafedSpace
hS : S ∈ {x | ∃ a, x = Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map a).base)}
hxS : x ∈ S
hSU : S ⊆ ↑U
⊢ ∃ U' ∈ X.affineOpens, x ∈ U' ∧ U' ≤ U

Tactic:
refine ⟨⟨S, X.affineBasisCover_is_basis.isOpen hS⟩, ?_, hxS, hSU⟩

Result:
case intro.intro.intro
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hU : x ∈ ↑U
S : Set ↑↑X.toPresheafedSpace
hS : S ∈ {x | ∃ a, x = Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map a).base)}
hxS : x ∈ S
hSU : S ⊆ ↑U
⊢ { carrier := S, is_open' := ⋯ } ∈ X.affineOpens

Proof state:
case intro.intro.intro
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hU : x ∈ ↑U
S : Set ↑↑X.toPresheafedSpace
hS : S ∈ {x | ∃ a, x = Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map a).base)}
hxS : x ∈ S
hSU : S ⊆ ↑U
⊢ { carrier := S, is_open' := ⋯ } ∈ X.affineOpens

Tactic:
rcases hS with ⟨i, rfl⟩

Result:
case intro.intro.intro.intro
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hU : x ∈ ↑U
i : X.affineBasisCover.J
hxS : x ∈ Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map i).base)
hSU : Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map i).base) ⊆ ↑U
⊢ { carrier := Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map i).base), is_open' := ⋯ } ∈ X.affineOpens

Proof state:
X : Scheme
⊢ ∀ {U : Opens ↑↑X.toPresheafedSpace} {x : ↑↑X.toPresheafedSpace}, x ∈ U → ∃ U' ∈ X.affineOpens, x ∈ U' ∧ U' ≤ U

Tactic:
rintro U x (hU : x ∈ (U : Set X))

Result:
X : Scheme
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑X.toPresheafedSpace
hU : x ∈ ↑U
⊢ ∃ U' ∈ X.affineOpens, x ∈ U' ∧ U' ≤ U
-- Mathlib/Data/Real/Irrational.lean
theorem mul_cases : Irrational (x * y) → Irrational x ∨ Irrational y

Proof state:
x y : ℝ
⊢ x * y ∉ Set.range Rat.cast → x ∉ Set.range Rat.cast ∨ y ∉ Set.range Rat.cast

Tactic:
contrapose!

Result:
x y : ℝ
⊢ x ∈ Set.range Rat.cast ∧ y ∈ Set.range Rat.cast → x * y ∈ Set.range Rat.cast

Proof state:
x y : ℝ
⊢ Irrational (x * y) → Irrational x ∨ Irrational y

Tactic:
delta Irrational

Result:
x y : ℝ
⊢ x * y ∉ Set.range Rat.cast → x ∉ Set.range Rat.cast ∨ y ∉ Set.range Rat.cast

Proof state:
x y : ℝ
⊢ x ∈ Set.range Rat.cast ∧ y ∈ Set.range Rat.cast → x * y ∈ Set.range Rat.cast

Tactic:
rintro ⟨⟨rx, rfl⟩, ⟨ry, rfl⟩⟩

Result:
case intro.intro.intro
rx ry : ℚ
⊢ ↑rx * ↑ry ∈ Set.range Rat.cast

Proof state:
case intro.intro.intro
rx ry : ℚ
⊢ ↑rx * ↑ry ∈ Set.range Rat.cast

Tactic:
exact ⟨rx * ry, cast_mul rx ry⟩

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Circulant.lean
theorem Fin.circulant_ite (α) [Zero α] [One α] :
    ∀ n, circulant (fun i => ite (i.1 = 0) 1 0 : Fin n → α) = 1
  | 0 => by simp [Injective, eq_iff_true_of_subsingleton]
  | n + 1 => by
    rw [← circulant_single_one]
    congr with j
    simp [Pi.single_apply]

Proof state:
α : Type u_5
inst✝¹ : Zero α
inst✝ : One α
⊢ (circulant fun i => if ↑i = 0 then 1 else 0) = 1

Tactic:
simp [Injective, eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
α : Type u_5
inst✝¹ : Zero α
inst✝ : One α
n : ℕ
⊢ (circulant fun i => if ↑i = 0 then 1 else 0) = 1

Tactic:
rw [← circulant_single_one]

Result:
α : Type u_5
inst✝¹ : Zero α
inst✝ : One α
n : ℕ
⊢ (circulant fun i => if ↑i = 0 then 1 else 0) = circulant (Pi.single 0 1)

Proof state:
α : Type u_5
inst✝¹ : Zero α
inst✝ : One α
n : ℕ
⊢ (circulant fun i => if ↑i = 0 then 1 else 0) = circulant (Pi.single 0 1)

Tactic:
congr with j

Result:
case a
α : Type u_5
inst✝¹ : Zero α
inst✝ : One α
n : ℕ
j j✝ : Fin (n + 1)
⊢ circulant (fun i => if ↑i = 0 then 1 else 0) j j✝ = circulant (Pi.single 0 1) j j✝

Proof state:
case a
α : Type u_5
inst✝¹ : Zero α
inst✝ : One α
n : ℕ
j j✝ : Fin (n + 1)
⊢ circulant (fun i => if ↑i = 0 then 1 else 0) j j✝ = circulant (Pi.single 0 1) j j✝

Tactic:
simp [Pi.single_apply]

Result:
no goals
-- Mathlib/Order/CompleteBooleanAlgebra.lean
theorem compl_iSup : (iSup f)ᶜ = ⨅ i, (f i)ᶜ :=
  compl_injective (by simp [compl_iInf])

Proof state:
α : Type u
ι : Sort w
inst✝ : CompleteBooleanAlgebra α
f : ι → α
⊢ (iSup f)ᶜᶜ = (⨅ i, (f i)ᶜ)ᶜ

Tactic:
simp [compl_iInf]

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject.lean
@[simp]
lemma mapMap_id : mapMap (𝟙 X) p = 𝟙 _

Proof state:
I : Type u_1
J : Type u_2
C : Type u_4
inst✝¹ : Category.{u_5, u_4} C
X : GradedObject I C
p : I → J
inst✝ : X.HasMap p
⊢ mapMap (𝟙 X) p = 𝟙 (X.mapObj p)

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Basic.lean
theorem LinearIndependent.eq_coords_of_eq [Fintype ι] {v : ι → M} (hv : LinearIndependent R v)
    {f : ι → R} {g : ι → R} (heq : ∑ i, f i • v i = ∑ i, g i • v i) (i : ι) : f i = g i

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Fintype ι
v : ι → M
hv : LinearIndependent R v
f g : ι → R
heq : ∑ x : ι, (f x • v x - g x • v x) = 0
i : ι
⊢ f i = g i

Tactic:
simp_rw [← sub_smul] at heq

Result:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Fintype ι
v : ι → M
hv : LinearIndependent R v
f g : ι → R
i : ι
heq : ∑ x : ι, (f x - g x) • v x = 0
⊢ f i = g i

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Fintype ι
v : ι → M
hv : LinearIndependent R v
f g : ι → R
i : ι
heq : ∑ x : ι, (f x - g x) • v x = 0
⊢ f i = g i

Tactic:
exact sub_eq_zero.mp ((linearIndependent_iff'.mp hv) univ (fun i ↦ f i - g i) heq i (mem_univ i))

Result:
no goals

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Fintype ι
v : ι → M
hv : LinearIndependent R v
f g : ι → R
heq : ∑ i : ι, f i • v i = ∑ i : ι, g i • v i
i : ι
⊢ f i = g i

Tactic:
rw [← sub_eq_zero, ← sum_sub_distrib] at heq

Result:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Fintype ι
v : ι → M
hv : LinearIndependent R v
f g : ι → R
heq : ∑ x : ι, (f x • v x - g x • v x) = 0
i : ι
⊢ f i = g i
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
lemma differentiableAt_comp_const_sub {a b : 𝕜} :
    DifferentiableAt 𝕜 (fun x ↦ f (b - x)) a ↔ DifferentiableAt 𝕜 f (b - a)

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
H : DifferentiableAt 𝕜 (fun x => f (b - x)) a
⊢ DifferentiableAt 𝕜 f (b - a)

Tactic:
convert ((sub_sub_cancel _ a).symm ▸ H).comp (b - a)
  (differentiable_id.const_sub _).differentiableAt

Result:
case h.e'_11
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
H : DifferentiableAt 𝕜 (fun x => f (b - x)) a
⊢ f = (fun x => f (b - x)) ∘ HSub.hSub b

Proof state:
case h.e'_11.h
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
H : DifferentiableAt 𝕜 (fun x => f (b - x)) a
x✝ : 𝕜
⊢ f x✝ = ((fun x => f (b - x)) ∘ HSub.hSub b) x✝

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
⊢ DifferentiableAt 𝕜 (fun x => f (b - x)) a ↔ DifferentiableAt 𝕜 f (b - a)

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ H.comp a (differentiable_id.const_sub _).differentiableAt⟩

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
H : DifferentiableAt 𝕜 (fun x => f (b - x)) a
⊢ DifferentiableAt 𝕜 f (b - a)

Proof state:
case h.e'_11
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
H : DifferentiableAt 𝕜 (fun x => f (b - x)) a
⊢ f = (fun x => f (b - x)) ∘ HSub.hSub b

Tactic:
ext

Result:
case h.e'_11.h
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
H : DifferentiableAt 𝕜 (fun x => f (b - x)) a
x✝ : 𝕜
⊢ f x✝ = ((fun x => f (b - x)) ∘ HSub.hSub b) x✝
-- Mathlib/RingTheory/Polynomial/ScaleRoots.lean
theorem support_scaleRoots_le (p : R[X]) (s : R) : (scaleRoots p s).support ≤ p.support

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
a✝ : ℕ
⊢ a✝ ∈ (p.scaleRoots s).support → a✝ ∈ p.support

Tactic:
simpa using left_ne_zero_of_mul

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
⊢ (p.scaleRoots s).support ≤ p.support

Tactic:
intro

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
a✝ : ℕ
⊢ a✝ ∈ (p.scaleRoots s).support → a✝ ∈ p.support
-- Mathlib/Order/CompleteLattice.lean
lemma isLUB_iff_sSup_eq : IsLUB s a ↔ sSup s = a :=
  ⟨(isLUB_sSup s).unique, by rintro rfl; exact isLUB_sSup _⟩

Proof state:
α : Type u_1
inst✝ : CompleteSemilatticeSup α
s : Set α
⊢ IsLUB s (sSup s)

Tactic:
exact isLUB_sSup _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CompleteSemilatticeSup α
s : Set α
a : α
⊢ sSup s = a → IsLUB s a

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝ : CompleteSemilatticeSup α
s : Set α
⊢ IsLUB s (sSup s)
-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
theorem map_esymm (n : ℕ) (f : R →+* S) : map f (esymm σ R n) = esymm σ S n

Proof state:
S : Type u_4
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Fintype σ
n : ℕ
f : R →+* S
⊢ (map f) (esymm σ R n) = esymm σ S n

Tactic:
simp_rw [esymm, map_sum, map_prod, map_X]

Result:
no goals
-- Mathlib/Order/WithBot.lean
/-- A version of `lt_top_iff_ne_top` for `WithTop` that only requires `LT α`, not
`PartialOrder α`. -/
protected lemma lt_top_iff_ne_top : x < ⊤ ↔ x ≠ ⊤

Proof state:
α : Type u_1
inst✝ : LT α
x : WithTop α
⊢ x < ⊤ ↔ x ≠ ⊤

Tactic:
cases x <;> simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/ComplexDeriv.lean
theorem continuousAt_tan {x : ℂ} : ContinuousAt tan x ↔ cos x ≠ 0

Proof state:
x : ℂ
hc : ContinuousAt tan x
h₀ : cos x = 0
⊢ False

Tactic:
exact not_tendsto_nhds_of_tendsto_atTop (tendsto_norm_tan_of_cos_eq_zero h₀) _
  (hc.norm.tendsto.mono_left inf_le_left)

Result:
no goals

Proof state:
x : ℂ
⊢ ContinuousAt tan x ↔ cos x ≠ 0

Tactic:
refine ⟨fun hc h₀ => ?_, fun h => (hasDerivAt_tan h).continuousAt⟩

Result:
x : ℂ
hc : ContinuousAt tan x
h₀ : cos x = 0
⊢ False
-- Mathlib/Data/Vector/Basic.lean
theorem prod_set [Monoid α] (v : Vector α n) (i : Fin n) (a : α) :
    (v.set i a).toList.prod = (v.take i).toList.prod * a * (v.drop (i + 1)).toList.prod

Proof state:
α : Type u_1
n : ℕ
inst✝ : Monoid α
v : Vector α n
i : Fin n
a : α
⊢ ((List.take (↑i) v.toList).prod * if ↑i < v.toList.length then a else 1) * (List.drop (↑i + 1) v.toList).prod =
    (take (↑i) v).toList.prod * a * (drop (↑i + 1) v).toList.prod

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
inst✝ : Monoid α
v : Vector α n
i : Fin n
a : α
⊢ (v.set i a).toList.prod = (take (↑i) v).toList.prod * a * (drop (↑i + 1) v).toList.prod

Tactic:
refine (List.prod_set v.toList i a).trans ?_

Result:
α : Type u_1
n : ℕ
inst✝ : Monoid α
v : Vector α n
i : Fin n
a : α
⊢ ((List.take (↑i) v.toList).prod * if ↑i < v.toList.length then a else 1) * (List.drop (↑i + 1) v.toList).prod =
    (take (↑i) v).toList.prod * a * (drop (↑i + 1) v).toList.prod
-- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
theorem measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_right
    (hab : IntervalIntegrable f μ a b) (hmeas : StronglyMeasurableAtFilter f lb' μ)
    (hf : Tendsto f (lb' ⊓ ae μ) (𝓝 c)) (hu : Tendsto u lt lb) (hv : Tendsto v lt lb) :
    (fun t => ((∫ x in a..v t, f x ∂μ) - ∫ x in a..u t, f x ∂μ) - ∫ _ in u t..v t, c ∂μ) =o[lt]
      fun t => ∫ _ in u t..v t, (1 : ℝ) ∂μ

Proof state:
ι : Type u_1
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
c : E
lb lb' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst✝¹ : FTCFilter b lb lb'
inst✝ : IsLocallyFiniteMeasure μ
hab : IntervalIntegrable f μ a b
hmeas : StronglyMeasurableAtFilter f lb' μ
hf : Tendsto f (lb' ⊓ ae μ) (𝓝 c)
hu : Tendsto u lt lb
hv : Tendsto v lt lb
⊢ (fun t => ∫ (x : ℝ) in a..v t, f x ∂μ - ∫ (x : ℝ) in a..u t, f x ∂μ - ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt] fun t =>
    ∫ (x : ℝ) in u t..v t, 1 ∂μ

Tactic:
simpa using
  measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae hab stronglyMeasurableAt_bot
    hmeas ((tendsto_bot : Tendsto _ ⊥ (𝓝 (0 : E))).mono_left inf_le_left) hf
    (tendsto_const_pure : Tendsto _ _ (pure a)) tendsto_const_pure hu hv

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem natDegree_C_mul_le (a : R) (f : R[X]) : (C a * f).natDegree ≤ f.natDegree

Proof state:
R : Type u
inst✝ : Semiring R
a : R
f : R[X]
⊢ (C a * f).natDegree ≤ f.natDegree

Tactic:
simpa using natDegree_mul_le (p := C a)

Result:
no goals
-- Mathlib/Algebra/Order/Group/DenselyOrdered.lean
theorem le_of_forall_one_lt_div_le (h : ∀ ε : α, 1 < ε → a / ε ≤ b) : a ≤ b :=
  le_of_forall_lt_one_mul_le fun ε ε1 => by
    simpa only [div_eq_mul_inv, inv_inv] using h ε⁻¹ (Left.one_lt_inv_iff.2 ε1)

Proof state:
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
inst✝ : DenselyOrdered α
a b : α
h : ∀ (ε : α), 1 < ε → a / ε ≤ b
ε : α
ε1 : ε < 1
⊢ a * ε ≤ b

Tactic:
simpa only [div_eq_mul_inv, inv_inv] using h ε⁻¹ (Left.one_lt_inv_iff.2 ε1)

Result:
no goals
-- Mathlib/Data/Bundle.lean
theorem TotalSpace.mk_cast {x x' : B} (h : x = x') (b : E x) :
    .mk' F x' (cast (congr_arg E h) b) = TotalSpace.mk x b

Proof state:
B : Type u_1
F : Type u_2
E : B → Type u_3
x x' : B
h : x = x'
b : E x
⊢ mk' F x' (cast ⋯ b) = { proj := x, snd := b }

Tactic:
subst h

Result:
B : Type u_1
F : Type u_2
E : B → Type u_3
x : B
b : E x
⊢ mk' F x (cast ⋯ b) = { proj := x, snd := b }

Proof state:
B : Type u_1
F : Type u_2
E : B → Type u_3
x : B
b : E x
⊢ mk' F x (cast ⋯ b) = { proj := x, snd := b }

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/WF.lean
theorem fixFEq (x : α) (acx : Acc r x) : fixF F x acx = F x (fun (y : α) (p : r y x) => fixF F y (Acc.inv acx p))

Proof state:
α : Sort u
r : α → α → Prop
C : α → Sort v
F : (x : α) → ((y : α) → r y x → C y) → C x
x : α
acx : Acc r x
⊢ fixF F x acx = F x fun y p => fixF F y ⋯

Tactic:
induction acx with
| intro x r _ => exact rfl

Result:
no goals

Proof state:
case intro
α : Sort u
r✝ : α → α → Prop
C : α → Sort v
F : (x : α) → ((y : α) → r✝ y x → C y) → C x
x✝ x : α
r : ∀ (y : α), r✝ y x → Acc r✝ y
h_ih✝ : ∀ (y : α) (a : r✝ y x), fixF F y ⋯ = F y fun y_1 p => fixF F y_1 ⋯
⊢ fixF F x ⋯ = F x fun y p => fixF F y ⋯

Tactic:
exact rfl

Result:
no goals