harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Prod/TProd.lean
theorem elim_mk : ∀ (l : List ι) (f : ∀ i, α i) {i : ι} (hi : i ∈ l), (TProd.mk l f).elim hi = f i
  | i :: is, f, j, hj => by
    by_cases hji : j = i
    · subst hji
      simp
    · rw [TProd.elim_of_ne _ hji, snd_mk, elim_mk is]

Proof state:
case pos
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ j :: is
⊢ (TProd.mk (j :: is) f).elim hj = f j

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
⊢ (TProd.mk (i :: is) f).elim hj = f j

Tactic:
by_cases hji : j = i

Result:
case pos
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
hji : j = i
⊢ (TProd.mk (i :: is) f).elim hj = f j

case neg
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
hji : ¬j = i
⊢ (TProd.mk (i :: is) f).elim hj = f j

Proof state:
case neg
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
hji : ¬j = i
⊢ (TProd.mk (i :: is) f).elim hj = f j

Tactic:
rw [TProd.elim_of_ne _ hji, snd_mk, elim_mk is]

Result:
no goals

Proof state:
case pos
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
hji : j = i
⊢ (TProd.mk (i :: is) f).elim hj = f j

Tactic:
subst hji

Result:
case pos
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ j :: is
⊢ (TProd.mk (j :: is) f).elim hj = f j
-- Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean
/-- `γ` is an integral curve for `v` at `t₀` iff `γ` is an integral curve on some interval
containing `t₀`. -/
lemma isIntegralCurveAt_iff' :
    IsIntegralCurveAt γ v t₀ ↔ ∃ ε > 0, IsIntegralCurveOn γ v (Metric.ball t₀ ε)

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
⊢ IsIntegralCurveAt γ v t₀ ↔ ∃ ε > 0, IsIntegralCurveOn γ v (Metric.ball t₀ ε)

Tactic:
simp_rw [IsIntegralCurveOn, ← Metric.eventually_nhds_iff_ball, IsIntegralCurveAt]

Result:
no goals
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem Step.append_left : ∀ {L₁ L₂ L₃ : List (α × Bool)}, Step L₂ L₃ → Step (L₁ ++ L₂) (L₁ ++ L₃)
  | _, _, _, Red.Step.not => by rw [← List.append_assoc, ← List.append_assoc]; constructor

Proof state:
α : Type u
x✝¹ L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ Step (x✝¹ ++ L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝) (x✝¹ ++ L₁✝ ++ L₂✝)

Tactic:
constructor

Result:
no goals

Proof state:
α : Type u
x✝¹ L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ Step (x✝¹ ++ (L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝)) (x✝¹ ++ (L₁✝ ++ L₂✝))

Tactic:
rw [← List.append_assoc, ← List.append_assoc]

Result:
α : Type u
x✝¹ L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ Step (x✝¹ ++ L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝) (x✝¹ ++ L₁✝ ++ L₂✝)
-- Mathlib/GroupTheory/OreLocalization/Basic.lean
theorem mul_cancel' {r₁ r₂ : R} {s t : S} :
    ((r₁ * s) /ₒ t) * (r₂ /ₒ s) = (r₁ * r₂) /ₒ t

Proof state:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s t : ↥S
⊢ ↑1 * (r₁ * ↑s) = r₁ * ↑s

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s t : ↥S
⊢ r₁ * ↑s /ₒ t * (r₂ /ₒ s) = r₁ * r₂ /ₒ t

Tactic:
simp [oreDiv_mul_char (r₁ * s) r₂ t s r₁ 1 (by simp)]

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
theorem algebraicIndependent_empty_type [IsEmpty ι] [Nontrivial A] : AlgebraicIndependent K x

Proof state:
ι : Type u_1
K : Type u_4
A : Type u_5
x : ι → A
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra K A
inst✝¹ : IsEmpty ι
inst✝ : Nontrivial A
⊢ Injective ⇑(algebraMap K A)

Tactic:
exact RingHom.injective _

Result:
no goals

Proof state:
ι : Type u_1
K : Type u_4
A : Type u_5
x : ι → A
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra K A
inst✝¹ : IsEmpty ι
inst✝ : Nontrivial A
⊢ AlgebraicIndependent K x

Tactic:
rw [algebraicIndependent_empty_type_iff]

Result:
ι : Type u_1
K : Type u_4
A : Type u_5
x : ι → A
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra K A
inst✝¹ : IsEmpty ι
inst✝ : Nontrivial A
⊢ Injective ⇑(algebraMap K A)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_alter_eq_self_of_mem (h : m.1.WF) {k : α} {f : Option β → Option β}
    (h₁ : m.contains k) (h₂ : (f (Const.get? m k)).isSome) :
    (Const.alter m k f).1.size = m.1.size

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
k : α
f : Option β → Option β
h₁ : m.contains k = true
h₂ : (f (get? m k)).isSome = true
⊢ (alter m k f).val.size = m.val.size

Tactic:
simp [size_alter, h, h₁, Option.isSome_iff_ne_none.mp h₂]

Result:
no goals
-- Mathlib/Data/List/MinMax.lean
lemma maximum_append (l₁ l₂ : List α) : (l₁ ++ l₂).maximum = max l₁.maximum l₂.maximum

Proof state:
case cons
α : Type u_1
inst✝ : LinearOrder α
l₂ : List α
head✝ : α
tail✝ : List α
ih : (tail✝ ++ l₂).maximum = tail✝.maximum ⊔ l₂.maximum
⊢ (head✝ :: tail✝ ++ l₂).maximum = (head✝ :: tail✝).maximum ⊔ l₂.maximum

Tactic:
rw [maximum_cons, cons_append, maximum_cons, ih, ← max_assoc]

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : LinearOrder α
l₂ : List α
⊢ ([] ++ l₂).maximum = [].maximum ⊔ l₂.maximum

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
l₁ l₂ : List α
⊢ (l₁ ++ l₂).maximum = l₁.maximum ⊔ l₂.maximum

Tactic:
induction l₁ with
| nil => simp
| cons _ _ ih => rw [maximum_cons, cons_append, maximum_cons, ih, ← max_assoc]

Result:
no goals
-- Mathlib/Data/Finset/Density.lean
@[simp] lemma dens_le_one : s.dens ≤ 1

Proof state:
case inl
α : Type u_2
inst✝ : Fintype α
s : Finset α
h✝ : IsEmpty α
⊢ s.dens ≤ 1

Tactic:
simp [Subsingleton.elim s ∅]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Fintype α
s : Finset α
⊢ s.dens ≤ 1

Tactic:
cases isEmpty_or_nonempty α

Result:
case inl
α : Type u_2
inst✝ : Fintype α
s : Finset α
h✝ : IsEmpty α
⊢ s.dens ≤ 1

case inr
α : Type u_2
inst✝ : Fintype α
s : Finset α
h✝ : Nonempty α
⊢ s.dens ≤ 1

Proof state:
case inr
α : Type u_2
inst✝ : Fintype α
s : Finset α
h✝ : Nonempty α
⊢ s.dens ≤ 1

Tactic:
simpa using dens_le_dens s.subset_univ

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem isClosed_sInter {s : Set (Set X)} : (∀ t ∈ s, IsClosed t) → IsClosed (⋂₀ s)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set (Set X)
⊢ (∀ t ∈ s, IsClosed t) → IsClosed (⋂₀ s)

Tactic:
simpa only [← isOpen_compl_iff, compl_sInter, sUnion_image] using isOpen_biUnion

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem normSq_to_real {x : ℝ} : normSq x = x * x

Proof state:
x : ℝ
⊢ normSq x = x * x

Tactic:
simp [RCLike.normSq]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem kernel_map_comp_kernelSubobjectIso_inv (sq : Arrow.mk f ⟶ Arrow.mk f') :
    kernel.map f f' sq.1 sq.2 sq.3.symm ≫ (kernelSubobjectIso _).inv =
      (kernelSubobjectIso _).inv ≫ kernelSubobjectMap sq

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : HasZeroMorphisms C
f : X ⟶ Y
inst✝¹ : HasKernel f
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasKernel f'
sq : Arrow.mk f ⟶ Arrow.mk f'
⊢ kernel.map f f' sq.left sq.right ⋯ ≫ (kernelSubobjectIso f').inv = (kernelSubobjectIso f).inv ≫ kernelSubobjectMap sq

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem norm_iteratedFDerivWithin_zero : ‖iteratedFDerivWithin 𝕜 0 f s x‖ = ‖f x‖

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
⊢ ‖iteratedFDerivWithin 𝕜 0 f s x‖ = ‖f x‖

Tactic:
rw [iteratedFDerivWithin_zero_eq_comp, comp_apply, LinearIsometryEquiv.norm_map]

Result:
no goals
-- Mathlib/Algebra/Quandle.lean
theorem dihedralAct.inv (n : ℕ) (a : ZMod n) : Function.Involutive (dihedralAct n a)

Proof state:
n : ℕ
a b : ZMod n
⊢ dihedralAct n a (dihedralAct n a b) = b

Tactic:
dsimp only [dihedralAct]

Result:
n : ℕ
a b : ZMod n
⊢ 2 * a - (2 * a - b) = b

Proof state:
n : ℕ
a : ZMod n
⊢ Function.Involutive (dihedralAct n a)

Tactic:
intro b

Result:
n : ℕ
a b : ZMod n
⊢ dihedralAct n a (dihedralAct n a b) = b

Proof state:
n : ℕ
a b : ZMod n
⊢ 2 * a - (2 * a - b) = b

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma le_add_of_forall_gt {a b c : EReal} (h₁ : a ≠ ⊥ ∨ b ≠ ⊤) (h₂ : a ≠ ⊤ ∨ b ≠ ⊥)
    (h : ∀ a' > a, ∀ b' > b, c ≤ a' + b') : c ≤ a + b

Proof state:
a b c : EReal
h₁ : a ≠ ⊥ ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ ⊥
h : ∀ a' > a, ∀ b' > b, c ≤ a' + b'
a' : EReal
ha' : a' < -a
b' : EReal
hb' : b' < -b
⊢ c ≤ -(a' + b')

Tactic:
rw [neg_add (.inr hb'.ne_top) (.inl ha'.ne_top)]

Result:
a b c : EReal
h₁ : a ≠ ⊥ ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ ⊥
h : ∀ a' > a, ∀ b' > b, c ≤ a' + b'
a' : EReal
ha' : a' < -a
b' : EReal
hb' : b' < -b
⊢ c ≤ -a' - b'

Proof state:
a b c : EReal
h₁ : a ≠ ⊥ ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ ⊥
h : ∀ a' > a, ∀ b' > b, c ≤ a' + b'
⊢ -a - b ≤ -c

Tactic:
refine add_le_of_forall_lt fun a' ha' b' hb' ↦ EReal.le_neg_of_le_neg ?_

Result:
a b c : EReal
h₁ : a ≠ ⊥ ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ ⊥
h : ∀ a' > a, ∀ b' > b, c ≤ a' + b'
a' : EReal
ha' : a' < -a
b' : EReal
hb' : b' < -b
⊢ c ≤ -(a' + b')

Proof state:
a b c : EReal
h₁ : a ≠ ⊥ ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ ⊥
h : ∀ a' > a, ∀ b' > b, c ≤ a' + b'
⊢ c ≤ a + b

Tactic:
rw [← neg_le_neg_iff, neg_add h₁ h₂]

Result:
a b c : EReal
h₁ : a ≠ ⊥ ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ ⊥
h : ∀ a' > a, ∀ b' > b, c ≤ a' + b'
⊢ -a - b ≤ -c

Proof state:
a b c : EReal
h₁ : a ≠ ⊥ ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ ⊥
h : ∀ a' > a, ∀ b' > b, c ≤ a' + b'
a' : EReal
ha' : a' < -a
b' : EReal
hb' : b' < -b
⊢ c ≤ -a' - b'

Tactic:
exact h _ (EReal.lt_neg_of_lt_neg ha') _ (EReal.lt_neg_of_lt_neg hb')

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem id_whiskerLeft_symm {f g : a ⟶ b} (η : f ⟶ g) : η = (λ_ f).inv ≫ 𝟙 a ◁ η ≫ (λ_ g).hom

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η : f ⟶ g
⊢ η = (λ_ f).inv ≫ 𝟙 a ◁ η ≫ (λ_ g).hom

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_congr_Prop {p q : Prop} {f : p → M} {g : q → M} (hpq : p = q)
    (hfg : ∀ h : q, f (hpq.mpr h) = g h) : finprod f = finprod g

Proof state:
M : Type u_2
inst✝ : CommMonoid M
p : Prop
f g : p → M
hfg : ∀ (h : p), f ⋯ = g h
⊢ finprod f = finprod g

Tactic:
exact finprod_congr hfg

Result:
no goals

Proof state:
M : Type u_2
inst✝ : CommMonoid M
p q : Prop
f : p → M
g : q → M
hpq : p = q
hfg : ∀ (h : q), f ⋯ = g h
⊢ finprod f = finprod g

Tactic:
subst q

Result:
M : Type u_2
inst✝ : CommMonoid M
p : Prop
f g : p → M
hfg : ∀ (h : p), f ⋯ = g h
⊢ finprod f = finprod g
-- Mathlib/Algebra/Category/Grp/Limits.lean
theorem kernelIsoKer_inv_comp_ι {G H : AddCommGrp.{u}} (f : G ⟶ H) :
    (kernelIsoKer f).inv ≫ kernel.ι f = ofHom (AddSubgroup.subtype f.hom.ker)

Proof state:
G H : AddCommGrp
f : G ⟶ H
⊢ (kernelIsoKer f).inv ≫ kernel.ι f = ofHom (Hom.hom f).ker.subtype

Tactic:
ext

Result:
case hf.h
G H : AddCommGrp
f : G ⟶ H
x✝ : ↑(of ↥(Hom.hom f).ker)
⊢ (Hom.hom ((kernelIsoKer f).inv ≫ kernel.ι f)) x✝ = (Hom.hom (ofHom (Hom.hom f).ker.subtype)) x✝

Proof state:
case hf.h
G H : AddCommGrp
f : G ⟶ H
x✝ : ↑(of ↥(Hom.hom f).ker)
⊢ (Hom.hom ((kernelIsoKer f).inv ≫ kernel.ι f)) x✝ = (Hom.hom (ofHom (Hom.hom f).ker.subtype)) x✝

Tactic:
simp [kernelIsoKer]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cosh_conj : cosh (conj x) = conj (cosh x)

Proof state:
x : ℂ
⊢ cosh ((starRingEnd ℂ) x) = (starRingEnd ℂ) (cosh x)

Tactic:
rw [cosh, ← RingHom.map_neg, exp_conj, exp_conj, ← RingHom.map_add, cosh, map_div₀]

Result:
x : ℂ
⊢ (starRingEnd ℂ) (cexp x + cexp (-x)) / 2 = (starRingEnd ℂ) (cexp x + cexp (-x)) / (starRingEnd ℂ) 2

Proof state:
x : ℂ
⊢ (starRingEnd ℂ) (cexp x + cexp (-x)) / 2 = (starRingEnd ℂ) (cexp x + cexp (-x)) / (starRingEnd ℂ) 2

Tactic:
simp [← one_add_one_eq_two]

Result:
no goals
-- Mathlib/Probability/Distributions/Uniform.lean
theorem absolutelyContinuous {X : Ω → E} {s : Set E} (hu : IsUniform X s ℙ μ) : map X ℙ ≪ μ

Proof state:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hu : IsUniform X s ℙ μ
⊢ Measure.map X ℙ ≪ μ

Tactic:
rw [hu]

Result:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hu : IsUniform X s ℙ μ
⊢ ProbabilityTheory.cond μ s ≪ μ

Proof state:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hu : IsUniform X s ℙ μ
⊢ ProbabilityTheory.cond μ s ≪ μ

Tactic:
exact ProbabilityTheory.cond_absolutelyContinuous

Result:
no goals
-- Mathlib/Computability/Halting.lean
theorem comp' {n m f g} (hf : @Partrec' m f) (hg : @Vec n m g) : Partrec' fun v => f (g v) :=
  (hf.comp _ hg).of_eq fun v => by simp

Proof state:
n m : ℕ
f : List.Vector ℕ m →. ℕ
g : List.Vector ℕ n → List.Vector ℕ m
hf : Partrec' f
hg : Vec g
v : List.Vector ℕ n
⊢ (mOfFn fun i => ↑(some ((g v).get i))) >>= f = f (g v)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Field/Rat.lean
lemma div_def (p q : ℚ≥0) : p / q = divNat (p.num * q.den) (p.den * q.num)

Proof state:
p q : ℚ≥0
⊢ p / q = divNat (p.num * q.den) (p.den * q.num)

Tactic:
ext

Result:
case a
p q : ℚ≥0
⊢ ↑(p / q) = ↑(divNat (p.num * q.den) (p.den * q.num))

Proof state:
case a
p q : ℚ≥0
⊢ ↑(p / q) = ↑(divNat (p.num * q.den) (p.den * q.num))

Tactic:
simp [Rat.div_def', num_coe, den_coe]

Result:
no goals
-- Mathlib/RingTheory/Localization/Defs.lean
theorem sec_spec' (z : S) :
    algebraMap R S (IsLocalization.sec M z).1 = algebraMap R S (IsLocalization.sec M z).2 * z

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
z : S
⊢ (algebraMap R S) (sec M z).1 = (algebraMap R S) ↑(sec M z).2 * z

Tactic:
rw [mul_comm, sec_spec]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem compl_sInf (S : Set (UpperSet α)) : (sInf S).compl = ⨅ s ∈ S, UpperSet.compl s :=
  LowerSet.ext <| by simp only [coe_compl, coe_sInf, compl_iUnion₂, LowerSet.coe_iInf₂]

Proof state:
α : Type u_1
inst✝ : LE α
S : Set (UpperSet α)
⊢ ↑(sInf S).compl = ↑(⨅ s ∈ S, s.compl)

Tactic:
simp only [coe_compl, coe_sInf, compl_iUnion₂, LowerSet.coe_iInf₂]

Result:
no goals
-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem fourier_neg' {n : ℤ} {x : AddCircle T} : @toCircle T (-(n • x)) = conj (fourier n x)

Proof state:
T : ℝ
n : ℤ
x : AddCircle T
⊢ ↑(-(n • x)).toCircle = (starRingEnd ℂ) ((fourier n) x)

Tactic:
rw [← neg_smul, ← fourier_apply]

Result:
T : ℝ
n : ℤ
x : AddCircle T
⊢ (fourier (-n)) x = (starRingEnd ℂ) ((fourier n) x)

Proof state:
T : ℝ
n : ℤ
x : AddCircle T
⊢ (fourier (-n)) x = (starRingEnd ℂ) ((fourier n) x)

Tactic:
exact fourier_neg

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Split.lean
theorem splitUpper_eq_self : I.splitUpper i x = I ↔ x ≤ I.lower i

Proof state:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ I.splitUpper i x = ↑I ↔ x ≤ I.lower i

Tactic:
simp [splitUpper, update_eq_iff]

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/Basic.lean
theorem Topology.IsOpenEmbedding.isManifold_singleton {𝕜 E H : Type*}
    [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H]
    {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
    {M : Type*} [TopologicalSpace M] [Nonempty M] {f : M → H} (h : IsOpenEmbedding f) :
    @IsManifold 𝕜 _ E _ _ H _ I n M _ h.singletonChartedSpace :=
  (h.toPartialHomeomorph f).isManifold_singleton (by simp)

Proof state:
𝕜 : Type u_1
E : Type u_2
H : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
n : WithTop ℕ∞
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : Nonempty M
f : M → H
h : IsOpenEmbedding f
⊢ (toPartialHomeomorph f h).source = univ

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Arrow.lean
@[reassoc (attr := simp)]
lemma hom_inv_id_right (e : f ≅ g) : e.hom.right ≫ e.inv.right = 𝟙 _

Proof state:
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
⊢ e.hom.right ≫ e.inv.right = 𝟙 f.right

Tactic:
rw [← comp_right, e.hom_inv_id, id_right]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem iUnion_nonempty_self (s : Set α) : ⋃ _ : s.Nonempty, s = s

Proof state:
α : Type u_1
s : Set α
⊢ ⋃ (_ : s.Nonempty), s = s

Tactic:
rw [iUnion_nonempty_index, biUnion_self]

Result:
no goals
-- Mathlib/Analysis/Complex/AbsMax.lean
theorem norm_eventually_eq_of_isLocalMax {f : E → F} {c : E}
    (hd : ∀ᶠ z in 𝓝 c, DifferentiableAt ℂ f z) (hc : IsLocalMax (norm ∘ f) c) :
    ∀ᶠ y in 𝓝 c, ‖f y‖ = ‖f c‖

Proof state:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
c : E
hd : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMax (norm ∘ f) c
⊢ ∀ᶠ (y : E) in 𝓝 c, ‖f y‖ = ‖f c‖

Tactic:
rcases nhds_basis_closedBall.eventually_iff.1 (hd.and hc) with ⟨r, hr₀, hr⟩

Result:
case intro.intro
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
c : E
hd : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMax (norm ∘ f) c
r : ℝ
hr₀ : 0 < r
hr : ∀ ⦃x : E⦄, x ∈ closedBall c r → DifferentiableAt ℂ f x ∧ (norm ∘ f) x ≤ (norm ∘ f) c
⊢ ∀ᶠ (y : E) in 𝓝 c, ‖f y‖ = ‖f c‖

Proof state:
case intro.intro
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
c : E
hd : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMax (norm ∘ f) c
r : ℝ
hr₀ : 0 < r
hr : ∀ ⦃x : E⦄, x ∈ closedBall c r → DifferentiableAt ℂ f x ∧ (norm ∘ f) x ≤ (norm ∘ f) c
⊢ ∀ᶠ (y : E) in 𝓝 c, ‖f y‖ = ‖f c‖

Tactic:
exact nhds_basis_closedBall.eventually_iff.2
  ⟨r, hr₀, norm_eqOn_closedBall_of_isMaxOn (DifferentiableOn.diffContOnCl fun x hx =>
      (hr <| closure_ball_subset_closedBall hx).1.differentiableWithinAt) fun x hx =>
    (hr <| ball_subset_closedBall hx).2⟩

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem mapRange.addMonoidHom_comp (f : N →+ P) (f₂ : M →+ N) :
    (mapRange.addMonoidHom (f.comp f₂) : (α →₀ _) →+ _) =
      (mapRange.addMonoidHom f).comp (mapRange.addMonoidHom f₂) :=
  AddMonoidHom.ext <|
    mapRange_comp f (map_zero f) f₂ (map_zero f₂) (by simp only [comp_apply, map_zero])

Proof state:
α : Type u_1
M : Type u_5
N : Type u_7
P : Type u_8
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid P
f : N →+ P
f₂ : M →+ N
⊢ (⇑f ∘ ⇑f₂) 0 = 0

Tactic:
simp only [comp_apply, map_zero]

Result:
no goals
-- Mathlib/Order/Filter/Pointwise.lean
theorem zero_smul_filter (hg : g.NeBot) : (0 : α) • g = 0 :=
  zero_smul_filter_nonpos.antisymm <|
    le_map_iff.2 fun s hs => by
      simp_rw [zero_smul, (hg.nonempty_of_mem hs).image_const]
      exact zero_mem_zero

Proof state:
α : Type u_2
β : Type u_3
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
g : Filter β
hg : g.NeBot
s : Set β
hs : s ∈ g
⊢ (fun x => 0 • x) '' s ∈ 0

Tactic:
simp_rw [zero_smul, (hg.nonempty_of_mem hs).image_const]

Result:
α : Type u_2
β : Type u_3
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
g : Filter β
hg : g.NeBot
s : Set β
hs : s ∈ g
⊢ {0} ∈ 0

Proof state:
α : Type u_2
β : Type u_3
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
g : Filter β
hg : g.NeBot
s : Set β
hs : s ∈ g
⊢ {0} ∈ 0

Tactic:
exact zero_mem_zero

Result:
no goals
-- Mathlib/Condensed/Discrete/LocallyConstant.lean
lemma sigmaComparison_comp_sigmaIso [HasExplicitFiniteCoproducts.{u} P]
    (X : (CompHausLike.{u} P)ᵒᵖ ⥤ Type max u w) :
    (X.mapIso (sigmaIso r).op).hom ≫ sigmaComparison X (fun a ↦ (fiber r a).1) ≫
      (fun g ↦ g a) = X.map (sigmaIncl r a).op

Proof state:
case h
P : TopCat → Prop
inst✝¹ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
Q : CompHausLike P
Z : Type (max u w)
r : LocallyConstant (↑Q.toTop) Z
a : Fiber ⇑r
inst✝ : HasExplicitFiniteCoproducts P
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
a✝ : X.obj (op Q)
⊢ X.map ((sigmaIso r).hom.op ≫ (ofHom P { toFun := Sigma.mk a, continuous_toFun := ⋯ }).op) a✝ =
    X.map (sigmaIncl r a).op a✝

Tactic:
rfl

Result:
no goals

Proof state:
case h
P : TopCat → Prop
inst✝¹ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
Q : CompHausLike P
Z : Type (max u w)
r : LocallyConstant (↑Q.toTop) Z
a : Fiber ⇑r
inst✝ : HasExplicitFiniteCoproducts P
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
a✝ : X.obj (op Q)
⊢ ((X.mapIso (sigmaIso r).op).hom ≫ (sigmaComparison X fun a => ↑(fiber r a).toTop) ≫ fun g => g a) a✝ =
    X.map (sigmaIncl r a).op a✝

Tactic:
simp only [Functor.mapIso_hom, Iso.op_hom, types_comp_apply, sigmaComparison, coe_of,
  ← FunctorToTypes.map_comp_apply]

Result:
case h
P : TopCat → Prop
inst✝¹ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
Q : CompHausLike P
Z : Type (max u w)
r : LocallyConstant (↑Q.toTop) Z
a : Fiber ⇑r
inst✝ : HasExplicitFiniteCoproducts P
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
a✝ : X.obj (op Q)
⊢ X.map ((sigmaIso r).hom.op ≫ (ofHom P { toFun := Sigma.mk a, continuous_toFun := ⋯ }).op) a✝ =
    X.map (sigmaIncl r a).op a✝

Proof state:
P : TopCat → Prop
inst✝¹ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
Q : CompHausLike P
Z : Type (max u w)
r : LocallyConstant (↑Q.toTop) Z
a : Fiber ⇑r
inst✝ : HasExplicitFiniteCoproducts P
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
⊢ ((X.mapIso (sigmaIso r).op).hom ≫ (sigmaComparison X fun a => ↑(fiber r a).toTop) ≫ fun g => g a) =
    X.map (sigmaIncl r a).op

Tactic:
ext

Result:
case h
P : TopCat → Prop
inst✝¹ : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), HasProp P (Subtype p)
Q : CompHausLike P
Z : Type (max u w)
r : LocallyConstant (↑Q.toTop) Z
a : Fiber ⇑r
inst✝ : HasExplicitFiniteCoproducts P
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
a✝ : X.obj (op Q)
⊢ ((X.mapIso (sigmaIso r).op).hom ≫ (sigmaComparison X fun a => ↑(fiber r a).toTop) ≫ fun g => g a) a✝ =
    X.map (sigmaIncl r a).op a✝
-- Mathlib/Order/Filter/Basic.lean
lemma iSup_inf_principal (f : ι → Filter α) (s : Set α) : ⨆ i, f i ⊓ 𝓟 s = (⨆ i, f i) ⊓ 𝓟 s

Proof state:
α : Type u
ι : Sort x
f : ι → Filter α
s : Set α
⊢ ⨆ i, f i ⊓ 𝓟 s = (⨆ i, f i) ⊓ 𝓟 s

Tactic:
ext

Result:
case h
α : Type u
ι : Sort x
f : ι → Filter α
s s✝ : Set α
⊢ s✝ ∈ ⨆ i, f i ⊓ 𝓟 s ↔ s✝ ∈ (⨆ i, f i) ⊓ 𝓟 s

Proof state:
case h
α : Type u
ι : Sort x
f : ι → Filter α
s s✝ : Set α
⊢ s✝ ∈ ⨆ i, f i ⊓ 𝓟 s ↔ s✝ ∈ (⨆ i, f i) ⊓ 𝓟 s

Tactic:
simp only [mem_iSup, mem_inf_principal]

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
@[simp] lemma krullDim_of_noMaxOrder [Nonempty α] [NoMaxOrder α] : krullDim α = ⊤

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : Nonempty α
inst✝ : NoMaxOrder α
⊢ krullDim α = ⊤

Tactic:
simp [krullDim_eq_iSup_coheight, coheight_of_noMaxOrder]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Inverse.lean
theorem eq_inv_iff_mul_eq_one {φ ψ : MvPowerSeries σ k} (h : constantCoeff σ k ψ ≠ 0) :
    φ = ψ⁻¹ ↔ φ * ψ = 1

Proof state:
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : (constantCoeff σ k) ψ ≠ 0
⊢ φ = ψ⁻¹ ↔ φ * ψ = 1

Tactic:
rw [← MvPowerSeries.eq_mul_inv_iff_mul_eq h, one_mul]

Result:
no goals