harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Bounds/Basic.lean
theorem upperBounds_insert (a : α) (s : Set α) :
    upperBounds (insert a s) = Ici a ∩ upperBounds s

Proof state:
α : Type u
inst✝ : Preorder α
a : α
s : Set α
⊢ upperBounds (insert a s) = Ici a ∩ upperBounds s

Tactic:
rw [insert_eq, upperBounds_union, upperBounds_singleton]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Bicategory/PureCoherence.lean
theorem mk_eq_of_naturality {f g f' : a ⟶ b} {η θ : f ⟶ g} {η' θ' : f ≅ g}
    (η_f : 𝟙 a ≫ f ≅ f') (η_g : 𝟙 a ≫ g ≅ f')
    (Hη : η'.hom = η) (Hθ : θ'.hom = θ)
    (Hη' : whiskerLeftIso (𝟙 a) η' ≪≫ η_g = η_f)
    (Hθ' : whiskerLeftIso (𝟙 a) θ' ≪≫ η_g = η_f) : η = θ :=
  calc
    η = η'.hom := Hη.symm
    _ = (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f g f' : a ⟶ b
η θ : f ⟶ g
η' θ' : f ≅ g
η_f : 𝟙 a ≫ f ≅ f'
η_g : 𝟙 a ≫ g ≅ f'
Hη : η'.hom = η
Hθ : θ'.hom = θ
Hη' : 𝟙 a ◁ η' ≪≫ η_g = η_f
Hθ' : 𝟙 a ◁ θ' ≪≫ η_g = η_f
⊢ (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom = θ'.hom

Tactic:
simp [← reassoc_of% (congrArg Iso.hom Hθ')]

Result:
no goals

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f g f' : a ⟶ b
η θ : f ⟶ g
η' θ' : f ≅ g
η_f : 𝟙 a ≫ f ≅ f'
η_g : 𝟙 a ≫ g ≅ f'
Hη : η'.hom = η
Hθ : θ'.hom = θ
Hη' : 𝟙 a ◁ η' ≪≫ η_g = η_f
Hθ' : 𝟙 a ◁ θ' ≪≫ η_g = η_f
⊢ η'.hom = (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom

Tactic:
simp [← reassoc_of% (congrArg Iso.hom Hη')]

Result:
no goals
-- Mathlib/RingTheory/WittVector/InitTail.lean
theorem init_neg (x : 𝕎 R) (n : ℕ) : init n (-x) = init n (-init n x)

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
⊢ init n (-x) = init n (-init n x)

Tactic:
init_ring using wittNeg_vars

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem contains_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} :
    m.contains a = Raw₀.contains ⟨m, h.size_buckets_pos⟩ a

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α β
h : m.WF
a : α
⊢ m.contains a = Raw₀.contains ⟨m, ⋯⟩ a

Tactic:
simp [Raw.contains, h.size_buckets_pos]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem tendsto_atTop' [Nonempty β] [SemilatticeSup β] [NoMaxOrder β] {u : β → α} {a : α} :
    Tendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n > N, dist (u n) a < ε :=
  (atTop_basis_Ioi.tendsto_iff nhds_basis_ball).trans <| by
    simp only [true_and, gt_iff_lt, mem_Ioi, mem_ball]

Proof state:
α : Type u
β : Type v
inst✝³ : PseudoMetricSpace α
inst✝² : Nonempty β
inst✝¹ : SemilatticeSup β
inst✝ : NoMaxOrder β
u : β → α
a : α
⊢ (∀ (ib : ℝ), 0 < ib → ∃ ia, True ∧ ∀ x ∈ Ioi ia, u x ∈ ball a ib) ↔ ∀ ε > 0, ∃ N, ∀ n > N, dist (u n) a < ε

Tactic:
simp only [true_and, gt_iff_lt, mem_Ioi, mem_ball]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
lemma isIdempotentElemEquivClopens_mul (e₁ e₂ : {e : R | IsIdempotentElem e}) :
    isIdempotentElemEquivClopens ⟨_, e₁.2.mul e₂.2⟩ =
      isIdempotentElemEquivClopens e₁ ⊓ isIdempotentElemEquivClopens e₂ :=
  Clopens.ext <| by simp_rw [coe_isIdempotentElemEquivClopens_apply, basicOpen_mul]; rfl

Proof state:
R : Type u
inst✝ : CommRing R
e₁ e₂ : ↑{e | IsIdempotentElem e}
⊢ ↑(isIdempotentElemEquivClopens ⟨↑e₁ * ↑e₂, ⋯⟩) = ↑(isIdempotentElemEquivClopens e₁ ⊓ isIdempotentElemEquivClopens e₂)

Tactic:
simp_rw [coe_isIdempotentElemEquivClopens_apply, basicOpen_mul]

Result:
R : Type u
inst✝ : CommRing R
e₁ e₂ : ↑{e | IsIdempotentElem e}
⊢ ↑(basicOpen ↑e₁ ⊓ basicOpen ↑e₂) = ↑(isIdempotentElemEquivClopens e₁ ⊓ isIdempotentElemEquivClopens e₂)

Proof state:
R : Type u
inst✝ : CommRing R
e₁ e₂ : ↑{e | IsIdempotentElem e}
⊢ ↑(basicOpen ↑e₁ ⊓ basicOpen ↑e₂) = ↑(isIdempotentElemEquivClopens e₁ ⊓ isIdempotentElemEquivClopens e₂)

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem mk_add_mem_enumFrom_iff_getElem? {n i : Nat} {x : α} {l : List α} :
    (n + i, x) ∈ enumFrom n l ↔ l[i]? = some x

Proof state:
α : Type u_1
n i : Nat
x : α
l : List α
⊢ (n + i, x) ∈ enumFrom n l ↔ l[i]? = some x

Tactic:
simp [mem_iff_get?]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioi_subset_Ioi_iff : Ioi b ⊆ Ioi a ↔ a ≤ b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ioi b ⊆ Ioi a ↔ a ≤ b

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

Result:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : Ioi b ⊆ Ioi a
⊢ a ≤ b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : Ioi b ⊆ Ioi a
ba : ¬a ≤ b
⊢ False

Tactic:
exact lt_irrefl _ (h (not_le.mp ba))

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : Ioi b ⊆ Ioi a
⊢ a ≤ b

Tactic:
by_contra ba

Result:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : Ioi b ⊆ Ioi a
ba : ¬a ≤ b
⊢ False
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem LinearMap.toMatrix_mul (f g : M₁ →ₗ[R] M₁) :
    LinearMap.toMatrix v₁ v₁ (f * g) = LinearMap.toMatrix v₁ v₁ f * LinearMap.toMatrix v₁ v₁ g

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
f g : M₁ →ₗ[R] M₁
⊢ (toMatrix v₁ v₁) (f * g) = (toMatrix v₁ v₁) f * (toMatrix v₁ v₁) g

Tactic:
rw [LinearMap.mul_eq_comp, LinearMap.toMatrix_comp v₁ v₁ v₁ f g]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup'_union [DecidableEq β] {s₁ s₂ : Finset β} (h₁ : s₁.Nonempty) (h₂ : s₂.Nonempty)
    (f : β → α) :
    (s₁ ∪ s₂).sup' (h₁.mono subset_union_left) f = s₁.sup' h₁ f ⊔ s₂.sup' h₂ f :=
  eq_of_forall_ge_iff fun a => by simp [or_imp, forall_and]

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : DecidableEq β
s₁ s₂ : Finset β
h₁ : s₁.Nonempty
h₂ : s₂.Nonempty
f : β → α
a : α
⊢ (s₁ ∪ s₂).sup' ⋯ f ≤ a ↔ s₁.sup' h₁ f ⊔ s₂.sup' h₂ f ≤ a

Tactic:
simp [or_imp, forall_and]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean
theorem SuperpolynomialDecay.mul [ContinuousMul β] (hf : SuperpolynomialDecay l k f)
    (hg : SuperpolynomialDecay l k g) : SuperpolynomialDecay l k (f * g) := fun z => by
  simpa only [mul_assoc, one_mul, mul_zero, pow_zero] using (hf z).mul (hg 0)

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : CommSemiring β
inst✝ : ContinuousMul β
hf : SuperpolynomialDecay l k f
hg : SuperpolynomialDecay l k g
z : ℕ
⊢ Tendsto (fun a => k a ^ z * (f * g) a) l (𝓝 0)

Tactic:
simpa only [mul_assoc, one_mul, mul_zero, pow_zero] using (hf z).mul (hg 0)

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem lsub_eq_lsub {ι ι' : Type u} (r : ι → ι → Prop) (r' : ι' → ι' → Prop) [IsWellOrder ι r]
    [IsWellOrder ι' r'] {o} (ho : type r = o) (ho' : type r' = o)
    (f : ∀ a < o, Ordinal.{max u v}) :
    lsub.{_, v} (familyOfBFamily' r ho f) = lsub.{_, v} (familyOfBFamily' r' ho' f)

Proof state:
ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal.{u}
ho : type r = o
ho' : type r' = o
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ lsub (familyOfBFamily' r ho f) = lsub (familyOfBFamily' r' ho' f)

Tactic:
rw [lsub_eq_blsub', lsub_eq_blsub']

Result:
no goals
-- Mathlib/Topology/PartitionOfUnity.lean
theorem sum_finsupport (hx₀ : x₀ ∈ s) : ∑ i ∈ ρ.finsupport x₀, ρ i x₀ = 1

Proof state:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
hx₀ : x₀ ∈ s
⊢ ∑ i ∈ ρ.finsupport x₀, (ρ i) x₀ = 1

Tactic:
rw [← ρ.sum_eq_one hx₀, finsum_eq_sum_of_support_subset _ (ρ.coe_finsupport x₀).superset]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem angle_zero_right (x : V) : angle x 0 = π / 2

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V
⊢ angle x 0 = π / 2

Tactic:
unfold angle

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V
⊢ arccos (inner x 0 / (‖x‖ * ‖0‖)) = π / 2

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V
⊢ arccos (inner x 0 / (‖x‖ * ‖0‖)) = π / 2

Tactic:
rw [inner_zero_right, zero_div, Real.arccos_zero]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean
theorem evalWhiskerRight_cons_whisker {f g h i j k : C}
    {α : g ≅ f ⊗ h} {η : h ⟶ i} {ηs : f ⊗ i ⟶ j}
    {η₁ : h ⊗ k ⟶ i ⊗ k} {η₂ : f ⊗ (h ⊗ k) ⟶ f ⊗ (i ⊗ k)} {ηs₁ : (f ⊗ i) ⊗ k ⟶ j ⊗ k}
    {ηs₂ : f ⊗ (i ⊗ k) ⟶ j ⊗ k} {η₃ : f ⊗ (h ⊗ k) ⟶ j ⊗ k} {η₄ : (f ⊗ h) ⊗ k ⟶ j ⊗ k}
    {η₅ : g ⊗ k ⟶ j ⊗ k}
    (e_η₁ : ((Iso.refl _).hom ≫ η ≫ (Iso.refl _).hom) ▷ k = η₁) (e_η₂ : f ◁ η₁ = η₂)
    (e_ηs₁ : ηs ▷ k = ηs₁) (e_ηs₂ : (α_ _ _ _).inv ≫ ηs₁ = ηs₂)
    (e_η₃ : η₂ ≫ ηs₂ = η₃) (e_η₄ : (α_ _ _ _).hom ≫ η₃ = η₄)
    (e_η₅ : (whiskerRightIso α k).hom ≫ η₄ = η₅) :
    (α.hom ≫ (f ◁ η) ≫ ηs) ▷ k = η₅

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h i j k : C
α : g ≅ f ⊗ h
η : h ⟶ i
ηs : f ⊗ i ⟶ j
η₁ : h ⊗ k ⟶ i ⊗ k
η₂ : f ⊗ h ⊗ k ⟶ f ⊗ i ⊗ k
ηs₁ : (f ⊗ i) ⊗ k ⟶ j ⊗ k
ηs₂ : f ⊗ i ⊗ k ⟶ j ⊗ k
η₃ : f ⊗ h ⊗ k ⟶ j ⊗ k
η₄ : (f ⊗ h) ⊗ k ⟶ j ⊗ k
η₅ : g ⊗ k ⟶ j ⊗ k
e_η₁ : ((Iso.refl h).hom ≫ η ≫ (Iso.refl i).hom) ▷ k = η₁
e_η₂ : f ◁ η₁ = η₂
e_ηs₁ : ηs ▷ k = ηs₁
e_ηs₂ : (α_ f i k).inv ≫ ηs₁ = ηs₂
e_η₃ : η₂ ≫ ηs₂ = η₃
e_η₄ : (α_ f h k).hom ≫ η₃ = η₄
e_η₅ : (whiskerRightIso α k).hom ≫ η₄ = η₅
⊢ (α.hom ≫ f ◁ η ≫ ηs) ▷ k = η₅

Tactic:
simp at e_η₁ e_η₅

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h i j k : C
α : g ≅ f ⊗ h
η : h ⟶ i
ηs : f ⊗ i ⟶ j
η₁ : h ⊗ k ⟶ i ⊗ k
η₂ : f ⊗ h ⊗ k ⟶ f ⊗ i ⊗ k
ηs₁ : (f ⊗ i) ⊗ k ⟶ j ⊗ k
ηs₂ : f ⊗ i ⊗ k ⟶ j ⊗ k
η₃ : f ⊗ h ⊗ k ⟶ j ⊗ k
η₄ : (f ⊗ h) ⊗ k ⟶ j ⊗ k
η₅ : g ⊗ k ⟶ j ⊗ k
e_η₂ : f ◁ η₁ = η₂
e_ηs₁ : ηs ▷ k = ηs₁
e_ηs₂ : (α_ f i k).inv ≫ ηs₁ = ηs₂
e_η₃ : η₂ ≫ ηs₂ = η₃
e_η₄ : (α_ f h k).hom ≫ η₃ = η₄
e_η₅ : α.hom ▷ k ≫ η₄ = η₅
e_η₁ : η ▷ k = η₁
⊢ (α.hom ≫ f ◁ η ≫ ηs) ▷ k = η₅

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h i j k : C
α : g ≅ f ⊗ h
η : h ⟶ i
ηs : f ⊗ i ⟶ j
η₁ : h ⊗ k ⟶ i ⊗ k
η₂ : f ⊗ h ⊗ k ⟶ f ⊗ i ⊗ k
ηs₁ : (f ⊗ i) ⊗ k ⟶ j ⊗ k
ηs₂ : f ⊗ i ⊗ k ⟶ j ⊗ k
η₃ : f ⊗ h ⊗ k ⟶ j ⊗ k
η₄ : (f ⊗ h) ⊗ k ⟶ j ⊗ k
η₅ : g ⊗ k ⟶ j ⊗ k
e_η₂ : f ◁ η₁ = η₂
e_ηs₁ : ηs ▷ k = ηs₁
e_ηs₂ : (α_ f i k).inv ≫ ηs₁ = ηs₂
e_η₃ : η₂ ≫ ηs₂ = η₃
e_η₄ : (α_ f h k).hom ≫ η₃ = η₄
e_η₅ : α.hom ▷ k ≫ η₄ = η₅
e_η₁ : η ▷ k = η₁
⊢ (α.hom ≫ f ◁ η ≫ ηs) ▷ k = η₅

Tactic:
simp [e_η₁, e_η₂, e_ηs₁, e_ηs₂, e_η₃, e_η₄, e_η₅]

Result:
no goals
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem closure_range_of (α) :
    Subgroup.closure (Set.range (FreeGroup.of : α → FreeGroup α)) = ⊤

Proof state:
α : Type u_1
⊢ Subgroup.closure (Set.range of) = ⊤

Tactic:
rw [← lift.range_eq_closure, lift_of_eq_id]

Result:
α : Type u_1
⊢ (MonoidHom.id (FreeGroup α)).range = ⊤

Proof state:
α : Type u_1
⊢ (MonoidHom.id (FreeGroup α)).range = ⊤

Tactic:
exact MonoidHom.range_eq_top.2 Function.surjective_id

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem inv_smul_integral_comp_add_div (c d) :
    (c⁻¹ • ∫ x in a..b, f (d + x / c)) = ∫ x in d + a / c..d + b / c, f x

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
⊢ c⁻¹ • ∫ (x : ℝ) in a..b, f (d + x / c) = ∫ (x : ℝ) in d + a / c..d + b / c, f x

Tactic:
by_cases hc : c = 0 <;> simp [hc, integral_comp_add_div]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toList_snd_unzip (as : Array (α × β)) :
    as.unzip.2.toList = as.toList.unzip.2

Proof state:
α : Type u_1
β : Type u_2
as : Array (α × β)
⊢ as.unzip.snd.toList = as.toList.unzip.snd

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Integral.lean
theorem iff_exists_smul_integral [IsReduced R] :
    IsAlgebraic R z ↔ ∃ y ≠ (0 : R), IsIntegral R (y • z) :=
  ⟨(exists_integral_multiple ·), fun ⟨_, hy, int⟩ ↦
    of_smul_isIntegral (by rwa [isNilpotent_iff_eq_zero]) int⟩

Proof state:
R : Type u_1
A : Type u_3
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
z : A
inst✝ : IsReduced R
x✝ : ∃ y, y ≠ 0 ∧ IsIntegral R (y • z)
w✝ : R
hy : w✝ ≠ 0
int : IsIntegral R (w✝ • z)
⊢ ¬IsNilpotent w✝

Tactic:
rwa [isNilpotent_iff_eq_zero]

Result:
no goals
-- Mathlib/Algebra/Group/Support.lean
theorem mulSupport_nonempty_iff {f : α → M} : (mulSupport f).Nonempty ↔ f ≠ 1

Proof state:
α : Type u_1
M : Type u_5
inst✝ : One M
f : α → M
⊢ (mulSupport f).Nonempty ↔ f ≠ 1

Tactic:
rw [nonempty_iff_ne_empty, Ne, mulSupport_eq_empty_iff]

Result:
no goals
-- Mathlib/Analysis/Fourier/FourierTransform.lean
theorem fourierIntegral_real_eq_integral_exp_smul (f : ℝ → E) (w : ℝ) :
    𝓕 f w = ∫ v : ℝ, Complex.exp (↑(-2 * π * v * w) * Complex.I) • f v

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
w : ℝ
⊢ 𝓕 f w = ∫ (v : ℝ), Complex.exp (↑(-2 * π * v * w) * Complex.I) • f v

Tactic:
simp_rw [fourierIntegral_real_eq, Circle.smul_def, Real.fourierChar_apply, mul_neg, neg_mul,
  mul_assoc]

Result:
no goals
-- Mathlib/GroupTheory/Subgroup/Center.lean
theorem mem_center_iff {z : G} : z ∈ center G ↔ ∀ g, g * z = z * g

Proof state:
G : Type u_1
inst✝ : Group G
z : G
⊢ z ∈ center G ↔ z ∈ Set.center G

Tactic:
exact Iff.rfl

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
z : G
⊢ z ∈ center G ↔ ∀ (g : G), g * z = z * g

Tactic:
rw [← Semigroup.mem_center_iff]

Result:
G : Type u_1
inst✝ : Group G
z : G
⊢ z ∈ center G ↔ z ∈ Set.center G
-- Mathlib/Topology/Sets/Closeds.lean
theorem Closeds.isAtom_iff [T1Space α] {s : Closeds α} :
    IsAtom s ↔ ∃ x, s = Closeds.singleton x

Proof state:
α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Closeds α
⊢ IsAtom s ↔ ∃ x, s = singleton x

Tactic:
simp [← Closeds.isAtom_coe, Set.isAtom_iff, SetLike.ext_iff, Set.ext_iff]

Result:
no goals
-- Mathlib/Algebra/Lie/CartanSubalgebra.lean
theorem normalizer_eq_self_of_isCartanSubalgebra (H : LieSubalgebra R L) [H.IsCartanSubalgebra] :
    H.toLieSubmodule.normalizer = H.toLieSubmodule

Proof state:
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : H.IsCartanSubalgebra
⊢ H.toLieSubmodule.normalizer = H.toLieSubmodule

Tactic:
rw [← LieSubmodule.toSubmodule_inj, coe_normalizer_eq_normalizer,
  IsCartanSubalgebra.self_normalizing, coe_toLieSubmodule]

Result:
no goals
-- Mathlib/Topology/NhdsSet.lean
theorem eventually_nhdsSet_iUnion {ι : Sort*} {s : ι → Set X} {P : X → Prop} :
    (∀ᶠ x in 𝓝ˢ (⋃ i, s i), P x) ↔ ∀ i, ∀ᶠ x in 𝓝ˢ (s i), P x

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
ι : Sort u_3
s : ι → Set X
P : X → Prop
⊢ (∀ᶠ (x : X) in 𝓝ˢ (⋃ i, s i), P x) ↔ ∀ (i : ι), ∀ᶠ (x : X) in 𝓝ˢ (s i), P x

Tactic:
simp only [nhdsSet_iUnion, eventually_iSup]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem toSubring_one :
    toSubring (1 : R[X]) T
        (Set.Subset.trans coeffs_one <| Finset.singleton_subset_set_iff.2 T.one_mem) =
      1 :=
  ext fun i => Subtype.eq <| by
    rw [coeff_toSubring', coeff_one, coeff_one, apply_ite Subtype.val, ZeroMemClass.coe_zero,
      OneMemClass.coe_one]

Proof state:
R : Type u
inst✝ : Ring R
T : Subring R
i : ℕ
⊢ ↑((toSubring 1 T ⋯).coeff i) = ↑(coeff 1 i)

Tactic:
rw [coeff_toSubring', coeff_one, coeff_one, apply_ite Subtype.val, ZeroMemClass.coe_zero,
  OneMemClass.coe_one]

Result:
no goals
-- Mathlib/RingTheory/Ideal/GoingUp.lean
theorem IsIntegralClosure.eq_bot_of_comap_eq_bot [Nontrivial R] {I : Ideal A} :
    I.comap (algebraMap R A) = ⊥ → I = ⊥

Proof state:
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A S
inst✝³ : IsScalarTower R A S
inst✝² : IsIntegralClosure A R S
inst✝¹ : IsDomain A
inst✝ : Nontrivial R
I : Ideal A
⊢ comap (algebraMap R A) I = ⊥ → I = ⊥

Tactic:
contrapose

Result:
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A S
inst✝³ : IsScalarTower R A S
inst✝² : IsIntegralClosure A R S
inst✝¹ : IsDomain A
inst✝ : Nontrivial R
I : Ideal A
⊢ ¬I = ⊥ → ¬comap (algebraMap R A) I = ⊥

Proof state:
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
A : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra A S
inst✝³ : IsScalarTower R A S
inst✝² : IsIntegralClosure A R S
inst✝¹ : IsDomain A
inst✝ : Nontrivial R
I : Ideal A
⊢ ¬I = ⊥ → ¬comap (algebraMap R A) I = ⊥

Tactic:
exact (IsIntegralClosure.comap_ne_bot S)

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
lemma predAbove_castPred_of_lt (p i : Fin (n + 1)) (h : p < i) (hp := Fin.ne_last_of_lt h)
  (hi := Fin.ne_zero_of_lt h) : (castPred p hp).predAbove i = pred i hi

Proof state:
n : ℕ
p i : Fin (n + 1)
h : p < i
hp : optParam (p ≠ last n) ⋯
hi : optParam (i ≠ 0) ⋯
⊢ (p.castPred hp).predAbove i = i.pred hi

Tactic:
rw [predAbove_of_castSucc_lt _ _ (castSucc_castPred _ _ ▸ h)]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
lemma IsColimit.isIso_ι_app_of_isTerminal {F : J ⥤ C} {c : Cocone F} (hc : IsColimit c)
    (X : J) (hX : IsTerminal X) :
    IsIso (c.ι.app X)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X : J
hX : IsTerminal X
⊢ IsIso (c.ι.app X)

Tactic:
change IsIso (coconePointUniqueUpToIso (colimitOfDiagramTerminal hX F) hc).hom

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X : J
hX : IsTerminal X
⊢ IsIso ((colimitOfDiagramTerminal hX F).coconePointUniqueUpToIso hc).hom

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X : J
hX : IsTerminal X
⊢ IsIso ((colimitOfDiagramTerminal hX F).coconePointUniqueUpToIso hc).hom

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
/-- An alternative description of the slit plane as consisting of nonzero complex numbers
whose argument is not π. -/
lemma mem_slitPlane_iff_arg {z : ℂ} : z ∈ slitPlane ↔ z.arg ≠ π ∧ z ≠ 0

Proof state:
z : ℂ
⊢ z ∈ slitPlane ↔ z.arg ≠ π ∧ z ≠ 0

Tactic:
simp only [mem_slitPlane_iff_not_le_zero, le_iff_lt_or_eq, ne_eq, arg_eq_pi_iff_lt_zero, not_or]

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem isBounded_bot : IsBounded r ⊥ ↔ Nonempty α

Proof state:
α : Type u_1
r : α → α → Prop
⊢ IsBounded r ⊥ ↔ Nonempty α

Tactic:
simp [IsBounded, exists_true_iff_nonempty]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKeyD_modify_self [LawfulBEq α] [Inhabited α] {k fallback : α} {f : β k → β k} (h : m.WF) :
    (m.modify k f).getKeyD k fallback = if k ∈ m then k else fallback

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k fallback : α
f : β k → β k
h : m.WF
⊢ (m.modify k f).getKeyD k fallback = if m.contains k = true then k else fallback

Tactic:
simp_to_raw using Raw₀.getKeyD_modify_self

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k fallback : α
f : β k → β k
h : m.WF
⊢ (m.modify k f).getKeyD k fallback = if k ∈ m then k else fallback

Tactic:
simp only [mem_iff_contains]

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k fallback : α
f : β k → β k
h : m.WF
⊢ (m.modify k f).getKeyD k fallback = if m.contains k = true then k else fallback
-- Mathlib/Data/Num/Lemmas.lean
theorem pred'_succ' (n) : pred' (succ' n) = n :=
  Num.to_nat_inj.1 <| by rw [pred'_to_nat, succ'_to_nat, Nat.add_one, Nat.pred_succ]

Proof state:
n : Num
⊢ ↑n.succ'.pred' = ↑n

Tactic:
rw [pred'_to_nat, succ'_to_nat, Nat.add_one, Nat.pred_succ]

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem derivative_rootMultiplicity_of_root [CharZero R] {p : R[X]} {t : R} (hpt : p.IsRoot t) :
    p.derivative.rootMultiplicity t = p.rootMultiplicity t - 1

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : p.IsRoot t
⊢ rootMultiplicity t (derivative p) = rootMultiplicity t p - 1

Tactic:
by_cases h : p = 0

Result:
case pos
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : p.IsRoot t
h : p = 0
⊢ rootMultiplicity t (derivative p) = rootMultiplicity t p - 1

case neg
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
⊢ rootMultiplicity t (derivative p) = rootMultiplicity t p - 1

Proof state:
case neg
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : p.IsRoot t
h : ¬p = 0
⊢ rootMultiplicity t (derivative p) = rootMultiplicity t p - 1

Tactic:
exact derivative_rootMultiplicity_of_root_of_mem_nonZeroDivisors hpt <|
  mem_nonZeroDivisors_of_ne_zero <| Nat.cast_ne_zero.2 ((rootMultiplicity_pos h).2 hpt).ne'

Result:
no goals

Proof state:
case pos
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : p.IsRoot t
h : p = 0
⊢ rootMultiplicity t (derivative p) = rootMultiplicity t p - 1

Tactic:
rw [h, map_zero, rootMultiplicity_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem basis_pair_right (hij : i ≠ j) : Lagrange.basis {i, j} v j = basisDivisor (v j) (v i)

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
v : ι → F
i j : ι
hij : i ≠ j
⊢ Lagrange.basis {i, j} v j = basisDivisor (v j) (v i)

Tactic:
rw [pair_comm]

Result:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
v : ι → F
i j : ι
hij : i ≠ j
⊢ Lagrange.basis {j, i} v j = basisDivisor (v j) (v i)

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
v : ι → F
i j : ι
hij : i ≠ j
⊢ Lagrange.basis {j, i} v j = basisDivisor (v j) (v i)

Tactic:
exact basis_pair_left hij.symm

Result:
no goals
-- Mathlib/Data/Rat/Cast/Order.lean
@[simp] lemma cast_le_one : (p : K) ≤ 1 ↔ p ≤ 1

Proof state:
K : Type u_5
inst✝ : LinearOrderedSemifield K
p : ℚ≥0
⊢ ↑p ≤ 1 ↔ p ≤ 1

Tactic:
norm_cast

Result:
no goals
-- Mathlib/LinearAlgebra/TensorPower/Pairing.lean
@[simp]
lemma pairingDual_tprod_tprod (f : (_ : Fin n) → Module.Dual R M) (v : Fin n → M) :
    pairingDual R M n (tprod _ f) (tprod _ v) = ∏ i, (f i (v i))

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
f : Fin n → Module.Dual R M
v : Fin n → M
⊢ ((pairingDual R M n) ((tprod R) f)) ((tprod R) v) = ∏ i : Fin n, (f i) (v i)

Tactic:
simp [pairingDual]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/PolarCoord.lean
theorem hasFDerivAt_pi_polarCoord_symm (p : ι → ℝ × ℝ) :
    HasFDerivAt (fun x i ↦ polarCoord.symm (x i)) (fderivPiPolarCoordSymm p) p

Proof state:
ι : Type u_1
inst✝ : Fintype ι
p : ι → ℝ × ℝ
⊢ HasFDerivAt (fun x i => ↑polarCoord.symm (x i)) (fderivPiPolarCoordSymm p) p

Tactic:
rw [fderivPiPolarCoordSymm, hasFDerivAt_pi]

Result:
ι : Type u_1
inst✝ : Fintype ι
p : ι → ℝ × ℝ
⊢ ∀ (i : ι),
    HasFDerivAt (fun x => ↑polarCoord.symm (x i)) ((fderivPolarCoordSymm (p i)).comp (ContinuousLinearMap.proj i)) p

Proof state:
ι : Type u_1
inst✝ : Fintype ι
p : ι → ℝ × ℝ
⊢ ∀ (i : ι),
    HasFDerivAt (fun x => ↑polarCoord.symm (x i)) ((fderivPolarCoordSymm (p i)).comp (ContinuousLinearMap.proj i)) p

Tactic:
exact fun i ↦ HasFDerivAt.comp _ (hasFDerivAt_polarCoord_symm _) (hasFDerivAt_apply i _)

Result:
no goals