harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
lemma toSpec_base_apply_eq {f} (x : Proj| pbo f) :
    (toSpec 𝒜 f).base x = ProjIsoSpecTopComponent.toSpec 𝒜 f x :=
  toSpec_base_apply_eq_comap 𝒜 x |>.trans <| PrimeSpectrum.ext <| Ideal.ext fun z =>
  show ¬ IsUnit _ ↔ z ∈ ProjIsoSpecTopComponent.ToSpec.carrier _ by
  obtain ⟨z, rfl⟩ := z.mk_surjective
  rw [← HomogeneousLocalization.isUnit_iff_isUnit_val,
    ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier, HomogeneousLocalization.map_mk,
    HomogeneousLocalization.val_mk, Localization.mk_eq_mk',
    IsLocalization.AtPrime.isUnit_mk'_iff]
  exact not_not

Proof state:
case intro
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
x : ↑(Proj.restrict ⋯).toTopCat
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ ↑{ deg := z.deg, num := ⟨(RingHom.id A) ↑z.num, ⋯⟩, den := ⟨(RingHom.id A) ↑z.den, ⋯⟩, den_mem := ⋯ }.num ∉
      (↑x).asHomogeneousIdeal.toIdeal.primeCompl ↔
    ↑z.num ∈ (↑x).asHomogeneousIdeal

Tactic:
exact not_not

Result:
no goals

Proof state:
case intro
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
x : ↑(Proj.restrict ⋯).toTopCat
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ ¬IsUnit ((mapId 𝒜 ⋯) (HomogeneousLocalization.mk z)) ↔
    HomogeneousLocalization.mk z ∈ ProjIsoSpecTopComponent.ToSpec.carrier x

Tactic:
rw [← HomogeneousLocalization.isUnit_iff_isUnit_val,
  ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier, HomogeneousLocalization.map_mk,
  HomogeneousLocalization.val_mk, Localization.mk_eq_mk',
  IsLocalization.AtPrime.isUnit_mk'_iff]

Result:
case intro
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
x : ↑(Proj.restrict ⋯).toTopCat
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ ↑{ deg := z.deg, num := ⟨(RingHom.id A) ↑z.num, ⋯⟩, den := ⟨(RingHom.id A) ↑z.den, ⋯⟩, den_mem := ⋯ }.num ∉
      (↑x).asHomogeneousIdeal.toIdeal.primeCompl ↔
    ↑z.num ∈ (↑x).asHomogeneousIdeal

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
x : ↑(Proj.restrict ⋯).toTopCat
z : HomogeneousLocalization 𝒜 (Submonoid.powers f)
⊢ ¬IsUnit ((mapId 𝒜 ⋯) z) ↔ z ∈ ProjIsoSpecTopComponent.ToSpec.carrier x

Tactic:
obtain ⟨z, rfl⟩ := z.mk_surjective

Result:
case intro
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
x : ↑(Proj.restrict ⋯).toTopCat
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ ¬IsUnit ((mapId 𝒜 ⋯) (HomogeneousLocalization.mk z)) ↔
    HomogeneousLocalization.mk z ∈ ProjIsoSpecTopComponent.ToSpec.carrier x
-- Mathlib/Algebra/Order/SuccPred.lean
theorem IsSuccPrelimit.add_one_lt [Add α] [One α] [SuccAddOrder α]
    (hx : IsSuccPrelimit x) (hy : y < x) : y + 1 < x

Proof state:
α : Type u_1
x y : α
inst✝³ : PartialOrder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
hx : IsSuccPrelimit x
hy : y < x
⊢ y + 1 < x

Tactic:
rw [← succ_eq_add_one]

Result:
α : Type u_1
x y : α
inst✝³ : PartialOrder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
hx : IsSuccPrelimit x
hy : y < x
⊢ succ y < x

Proof state:
α : Type u_1
x y : α
inst✝³ : PartialOrder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
hx : IsSuccPrelimit x
hy : y < x
⊢ succ y < x

Tactic:
exact hx.succ_lt hy

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/ConcreteCategory.lean
lemma ShortExact.injective_f [HasZeroObject C] (hS : S.ShortExact) :
    Function.Injective ((forget₂ C Ab).map S.f)

Proof state:
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : HasZeroObject C
hS : S.ShortExact
⊢ Function.Injective ⇑(ConcreteCategory.hom ((forget₂ C Ab).map S.f))

Tactic:
rw [← Preadditive.mono_iff_injective]

Result:
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : HasZeroObject C
hS : S.ShortExact
⊢ Mono S.f

Proof state:
C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : HasZeroObject C
hS : S.ShortExact
⊢ Mono S.f

Tactic:
exact hS.mono_f

Result:
no goals
-- Mathlib/NumberTheory/ClassNumber/Finite.lean
theorem prod_finsetApprox_ne_zero : algebraMap R S (∏ m ∈ finsetApprox bS adm, m) ≠ 0

Proof state:
case intro
R : Type u_1
S : Type u_2
inst✝⁷ : EuclideanDomain R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
hx : 0 ∈ finsetApprox bS adm
⊢ False

Tactic:
exact finsetApprox.zero_not_mem bS adm hx

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝⁷ : EuclideanDomain R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
⊢ (algebraMap R S) (∏ m ∈ finsetApprox bS adm, m) ≠ 0

Tactic:
refine mt ((injective_iff_map_eq_zero _).mp bS.algebraMap_injective _) ?_

Result:
R : Type u_1
S : Type u_2
inst✝⁷ : EuclideanDomain R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
⊢ ¬∏ m ∈ finsetApprox bS adm, m = 0

Proof state:
R : Type u_1
S : Type u_2
inst✝⁷ : EuclideanDomain R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
⊢ ∀ (x : R), ¬(x ∈ finsetApprox bS adm ∧ x = 0)

Tactic:
rintro x ⟨hx, rfl⟩

Result:
case intro
R : Type u_1
S : Type u_2
inst✝⁷ : EuclideanDomain R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
hx : 0 ∈ finsetApprox bS adm
⊢ False

Proof state:
R : Type u_1
S : Type u_2
inst✝⁷ : EuclideanDomain R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
⊢ ¬∏ m ∈ finsetApprox bS adm, m = 0

Tactic:
simp only [Finset.prod_eq_zero_iff, not_exists]

Result:
R : Type u_1
S : Type u_2
inst✝⁷ : EuclideanDomain R
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
⊢ ∀ (x : R), ¬(x ∈ finsetApprox bS adm ∧ x = 0)
-- Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
theorem convexHull_subset_space (hs : s ∈ K.faces) : convexHull 𝕜 ↑s ⊆ K.space

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
hs : s ∈ K.faces
⊢ (convexHull 𝕜) ↑s ⊆ K.space

Tactic:
convert subset_biUnion_of_mem hs

Result:
case h.e'_3
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
hs : s ∈ K.faces
⊢ (convexHull 𝕜) ↑s = (convexHull 𝕜) ↑s

Proof state:
case h.e'_3
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
hs : s ∈ K.faces
⊢ (convexHull 𝕜) ↑s = (convexHull 𝕜) ↑s

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Analytic/Inverse.lean
theorem rightInv_coeff (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E)
    (n : ℕ) (hn : 2 ≤ n) :
    p.rightInv i x n =
      -(i.symm : F →L[𝕜] E).compContinuousMultilinearMap
          (∑ c ∈ ({c | 1 < Composition.length c}.toFinset : Finset (Composition n)),
            p.compAlongComposition (p.rightInv i x) c)

Proof state:
case e_f
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
n✝ n : ℕ
hn : 2 ≤ n + 2
⊢ p.comp (fun k => if k < n + 2 then p.rightInv i x k else 0) (n + 2) =
    ∑ c ∈ {c | 1 < c.length}.toFinset, p.compAlongComposition (p.rightInv i x) c

Tactic:
ext v

Result:
case e_f.H
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
n✝ n : ℕ
hn : 2 ≤ n + 2
v : Fin (n + 2) → F
⊢ (p.comp (fun k => if k < n + 2 then p.rightInv i x k else 0) (n + 2)) v =
    (∑ c ∈ {c | 1 < c.length}.toFinset, p.compAlongComposition (p.rightInv i x) c) v
-- Mathlib/Algebra/Polynomial/Div.lean
lemma add_modByMonic (p₁ p₂ : R[X]) : (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

Proof state:
case pos
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

Tactic:
rcases subsingleton_or_nontrivial R with hR | hR

Result:
case pos.inl
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
hR : Subsingleton R
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

case pos.inr
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

Proof state:
case neg
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : ¬q.Monic
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

Tactic:
simp_rw [modByMonic_eq_of_not_monic _ hq]

Result:
no goals

Proof state:
case pos.inl
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
hR : Subsingleton R
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

Tactic:
simp only [eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

Tactic:
by_cases hq : q.Monic

Result:
case pos
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

case neg
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : ¬q.Monic
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

Proof state:
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ p₁ %ₘ q + p₂ %ₘ q + q * (p₁ /ₘ q + p₂ /ₘ q) = p₁ + p₂

Tactic:
rw [mul_add, add_left_comm, add_assoc, modByMonic_add_div _ hq, ← add_assoc,
  add_comm (q * _), modByMonic_add_div _ hq]

Result:
no goals

Proof state:
case pos.inr
R : Type u
inst✝ : CommRing R
q p₁ p₂ : R[X]
hq : q.Monic
hR : Nontrivial R
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

Tactic:
exact
(div_modByMonic_unique (p₁ /ₘ q + p₂ /ₘ q) _ hq
    ⟨by
      rw [mul_add, add_left_comm, add_assoc, modByMonic_add_div _ hq, ← add_assoc,
        add_comm (q * _), modByMonic_add_div _ hq],
      (degree_add_le _ _).trans_lt
        (max_lt (degree_modByMonic_lt _ hq) (degree_modByMonic_lt _ hq))⟩).2

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem subtypeEquiv_refl {p : α → Prop} (h : ∀ a, p a ↔ p (Equiv.refl _ a) := fun _ => Iff.rfl) :
    (Equiv.refl α).subtypeEquiv h = Equiv.refl { a : α // p a }

Proof state:
case H.a
α : Sort u_1
p : α → Prop
h : optParam (∀ (a : α), p a ↔ p ((Equiv.refl α) a)) ⋯
x✝ : { a // p a }
⊢ ↑(((Equiv.refl α).subtypeEquiv h) x✝) = ↑((Equiv.refl { a // p a }) x✝)

Tactic:
rfl

Result:
no goals

Proof state:
α : Sort u_1
p : α → Prop
h : optParam (∀ (a : α), p a ↔ p ((Equiv.refl α) a)) ⋯
⊢ (Equiv.refl α).subtypeEquiv h = Equiv.refl { a // p a }

Tactic:
ext

Result:
case H.a
α : Sort u_1
p : α → Prop
h : optParam (∀ (a : α), p a ↔ p ((Equiv.refl α) a)) ⋯
x✝ : { a // p a }
⊢ ↑(((Equiv.refl α).subtypeEquiv h) x✝) = ↑((Equiv.refl { a // p a }) x✝)
-- Mathlib/Data/Nat/Log.lean
theorem log_le_clog (b n : ℕ) : log b n ≤ clog b n

Proof state:
case inl
b n : ℕ
hb : b ≤ 1
⊢ 0 ≤ clog b n

Tactic:
exact zero_le _

Result:
no goals

Proof state:
case inl
b n : ℕ
hb : b ≤ 1
⊢ log b n ≤ clog b n

Tactic:
rw [log_of_left_le_one hb]

Result:
case inl
b n : ℕ
hb : b ≤ 1
⊢ 0 ≤ clog b n

Proof state:
case inr
b n : ℕ
hb : 1 < b
⊢ log b n ≤ clog b n

Tactic:
cases n with
| zero =>
  rw [log_zero_right]
  exact zero_le _
| succ n =>
  exact (Nat.pow_le_pow_iff_right hb).1
    ((pow_log_le_self b n.succ_ne_zero).trans <| le_pow_clog hb _)

Result:
no goals

Proof state:
b n : ℕ
⊢ log b n ≤ clog b n

Tactic:
obtain hb | hb := le_or_lt b 1

Result:
case inl
b n : ℕ
hb : b ≤ 1
⊢ log b n ≤ clog b n

case inr
b n : ℕ
hb : 1 < b
⊢ log b n ≤ clog b n

Proof state:
case inr.zero
b : ℕ
hb : 1 < b
⊢ log b 0 ≤ clog b 0

Tactic:
rw [log_zero_right]

Result:
case inr.zero
b : ℕ
hb : 1 < b
⊢ 0 ≤ clog b 0

Proof state:
case inr.zero
b : ℕ
hb : 1 < b
⊢ 0 ≤ clog b 0

Tactic:
exact zero_le _

Result:
no goals

Proof state:
case inr.succ
b : ℕ
hb : 1 < b
n : ℕ
⊢ log b (n + 1) ≤ clog b (n + 1)

Tactic:
exact (Nat.pow_le_pow_iff_right hb).1
  ((pow_log_le_self b n.succ_ne_zero).trans <| le_pow_clog hb _)

Result:
no goals
-- Mathlib/Algebra/Group/Invertible/Basic.lean
theorem Commute.invOf_left [Monoid α] {a b : α} [Invertible b] (h : Commute b a) :
    Commute (⅟ b) a :=
  calc
    ⅟ b * a = ⅟ b * (a * b * ⅟ b)

Proof state:
α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible b
h : Commute b a
⊢ ⅟b * (a * b * ⅟b) = ⅟b * (b * a * ⅟b)

Tactic:
rw [h.eq]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible b
h : Commute b a
⊢ ⅟b * a = ⅟b * (a * b * ⅟b)

Tactic:
simp [mul_assoc]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : Monoid α
a b : α
inst✝ : Invertible b
h : Commute b a
⊢ ⅟b * (b * a * ⅟b) = a * ⅟b

Tactic:
simp [mul_assoc]

Result:
no goals
-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem has_antideriv_at_fourier_neg (hT : Fact (0 < T)) {n : ℤ} (hn : n ≠ 0) (x : ℝ) :
    HasDerivAt (fun y : ℝ => (T : ℂ) / (-2 * π * I * n) * fourier (-n) (y : AddCircle T))
      (fourier (-n) (x : AddCircle T)) x

Proof state:
case h.e'_8.h
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x y : ℝ
⊢ ↑T / (-2 * ↑π * I * ↑n) * (fourier (-n)) ↑y = (fourier (-n)) ↑y / (-2 * ↑π * I * ↑n / ↑T)

Tactic:
rw [div_div_eq_mul_div]

Result:
case h.e'_8.h
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x y : ℝ
⊢ ↑T / (-2 * ↑π * I * ↑n) * (fourier (-n)) ↑y = (fourier (-n)) ↑y * ↑T / (-2 * ↑π * I * ↑n)

Proof state:
case h.e'_8
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x : ℝ
⊢ (fun y => ↑T / (-2 * ↑π * I * ↑n) * (fourier (-n)) ↑y) = fun x => (fourier (-n)) ↑x / (-2 * ↑π * I * ↑n / ↑T)

Tactic:
ext1 y

Result:
case h.e'_8.h
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x y : ℝ
⊢ ↑T / (-2 * ↑π * I * ↑n) * (fourier (-n)) ↑y = (fourier (-n)) ↑y / (-2 * ↑π * I * ↑n / ↑T)

Proof state:
case h.e'_8.h
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x y : ℝ
⊢ ↑T / (-2 * ↑π * I * ↑n) * (fourier (-n)) ↑y = (fourier (-n)) ↑y * ↑T / (-2 * ↑π * I * ↑n)

Tactic:
ring

Result:
no goals

Proof state:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x : ℝ
⊢ HasDerivAt (fun y => ↑T / (-2 * ↑π * I * ↑n) * (fourier (-n)) ↑y) ((fourier (-n)) ↑x) x

Tactic:
convert (hasDerivAt_fourier_neg T n x).div_const (-2 * π * I * n / T) using 1

Result:
case h.e'_8
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x : ℝ
⊢ (fun y => ↑T / (-2 * ↑π * I * ↑n) * (fourier (-n)) ↑y) = fun x => (fourier (-n)) ↑x / (-2 * ↑π * I * ↑n / ↑T)

case h.e'_9
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x : ℝ
⊢ (fourier (-n)) ↑x = -2 * ↑π * I * ↑n / ↑T * (fourier (-n)) ↑x / (-2 * ↑π * I * ↑n / ↑T)

Proof state:
case h.e'_9
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : n ≠ 0
x : ℝ
⊢ (fourier (-n)) ↑x = -2 * ↑π * I * ↑n / ↑T * (fourier (-n)) ↑x / (-2 * ↑π * I * ↑n / ↑T)

Tactic:
simp [mul_div_cancel_left₀, hn, (Fact.out : 0 < T).ne', Real.pi_pos.ne']

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem le_comap_pow (n : ℕ) : K.comap f ^ n ≤ (K ^ n).comap f

Proof state:
case zero
R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
⊢ ⊤ ≤ comap f ⊤

Tactic:
exact rfl.le

Result:
no goals

Proof state:
case succ
R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
n : ℕ
n_ih : comap f K ^ n ≤ comap f (K ^ n)
⊢ comap f K ^ (n + 1) ≤ comap f (K ^ (n + 1))

Tactic:
rw [pow_succ, pow_succ]

Result:
case succ
R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
n : ℕ
n_ih : comap f K ^ n ≤ comap f (K ^ n)
⊢ comap f K ^ n * comap f K ≤ comap f (K ^ n * K)

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
n : ℕ
⊢ comap f K ^ n ≤ comap f (K ^ n)

Tactic:
induction' n with n n_ih

Result:
case zero
R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
⊢ comap f K ^ 0 ≤ comap f (K ^ 0)

case succ
R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
n : ℕ
n_ih : comap f K ^ n ≤ comap f (K ^ n)
⊢ comap f K ^ (n + 1) ≤ comap f (K ^ (n + 1))

Proof state:
case succ
R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
n : ℕ
n_ih : comap f K ^ n ≤ comap f (K ^ n)
⊢ comap f K ^ n * comap f K ≤ comap f (K ^ n * K)

Tactic:
exact (Ideal.mul_mono_left n_ih).trans (Ideal.le_comap_mul f)

Result:
no goals

Proof state:
case zero
R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
⊢ comap f K ^ 0 ≤ comap f (K ^ 0)

Tactic:
rw [pow_zero, pow_zero, Ideal.one_eq_top, Ideal.one_eq_top]

Result:
case zero
R : Type u
S : Type v
F : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
⊢ ⊤ ≤ comap f ⊤
-- Mathlib/Order/Fin/Basic.lean
theorem cast_top {m n : ℕ} [NeZero m] [NeZero n] (h : m = n) : (⊤ : Fin m).cast h = ⊤

Proof state:
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h : m = n
⊢ Fin.cast h ⊤ = ⊤

Tactic:
simp [← val_inj, h]

Result:
no goals
-- Mathlib/CategoryTheory/Galois/Decomposition.lean
/-- The trivial case if `X` is connected. -/
private lemma has_decomp_connected_components_aux_conn (X : C) [IsConnected X] :
    ∃ (ι : Type) (f : ι → C) (g : (i : ι) → (f i) ⟶ X) (_ : IsColimit (Cofan.mk X g)),
    (∀ i, IsConnected (f i)) ∧ Finite ι

Proof state:
C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
X : C
inst✝ : IsConnected X
⊢ ∃ ι f g x, (∀ (i : ι), IsConnected (f i)) ∧ Finite ι

Tactic:
refine ⟨Unit, fun _ ↦ X, fun _ ↦ 𝟙 X, mkCofanColimit _ (fun s ↦ s.inj ()), ?_⟩

Result:
C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
X : C
inst✝ : IsConnected X
⊢ (∀ (i : Unit), IsConnected ((fun x => X) i)) ∧ Finite Unit

Proof state:
C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
X : C
inst✝ : IsConnected X
⊢ (∀ (i : Unit), IsConnected ((fun x => X) i)) ∧ Finite Unit

Tactic:
exact ⟨fun _ ↦ inferInstance, inferInstance⟩

Result:
no goals
-- Mathlib/GroupTheory/NoncommPiCoprod.lean
theorem noncommPiCoprod_apply (comm) (u : (i : ι) → H i) :
    Subgroup.noncommPiCoprod comm u = Finset.noncommProd Finset.univ (fun i ↦ u i)
      (fun i _ j _ h ↦ comm h _ _ (u i).prop (u j).prop)

Proof state:
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
inst✝ : Fintype ι
comm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
u : (i : ι) → ↥(H i)
⊢ (noncommPiCoprod comm) u = Finset.univ.noncommProd (fun i => ↑(u i)) ⋯

Tactic:
simp only [Subgroup.noncommPiCoprod, MonoidHom.noncommPiCoprod,
  coe_subtype, MonoidHom.coe_mk, OneHom.coe_mk]

Result:
no goals
-- Mathlib/Geometry/Manifold/ChartedSpace.lean
lemma ChartedSpace.sum_chartAt_inl (x : M) :
    haveI : Nonempty H := nonempty_of_chartedSpace x
    chartAt H (Sum.inl x)
      = (chartAt H x).lift_openEmbedding (X' := M ⊕ M') IsOpenEmbedding.inl

Proof state:
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
x : M
⊢ ChartedSpace.chartAt (Sum.inl x) = (ChartedSpace.chartAt x).lift_openEmbedding ⋯

Tactic:
rfl

Result:
no goals

Proof state:
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
x : M
⊢ chartAt H (Sum.inl x) = (chartAt H x).lift_openEmbedding ⋯

Tactic:
simp only [chartAt, sum, nonempty_of_chartedSpace x, ↓reduceDIte]

Result:
H : Type u
M : Type u_2
M' : Type u_3
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace M'
cm : ChartedSpace H M
cm' : ChartedSpace H M'
x : M
⊢ ChartedSpace.chartAt (Sum.inl x) = (ChartedSpace.chartAt x).lift_openEmbedding ⋯
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem toListModel_alter [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α]
    {m : Raw₀ α (fun _ => β)} (h : Raw.WFImp m.1) {a : α} {f : Option β → Option β} :
    Perm (toListModel (Const.alter m a f).1.2) (Const.alterKey a f (toListModel m.1.2))

Proof state:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : EquivBEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : Raw.WFImp m.val
a : α
f : Option β → Option β
⊢ toListModel (alterₘ m a f).val.buckets ~ Const.alterKey a f (toListModel m.val.buckets)

Tactic:
exact toListModel_alterₘ h

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : EquivBEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : Raw.WFImp m.val
a : α
f : Option β → Option β
⊢ toListModel (alter m a f).val.buckets ~ Const.alterKey a f (toListModel m.val.buckets)

Tactic:
rw [alter_eq_alterₘ]

Result:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : EquivBEq α
inst✝¹ : Hashable α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : Raw.WFImp m.val
a : α
f : Option β → Option β
⊢ toListModel (alterₘ m a f).val.buckets ~ Const.alterKey a f (toListModel m.val.buckets)
-- Mathlib/Order/Filter/Bases.lean
theorem mem_filter_iff (h : IsBasis p s) {U : Set α} :
    U ∈ h.filter ↔ ∃ i, p i ∧ s i ⊆ U

Proof state:
α : Type u_1
ι : Sort u_4
p : ι → Prop
s : ι → Set α
h : IsBasis p s
U : Set α
⊢ U ∈ h.filter ↔ ∃ i, p i ∧ s i ⊆ U

Tactic:
simp only [IsBasis.filter, FilterBasis.mem_filter_iff, mem_filterBasis_iff,
  exists_exists_and_eq_and]

Result:
no goals