harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Analysis/Topology.lean
theorem ext' [T : TopologicalSpace α] {σ : Type*} {F : Ctop α σ}
    (H : ∀ a s, s ∈ 𝓝 a ↔ ∃ b, a ∈ F b ∧ F b ⊆ s) : F.toTopsp = T

Proof state:
α : Type u_1
T : TopologicalSpace α
σ : Type u_5
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ b, a ∈ F.f b ∧ F.f b ⊆ s
⊢ F.toTopsp = T

Tactic:
refine TopologicalSpace.ext_nhds fun x ↦ ?_

Result:
α : Type u_1
T : TopologicalSpace α
σ : Type u_5
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ b, a ∈ F.f b ∧ F.f b ⊆ s
x : α
⊢ 𝓝 x = 𝓝 x

Proof state:
α : Type u_1
T : TopologicalSpace α
σ : Type u_5
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ b, a ∈ F.f b ∧ F.f b ⊆ s
x : α
⊢ 𝓝 x = 𝓝 x

Tactic:
ext s

Result:
case h
α : Type u_1
T : TopologicalSpace α
σ : Type u_5
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ b, a ∈ F.f b ∧ F.f b ⊆ s
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ s ∈ 𝓝 x

Proof state:
case h
α : Type u_1
T : TopologicalSpace α
σ : Type u_5
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ b, a ∈ F.f b ∧ F.f b ⊆ s
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ s ∈ 𝓝 x

Tactic:
rw [mem_nhds_toTopsp, H]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioo_union_right (hab : a < b) : Ioo a b ∪ {b} = Ioc a b

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b : α
hab : a < b
⊢ Ioo a b ∪ {b} = Ioc a b

Tactic:
simpa only [dual_Ioo, dual_Ico] using Ioo_union_left hab.dual

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem contains_insert_self [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
    (m.insert k v).contains k

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k : α
v : β k
⊢ (m.insert k v).contains k = true

Tactic:
simp_to_model [insert] using List.containsKey_insertEntry_self

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem irreducible_pow_sup [DecidableEq (Ideal T)] (hI : I ≠ ⊥) (hJ : Irreducible J) (n : ℕ) :
    J ^ n ⊔ I = J ^ min ((normalizedFactors I).count J) n

Proof state:
T : Type u_4
inst✝² : CommRing T
inst✝¹ : IsDedekindDomain T
I J : Ideal T
inst✝ : DecidableEq (Ideal T)
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
⊢ J ^ n ⊔ I = J ^ (count J (normalizedFactors I) ⊓ n)

Tactic:
rw [sup_eq_prod_inf_factors (pow_ne_zero n hJ.ne_zero) hI, min_comm,
  normalizedFactors_of_irreducible_pow hJ, normalize_eq J, replicate_inter, prod_replicate]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem back?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : Array α)
    (H : ∀ (a : α), a ∈ xs → P a) :
    (xs.pmap f H).back? = xs.attach.back?.map fun ⟨a, m⟩ => f a (H a m)

Proof state:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
xs : Array α
H : ∀ (a : α), a ∈ xs → P a
⊢ (pmap f xs H).back? =
    Option.map
      (fun x =>
        match x with
        | ⟨a, m⟩ => f a ⋯)
      xs.attach.back?

Tactic:
cases xs

Result:
case mk
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → P a
⊢ (pmap f { toList := toList✝ } H).back? =
    Option.map
      (fun x =>
        match x with
        | ⟨a, m⟩ => f a ⋯)
      { toList := toList✝ }.attach.back?

Proof state:
case mk
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → P a
⊢ (pmap f { toList := toList✝ } H).back? =
    Option.map
      (fun x =>
        match x with
        | ⟨a, m⟩ => f a ⋯)
      { toList := toList✝ }.attach.back?

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem length_le_iff' {s : Seq α} {n : ℕ} :
    (∃ h, s.length h ≤ n) ↔ s.TerminatedAt n

Proof state:
case refine_2
α : Type u
s : Seq α
n : ℕ
hn : s.get? n = none
⊢ (∃ n, s.get? n = none) ∧ ∃ m, m ≤ n ∧ s.get? m = none

Tactic:
exact ⟨⟨n, hn⟩, ⟨n, le_rfl, hn⟩⟩

Result:
no goals

Proof state:
case refine_1
α : Type u
s : Seq α
n : ℕ
⊢ ((∃ n, s.get? n = none) ∧ ∃ m, m ≤ n ∧ s.get? m = none) → s.get? n = none

Tactic:
rintro ⟨_, k, hkn, hk⟩

Result:
case refine_1.intro.intro.intro
α : Type u
s : Seq α
n : ℕ
left✝ : ∃ n, s.get? n = none
k : ℕ
hkn : k ≤ n
hk : s.get? k = none
⊢ s.get? n = none

Proof state:
α : Type u
s : Seq α
n : ℕ
⊢ (∃ h, s.length h ≤ n) ↔ s.TerminatedAt n

Tactic:
simp only [length, Nat.find_le_iff, TerminatedAt, Terminates, exists_prop]

Result:
α : Type u
s : Seq α
n : ℕ
⊢ ((∃ n, s.get? n = none) ∧ ∃ m, m ≤ n ∧ s.get? m = none) ↔ s.get? n = none

Proof state:
α : Type u
s : Seq α
n : ℕ
⊢ ((∃ n, s.get? n = none) ∧ ∃ m, m ≤ n ∧ s.get? m = none) ↔ s.get? n = none

Tactic:
refine ⟨?_, ?_⟩

Result:
case refine_1
α : Type u
s : Seq α
n : ℕ
⊢ ((∃ n, s.get? n = none) ∧ ∃ m, m ≤ n ∧ s.get? m = none) → s.get? n = none

case refine_2
α : Type u
s : Seq α
n : ℕ
⊢ s.get? n = none → (∃ n, s.get? n = none) ∧ ∃ m, m ≤ n ∧ s.get? m = none

Proof state:
case refine_2
α : Type u
s : Seq α
n : ℕ
⊢ s.get? n = none → (∃ n, s.get? n = none) ∧ ∃ m, m ≤ n ∧ s.get? m = none

Tactic:
intro hn

Result:
case refine_2
α : Type u
s : Seq α
n : ℕ
hn : s.get? n = none
⊢ (∃ n, s.get? n = none) ∧ ∃ m, m ≤ n ∧ s.get? m = none

Proof state:
case refine_1.intro.intro.intro
α : Type u
s : Seq α
n : ℕ
left✝ : ∃ n, s.get? n = none
k : ℕ
hkn : k ≤ n
hk : s.get? k = none
⊢ s.get? n = none

Tactic:
exact le_stable s hkn hk

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Maps.lean
lemma le_comap_of_subsingleton (f : V → W) [Subsingleton V] : G ≤ G'.comap f

Proof state:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : V → W
inst✝ : Subsingleton V
v w : V
⊢ G.Adj v w → (SimpleGraph.comap f G').Adj v w

Tactic:
simp [Subsingleton.elim v w]

Result:
no goals

Proof state:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : V → W
inst✝ : Subsingleton V
⊢ G ≤ SimpleGraph.comap f G'

Tactic:
intros v w

Result:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : V → W
inst✝ : Subsingleton V
v w : V
⊢ G.Adj v w → (SimpleGraph.comap f G').Adj v w
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_smul_real_right (x y : E) (r : ℝ) : ⟪x, (r : 𝕜) • y⟫ = r • ⟪x, y⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
r : ℝ
⊢ ⟪x, ↑r • y⟫_𝕜 = r • ⟪x, y⟫_𝕜

Tactic:
rw [inner_smul_right, Algebra.smul_def]

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Opposite/Pretriangulated.lean
lemma isomorphic_distinguished (T₁ : Triangle Cᵒᵖ)
    (hT₁ : T₁ ∈ distinguishedTriangles C) (T₂ : Triangle Cᵒᵖ) (e : T₂ ≅ T₁) :
    T₂ ∈ distinguishedTriangles C

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T₁ : Triangle Cᵒᵖ
hT₁ : T₁ ∈ distinguishedTriangles C
T₂ : Triangle Cᵒᵖ
e : T₂ ≅ T₁
⊢ T₂ ∈ distinguishedTriangles C

Tactic:
simp only [mem_distinguishedTriangles_iff] at hT₁ ⊢

Result:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T₁ T₂ : Triangle Cᵒᵖ
e : T₂ ≅ T₁
hT₁ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁) ∈ Pretriangulated.distinguishedTriangles
⊢ Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂) ∈ Pretriangulated.distinguishedTriangles

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T₁ T₂ : Triangle Cᵒᵖ
e : T₂ ≅ T₁
hT₁ : Opposite.unop ((triangleOpEquivalence C).inverse.obj T₁) ∈ Pretriangulated.distinguishedTriangles
⊢ Opposite.unop ((triangleOpEquivalence C).inverse.obj T₂) ∈ Pretriangulated.distinguishedTriangles

Tactic:
exact Pretriangulated.isomorphic_distinguished _ hT₁ _
  ((triangleOpEquivalence C).inverse.mapIso e).unop.symm

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_inv_coe_angle (x : ℂ) : (arg x⁻¹ : Real.Angle) = -arg x

Proof state:
x : ℂ
⊢ ↑x⁻¹.arg = -↑x.arg

Tactic:
by_cases h : arg x = π <;> simp [arg_inv, h]

Result:
no goals
-- Mathlib/Data/Rat/Defs.lean
theorem eq_iff_mul_eq_mul {p q : ℚ} : p = q ↔ p.num * q.den = q.num * p.den

Proof state:
case z₂
p q : ℚ
⊢ ↑q.den ≠ 0

Tactic:
rw [← Int.natCast_zero, Ne, Int.ofNat_inj]

Result:
case z₂
p q : ℚ
⊢ ¬q.den = 0

Proof state:
p q : ℚ
⊢ p = q ↔ p.num * ↑q.den = q.num * ↑p.den

Tactic:
conv =>
  lhs
  rw [← num_divInt_den p, ← num_divInt_den q]

Result:
p q : ℚ
⊢ p.num /. ↑p.den = q.num /. ↑q.den ↔ p.num * ↑q.den = q.num * ↑p.den

Proof state:
case z₂
p q : ℚ
⊢ ¬q.den = 0

Tactic:
apply den_nz

Result:
no goals
-- Mathlib/Data/Fintype/Card.lean
theorem injective_iff_surjective_of_equiv {f : α → β} (e : α ≃ β) : Injective f ↔ Surjective f :=
  have : Injective (e.symm ∘ f) ↔ Surjective (e.symm ∘ f) := injective_iff_surjective
  ⟨fun hinj => by
    simpa [Function.comp] using e.surjective.comp (this.1 (e.symm.injective.comp hinj)),
    fun hsurj => by
    simpa [Function.comp] using e.injective.comp (this.2 (e.symm.surjective.comp hsurj))⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
e : α ≃ β
this : Injective (⇑e.symm ∘ f) ↔ Surjective (⇑e.symm ∘ f)
hinj : Injective f
⊢ Surjective f

Tactic:
simpa [Function.comp] using e.surjective.comp (this.1 (e.symm.injective.comp hinj))

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
e : α ≃ β
this : Injective (⇑e.symm ∘ f) ↔ Surjective (⇑e.symm ∘ f)
hsurj : Surjective f
⊢ Injective f

Tactic:
simpa [Function.comp] using e.injective.comp (this.2 (e.symm.surjective.comp hsurj))

Result:
no goals
-- Mathlib/GroupTheory/QuotientGroup/Basic.lean
theorem subgroup_eq_top_of_subsingleton (H : Subgroup G) (h : Subsingleton (G ⧸ H)) : H = ⊤ :=
  top_unique fun x _ => by
    have this : 1⁻¹ * x ∈ H := QuotientGroup.eq.1 (Subsingleton.elim _ _)
    rwa [inv_one, one_mul] at this

Proof state:
G : Type u
inst✝ : Group G
H : Subgroup G
h : Subsingleton (G ⧸ H)
x : G
x✝ : x ∈ ⊤
this : 1⁻¹ * x ∈ H
⊢ x ∈ H

Tactic:
rwa [inv_one, one_mul] at this

Result:
no goals

Proof state:
G : Type u
inst✝ : Group G
H : Subgroup G
h : Subsingleton (G ⧸ H)
x : G
x✝ : x ∈ ⊤
⊢ x ∈ H

Tactic:
have this : 1⁻¹ * x ∈ H := QuotientGroup.eq.1 (Subsingleton.elim _ _)

Result:
G : Type u
inst✝ : Group G
H : Subgroup G
h : Subsingleton (G ⧸ H)
x : G
x✝ : x ∈ ⊤
this : 1⁻¹ * x ∈ H
⊢ x ∈ H
-- Mathlib/Data/Set/Function.lean
theorem BijOn.exists_extend {t' : Set β} (h : BijOn f s t) (htt' : t ⊆ t') (ht' : t' ⊆ range f) :
    ∃ s', s ⊆ s' ∧ BijOn f s' t'

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
htt' : t ⊆ t'
ht' : t' ⊆ range f
⊢ SurjOn f univ t'

Tactic:
simpa [SurjOn]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
htt' : t ⊆ t'
ht' : t' ⊆ range f
⊢ ∃ s', s ⊆ s' ∧ BijOn f s' t'

Tactic:
simpa using h.exists_extend_of_subset (subset_univ s) htt' (by simpa [SurjOn])

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem tangentMapWithin_univ : tangentMapWithin I I' f univ = tangentMap I I' f

Proof state:
case h
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
p : TangentBundle I M
⊢ tangentMapWithin I I' f univ p = tangentMap I I' f p

Tactic:
simp only [tangentMapWithin, tangentMap, mfld_simps]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
⊢ tangentMapWithin I I' f univ = tangentMap I I' f

Tactic:
ext p : 1

Result:
case h
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
p : TangentBundle I M
⊢ tangentMapWithin I I' f univ p = tangentMap I I' f p
-- Mathlib/Data/Stream/Init.lean
theorem cycle_singleton (a : α) : cycle [a] (by simp) = const a :=
  coinduction rfl fun β fr ch => by rwa [cycle_eq, const_eq]

Proof state:
α : Type u
a : α
β : Type u
fr : Stream' α → β
ch : fr (cycle [a] ⋯) = fr (const a)
⊢ fr (cycle [a] ⋯).tail = fr (const a).tail

Tactic:
rwa [cycle_eq, const_eq]

Result:
no goals

Proof state:
α : Type u
β : Type v
δ : Type w
m n : ℕ
x y : List α
a✝ b : Stream' α
a : α
⊢ [a] ≠ []

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/Normal/Defs.lean
theorem AlgHom.restrictNormal_comp [Normal F E] :
    (ψ.restrictNormal E).comp (ϕ.restrictNormal E) = (ψ.comp ϕ).restrictNormal E :=
  AlgHom.ext fun _ =>
    (algebraMap E K₃).injective (by simp only [AlgHom.comp_apply, AlgHom.restrictNormal_commutes])

Proof state:
F : Type u_1
inst✝¹⁵ : Field F
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst✝¹⁴ : Field K₁
inst✝¹³ : Field K₂
inst✝¹² : Field K₃
inst✝¹¹ : Algebra F K₁
inst✝¹⁰ : Algebra F K₂
inst✝⁹ : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
E : Type u_6
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra E K₁
inst✝⁵ : Algebra E K₂
inst✝⁴ : Algebra E K₃
inst✝³ : IsScalarTower F E K₁
inst✝² : IsScalarTower F E K₂
inst✝¹ : IsScalarTower F E K₃
inst✝ : Normal F E
x✝ : E
⊢ (algebraMap E K₃) (((ψ.restrictNormal E).comp (ϕ.restrictNormal E)) x✝) =
    (algebraMap E K₃) (((ψ.comp ϕ).restrictNormal E) x✝)

Tactic:
simp only [AlgHom.comp_apply, AlgHom.restrictNormal_commutes]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getEntry?_replaceEntry_of_containsKey_eq_false [BEq α] {l : List ((a : α) × β a)} {a k : α}
    {v : β k} (hl : containsKey k l = false) :
    getEntry? a (replaceEntry k v l) = getEntry? a l

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
a k : α
v : β k
hl : containsKey k l = false
⊢ getEntry? a (replaceEntry k v l) = getEntry? a l

Tactic:
rw [replaceEntry_of_containsKey_eq_false hl]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean
theorem liftAlgHom_fieldRange (hg : Function.Injective g) :
    (liftAlgHom hg : K →ₐ[F] L).fieldRange = IntermediateField.adjoin F g.range :=
  algHom_fieldRange_eq_of_comp_eq (by ext; simp)

Proof state:
case a
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst✝⁹ : Field F
inst✝⁸ : CommRing A
inst✝⁷ : Algebra F A
inst✝⁶ : Field K
inst✝⁵ : Algebra F K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
inst✝² : Field L
inst✝¹ : Algebra F L
g : A →ₐ[F] L
inst✝ : IsScalarTower F A K
hg : Function.Injective ⇑g
x✝ : A
⊢ ((↑(liftAlgHom hg)).comp (algebraMap A K)) x✝ = ↑g x✝

Tactic:
simp

Result:
no goals

Proof state:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst✝⁹ : Field F
inst✝⁸ : CommRing A
inst✝⁷ : Algebra F A
inst✝⁶ : Field K
inst✝⁵ : Algebra F K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
inst✝² : Field L
inst✝¹ : Algebra F L
g : A →ₐ[F] L
inst✝ : IsScalarTower F A K
hg : Function.Injective ⇑g
⊢ (↑(liftAlgHom hg)).comp (algebraMap A K) = ↑g

Tactic:
ext

Result:
case a
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst✝⁹ : Field F
inst✝⁸ : CommRing A
inst✝⁷ : Algebra F A
inst✝⁶ : Field K
inst✝⁵ : Algebra F K
inst✝⁴ : Algebra A K
inst✝³ : IsFractionRing A K
inst✝² : Field L
inst✝¹ : Algebra F L
g : A →ₐ[F] L
inst✝ : IsScalarTower F A K
hg : Function.Injective ⇑g
x✝ : A
⊢ ((↑(liftAlgHom hg)).comp (algebraMap A K)) x✝ = ↑g x✝
-- Mathlib/ModelTheory/Types.lean
theorem setOf_mem_eq_univ_iff (φ : L[[α]].Sentence) :
    { p : T.CompleteType α | φ ∈ p } = Set.univ ↔ (L.lhomWithConstants α).onTheory T ⊨ᵇ φ

Proof state:
L : Language
T : L.Theory
α : Type w
φ : L[[α]].Sentence
⊢ {p | Formula.not φ ∈ p} = ∅ ↔ {p | {Formula.not φ} ⊆ ↑p} = ∅

Tactic:
simp

Result:
no goals

Proof state:
L : Language
T : L.Theory
α : Type w
φ : L[[α]].Sentence
⊢ {p | φ ∈ p} = Set.univ ↔ (L.lhomWithConstants α).onTheory T ⊨ᵇ φ

Tactic:
rw [models_iff_not_satisfiable, ← compl_empty_iff, compl_setOf_mem, ← setOf_subset_eq_empty_iff]

Result:
L : Language
T : L.Theory
α : Type w
φ : L[[α]].Sentence
⊢ {p | Formula.not φ ∈ p} = ∅ ↔ {p | {Formula.not φ} ⊆ ↑p} = ∅
-- Mathlib/Tactic/CancelDenoms/Core.lean
theorem sub_subst {α} [Ring α] {n e1 e2 t1 t2 : α} (h1 : n * e1 = t1) (h2 : n * e2 = t2) :
    n * (e1 - e2) = t1 - t2

Proof state:
α : Type u_1
inst✝ : Ring α
n e1 e2 t1 t2 : α
h1 : n * e1 = t1
h2 : n * e2 = t2
⊢ n * (e1 - e2) = t1 - t2

Tactic:
simp [left_distrib, *, sub_eq_add_neg]

Result:
no goals
-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem fourierCoeff_liftIoc_eq {a : ℝ} (f : ℝ → ℂ) (n : ℤ) :
    fourierCoeff (AddCircle.liftIoc T a f) n =
    fourierCoeffOn (lt_add_of_pos_right a hT.out) f n

Proof state:
case e_a
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
x : ℝ
hx : x ∈ Ι a (a + T)
⊢ (fourier (-n)) ↑x • liftIoc T a f ↑x = (fourier (-n)) ↑x • f x

Tactic:
rw [liftIoc_coe_apply]

Result:
case e_a
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
x : ℝ
hx : x ∈ Ι a (a + T)
⊢ x ∈ Ioc a (a + T)

Proof state:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ (1 / T) • ∫ (x : ℝ) in ?a..?a + T, (fourier (-n)) ↑x • liftIoc T a f ↑x =
    (1 / T) • ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • f x

Tactic:
congr 1

Result:
case e_a
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ ∫ (x : ℝ) in ?a..?a + T, (fourier (-n)) ↑x • liftIoc T a f ↑x = ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • f x

Proof state:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ fourierCoeff (liftIoc T a f) n = fourierCoeffOn ⋯ f n

Tactic:
rw [fourierCoeffOn_eq_integral, fourierCoeff_eq_intervalIntegral, add_sub_cancel_left a T]

Result:
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ (1 / T) • ∫ (x : ℝ) in ?a..?a + T, (fourier (-n)) ↑x • liftIoc T a f ↑x =
    (1 / T) • ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • f x

case a
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ ℝ

Proof state:
case e_a
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
x : ℝ
hx : x ∈ Ι a (a + T)
⊢ x ∈ Ioc a (a + T)

Tactic:
rwa [uIoc_of_le (lt_add_of_pos_right a hT.out).le] at hx

Result:
no goals

Proof state:
case e_a
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
⊢ ∫ (x : ℝ) in ?a..?a + T, (fourier (-n)) ↑x • liftIoc T a f ↑x = ∫ (x : ℝ) in a..a + T, (fourier (-n)) ↑x • f x

Tactic:
refine intervalIntegral.integral_congr_ae (ae_of_all _ fun x hx => ?_)

Result:
case e_a
T : ℝ
hT : Fact (0 < T)
a : ℝ
f : ℝ → ℂ
n : ℤ
x : ℝ
hx : x ∈ Ι a (a + T)
⊢ (fourier (-n)) ↑x • liftIoc T a f ↑x = (fourier (-n)) ↑x • f x
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem IsBigOWith.right_le_add_of_lt_one {f₁ f₂ : α → E'} (h : IsBigOWith c l f₁ f₂) (hc : c < 1) :
    IsBigOWith (1 / (1 - c)) l f₂ fun x => f₁ x + f₂ x :=
  (h.neg_right.right_le_sub_of_lt_one hc).neg_right.of_neg_left.congr rfl (fun _ ↦ rfl) fun x ↦ by
    rw [neg_sub, sub_neg_eq_add]

Proof state:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
⊢ -(-f₂ x - f₁ x) = f₁ x + f₂ x

Tactic:
rw [neg_sub, sub_neg_eq_add]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arcsin_of_one_le {x : ℝ} (hx : 1 ≤ x) : arcsin x = π / 2

Proof state:
x : ℝ
hx : 1 ≤ x
⊢ arcsin x = π / 2

Tactic:
rw [← arcsin_projIcc, projIcc_of_right_le _ hx, Subtype.coe_mk, arcsin_one]

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
/-- A constructor for `PosSMulReflectLT` requiring you to prove `a • b₁ < a • b₂ → b₁ < b₂` only
when `0 < a` -/
lemma PosSMulReflectLT.of_pos (h₀ : ∀ a : α, 0 < a → ∀ b₁ b₂ : β, a • b₁ < a • b₂ → b₁ < b₂) :
    PosSMulReflectLT α β where
  elim a ha b₁ b₂ h

Proof state:
case inl
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), a • b₁ < a • b₂ → b₁ < b₂
a : α
ha✝ : 0 ≤ a
b₁ b₂ : β
h : a • b₁ < a • b₂
ha : 0 = a
⊢ b₁ < b₂

Tactic:
simp [← ha] at h

Result:
no goals

Proof state:
case inr
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), a • b₁ < a • b₂ → b₁ < b₂
a : α
ha✝ : 0 ≤ a
b₁ b₂ : β
h : a • b₁ < a • b₂
ha : 0 < a
⊢ b₁ < b₂

Tactic:
exact h₀ _ ha _ _ h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), a • b₁ < a • b₂ → b₁ < b₂
a : α
ha : 0 ≤ a
b₁ b₂ : β
h : a • b₁ < a • b₂
⊢ b₁ < b₂

Tactic:
obtain ha | ha := ha.eq_or_lt

Result:
case inl
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), a • b₁ < a • b₂ → b₁ < b₂
a : α
ha✝ : 0 ≤ a
b₁ b₂ : β
h : a • b₁ < a • b₂
ha : 0 = a
⊢ b₁ < b₂

case inr
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), a • b₁ < a • b₂ → b₁ < b₂
a : α
ha✝ : 0 ≤ a
b₁ b₂ : β
h : a • b₁ < a • b₂
ha : 0 < a
⊢ b₁ < b₂
-- Mathlib/FieldTheory/SplittingField/Construction.lean
theorem natDegree_removeFactor' {f : K[X]} {n : ℕ} (hfn : f.natDegree = n + 1) :
    f.removeFactor.natDegree = n

Proof state:
K : Type v
inst✝ : Field K
f : K[X]
n : ℕ
hfn : f.natDegree = n + 1
⊢ f.removeFactor.natDegree = n

Tactic:
rw [natDegree_removeFactor, hfn, n.add_sub_cancel]

Result:
no goals
-- Mathlib/LinearAlgebra/PerfectPairing/Basic.lean
theorem toDualLeft_of_toDualRight_symm (x : M) (f : Dual R M) :
    (p.toDualLeft x) (p.toDualRight.symm f) = f x

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
x : M
f : Dual R M
⊢ (p x) (p.toDualRight.symm f) = f x

Tactic:
exact apply_apply_toDualRight_symm p x f

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
x : M
f : Dual R M
⊢ (p.toDualLeft x) (p.toDualRight.symm f) = f x

Tactic:
rw [@toDualLeft_apply]

Result:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
x : M
f : Dual R M
⊢ (p x) (p.toDualRight.symm f) = f x