harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/ContinuousMap/Ideals.lean
theorem idealOfSet_isMaximal_iff (s : Opens X) :
    (idealOfSet 𝕜 (s : Set X)).IsMaximal ↔ IsCoatom s

Proof state:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Opens X
⊢ IsCoatom (idealOfSet 𝕜 ↑s) ↔ IsCoatom s

Tactic:
refine (idealOpensGI X 𝕜).isCoatom_iff (fun I hI => ?_) s

Result:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Opens X
I : Ideal C(X, 𝕜)
hI : IsCoatom I
⊢ idealOfSet 𝕜 ↑(opensOfIdeal I) = I

Proof state:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Opens X
⊢ (idealOfSet 𝕜 ↑s).IsMaximal ↔ IsCoatom s

Tactic:
rw [Ideal.isMaximal_def]

Result:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Opens X
⊢ IsCoatom (idealOfSet 𝕜 ↑s) ↔ IsCoatom s

Proof state:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Opens X
I : Ideal C(X, 𝕜)
hI : IsCoatom I
⊢ idealOfSet 𝕜 ↑(opensOfIdeal I) = I

Tactic:
rw [← Ideal.isMaximal_def] at hI

Result:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Opens X
I : Ideal C(X, 𝕜)
hI : I.IsMaximal
⊢ idealOfSet 𝕜 ↑(opensOfIdeal I) = I

Proof state:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
s : Opens X
I : Ideal C(X, 𝕜)
hI : I.IsMaximal
⊢ idealOfSet 𝕜 ↑(opensOfIdeal I) = I

Tactic:
exact idealOfSet_ofIdeal_isClosed inferInstance

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Roots.lean
theorem _root_.IsPrimitiveRoot.minpoly_dvd_cyclotomic {n : ℕ} {K : Type*} [Field K] {μ : K}
    (h : IsPrimitiveRoot μ n) (hpos : 0 < n) [CharZero K] : minpoly ℤ μ ∣ cyclotomic n ℤ

Proof state:
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst✝ : CharZero K
⊢ minpoly ℤ μ ∣ cyclotomic n ℤ

Tactic:
apply minpoly.isIntegrallyClosed_dvd (h.isIntegral hpos)

Result:
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst✝ : CharZero K
⊢ (aeval μ) (cyclotomic n ℤ) = 0

Proof state:
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst✝ : CharZero K
⊢ (aeval μ) (cyclotomic n ℤ) = 0

Tactic:
simpa [aeval_def, eval₂_eq_eval_map, IsRoot.def] using h.isRoot_cyclotomic hpos

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Ultra.lean
/-- All triangles are isosceles in an ultrametric normed group. -/
@[to_additive "All triangles are isosceles in an ultrametric normed additive group."]
lemma nnnorm_mul_eq_max_of_nnnorm_ne_nnnorm
    {x y : S} (h : ‖x‖₊ ≠ ‖y‖₊) : ‖x * y‖₊ = max ‖x‖₊ ‖y‖₊

Proof state:
S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x y : S
h : ‖x‖₊ ≠ ‖y‖₊
⊢ ‖x * y‖₊ = ‖x‖₊ ⊔ ‖y‖₊

Tactic:
simpa only [← NNReal.coe_inj, NNReal.coe_max] using
  norm_mul_eq_max_of_norm_ne_norm (NNReal.coe_injective.ne h)

Result:
no goals
-- Mathlib/Algebra/Algebra/Defs.lean
theorem right_comm (x : A) (r : R) (y : A) :
    x * algebraMap R A r * y = x * y * algebraMap R A r

Proof state:
R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
r : R
y : A
⊢ x * (algebraMap R A) r * y = x * y * (algebraMap R A) r

Tactic:
rw [mul_assoc, commutes, ← mul_assoc]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem iUnion_singleton_eq_range (f : α → β) : ⋃ x : α, {f x} = range f

Proof state:
α : Type u_1
β : Type u_2
f : α → β
⊢ ⋃ x, {f x} = range f

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
f : α → β
x : β
⊢ x ∈ ⋃ x, {f x} ↔ x ∈ range f

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → β
x : β
⊢ x ∈ ⋃ x, {f x} ↔ x ∈ range f

Tactic:
simp [@eq_comm _ x]

Result:
no goals
-- Mathlib/NumberTheory/Pell.lean
theorem sign_y_zpow_eq_sign_of_x_pos_of_y_pos {a : Solution₁ d} (hax : 0 < a.x) (hay : 0 < a.y)
    (n : ℤ) : (a ^ n).y.sign = n.sign

Proof state:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℤ
⊢ (a ^ n).y.sign = n.sign

Tactic:
rcases n with ((_ | n) | n)

Result:
case ofNat.zero
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
⊢ (a ^ Int.ofNat 0).y.sign = (Int.ofNat 0).sign

case ofNat.succ
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
⊢ (a ^ Int.ofNat (n + 1)).y.sign = (Int.ofNat (n + 1)).sign

case negSucc
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
⊢ (a ^ Int.negSucc n).y.sign = (Int.negSucc n).sign

Proof state:
case ofNat.succ
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
⊢ (a ^ (n + 1)).y.sign = (↑(n + 1)).sign

Tactic:
exact Int.sign_eq_one_of_pos (y_pow_succ_pos hax hay n)

Result:
no goals

Proof state:
case negSucc
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
⊢ (a ^ (n + 1))⁻¹.y.sign = (Int.negSucc n).sign

Tactic:
exact Int.sign_eq_neg_one_of_neg (neg_neg_of_pos (y_pow_succ_pos hax hay n))

Result:
no goals

Proof state:
case ofNat.zero
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
⊢ (a ^ Int.ofNat 0).y.sign = (Int.ofNat 0).sign

Tactic:
rfl

Result:
no goals

Proof state:
case ofNat.succ
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
⊢ (a ^ Int.ofNat (n + 1)).y.sign = (Int.ofNat (n + 1)).sign

Tactic:
rw [Int.ofNat_eq_coe, zpow_natCast]

Result:
case ofNat.succ
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
⊢ (a ^ (n + 1)).y.sign = (↑(n + 1)).sign

Proof state:
case negSucc
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
⊢ (a ^ Int.negSucc n).y.sign = (Int.negSucc n).sign

Tactic:
rw [zpow_negSucc]

Result:
case negSucc
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
⊢ (a ^ (n + 1))⁻¹.y.sign = (Int.negSucc n).sign
-- Mathlib/Topology/Gluing.lean
theorem ι_injective (i : D.J) : Function.Injective (𝖣.ι i)

Proof state:
D : GlueData
i : D.J
⊢ Function.Injective ⇑(ConcreteCategory.hom (D.ι i))

Tactic:
intro x y h

Result:
D : GlueData
i : D.J
x y : ↑(D.U i)
h : (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι i)) y
⊢ x = y

Proof state:
D : GlueData
i : D.J
x y : ↑(D.U i)
h : (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι i)) y
⊢ x = y

Tactic:
rcases (D.ι_eq_iff_rel _ _ _ _).mp h with ⟨_, e₁, e₂⟩

Result:
case intro.intro
D : GlueData
i : D.J
x y : ↑(D.U i)
h : (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι i)) y
w✝ : ↑(D.V (⟨i, x⟩.fst, ⟨i, y⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, x⟩.fst ⟨i, y⟩.fst)) w✝ = ⟨i, x⟩.snd
e₂ :
  (ConcreteCategory.hom (D.f ⟨i, y⟩.fst ⟨i, x⟩.fst)) ((ConcreteCategory.hom (D.t ⟨i, x⟩.fst ⟨i, y⟩.fst)) w✝) =
    ⟨i, y⟩.snd
⊢ x = y

Proof state:
case intro.intro
D : GlueData
i : D.J
x y : ↑(D.U i)
h : (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι i)) y
w✝ : ↑(D.V (⟨i, x⟩.fst, ⟨i, y⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, x⟩.fst ⟨i, y⟩.fst)) w✝ = ⟨i, x⟩.snd
e₂ :
  (ConcreteCategory.hom (D.f ⟨i, y⟩.fst ⟨i, x⟩.fst)) ((ConcreteCategory.hom (D.t ⟨i, x⟩.fst ⟨i, y⟩.fst)) w✝) =
    ⟨i, y⟩.snd
⊢ x = y

Tactic:
dsimp only at *

Result:
case intro.intro
D : GlueData
i : D.J
x y : ↑(D.U i)
h : (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι i)) y
w✝ : ↑(D.V (⟨i, x⟩.fst, ⟨i, y⟩.fst))
e₁ : (ConcreteCategory.hom (D.f i i)) w✝ = x
e₂ : (ConcreteCategory.hom (D.f i i)) ((ConcreteCategory.hom (D.t i i)) w✝) = y
⊢ x = y

Proof state:
case intro.intro
D : GlueData
i : D.J
x y : ↑(D.U i)
h : (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι i)) y
w✝ : ↑(D.V (⟨i, x⟩.fst, ⟨i, y⟩.fst))
e₁ : (ConcreteCategory.hom (D.f i i)) w✝ = x
e₂ : (ConcreteCategory.hom (D.f i i)) ((ConcreteCategory.hom (D.t i i)) w✝) = y
⊢ (ConcreteCategory.hom (D.f i i)) w✝ = (ConcreteCategory.hom (D.f i i)) ((ConcreteCategory.hom (D.t i i)) w✝)

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro
D : GlueData
i : D.J
x y : ↑(D.U i)
h : (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι i)) y
w✝ : ↑(D.V (⟨i, x⟩.fst, ⟨i, y⟩.fst))
e₁ : (ConcreteCategory.hom (D.f i i)) w✝ = x
e₂ : (ConcreteCategory.hom (D.f i i)) ((ConcreteCategory.hom (D.t i i)) w✝) = y
⊢ x = y

Tactic:
rw [← e₁, ← e₂]

Result:
case intro.intro
D : GlueData
i : D.J
x y : ↑(D.U i)
h : (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι i)) y
w✝ : ↑(D.V (⟨i, x⟩.fst, ⟨i, y⟩.fst))
e₁ : (ConcreteCategory.hom (D.f i i)) w✝ = x
e₂ : (ConcreteCategory.hom (D.f i i)) ((ConcreteCategory.hom (D.t i i)) w✝) = y
⊢ (ConcreteCategory.hom (D.f i i)) w✝ = (ConcreteCategory.hom (D.f i i)) ((ConcreteCategory.hom (D.t i i)) w✝)
-- Mathlib/Data/Rat/Cast/Order.lean
theorem cast_lt_natCast {m : ℚ} {n : ℕ} : (m : K) < n ↔ m < (n : ℚ)

Proof state:
K : Type u_5
inst✝ : LinearOrderedField K
m : ℚ
n : ℕ
⊢ ↑m < ↑n ↔ m < ↑n

Tactic:
rw [← cast_lt (K := K), cast_natCast]

Result:
no goals
-- Mathlib/Data/Fintype/Basic.lean
theorem map_univ_val_equiv (e : α ≃ β) :
    map e univ.val = univ.val

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
e : α ≃ β
⊢ map (⇑e) univ.val = univ.val

Tactic:
rw [← congr_arg Finset.val (Finset.map_univ_equiv e), Finset.map_val, Equiv.coe_toEmbedding]

Result:
no goals
-- Mathlib/CategoryTheory/Iso.lean
lemma Iso.isIso_hom (e : X ≅ Y) : IsIso e.hom :=
  ⟨e.inv, by simp, by simp⟩

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
⊢ e.inv ≫ e.hom = 𝟙 Y

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
⊢ e.hom ≫ e.inv = 𝟙 X

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Closed/Monoidal.lean
theorem uncurry_pre (f : B ⟶ A) (X : C) :
    MonoidalClosed.uncurry ((pre f).app X) = f ▷ _ ≫ (ihom.ev A).app X

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
A B : C
inst✝¹ : Closed A
inst✝ : Closed B
f : B ⟶ A
X : C
⊢ uncurry ((pre f).app X) = f ▷ (ihom A).obj X ≫ (ihom.ev A).app X

Tactic:
simp [uncurry_eq]

Result:
no goals
-- Mathlib/Data/Complex/Module.lean
theorem algHom_ext ⦃f g : ℂ →ₐ[ℝ] A⦄ (h : f I = g I) : f = g

Proof state:
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra ℝ A
f g : ℂ →ₐ[ℝ] A
h : f I = g I
⊢ f = g

Tactic:
ext ⟨x, y⟩

Result:
case H.mk
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra ℝ A
f g : ℂ →ₐ[ℝ] A
h : f I = g I
x y : ℝ
⊢ f { re := x, im := y } = g { re := x, im := y }

Proof state:
case H.mk
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra ℝ A
f g : ℂ →ₐ[ℝ] A
h : f I = g I
x y : ℝ
⊢ f { re := x, im := y } = g { re := x, im := y }

Tactic:
simp only [mk_eq_add_mul_I, map_add, AlgHom.map_coe_real_complex, map_mul, h]

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem exists_nhds_ne_neBot (X : Type*) [TopologicalSpace X] [CompactSpace X] [Infinite X] :
    ∃ z : X, (𝓝[≠] z).NeBot

Proof state:
X : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : Infinite X
⊢ ∃ z, (𝓝[≠] z).NeBot

Tactic:
simpa [AccPt] using (@infinite_univ X _).exists_accPt_principal

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem HasFDerivAt.cpow (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x)
    (h0 : f x ∈ slitPlane) : HasFDerivAt (fun x => f x ^ g x)
      ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
f' g' : E →L[ℂ] ℂ
x : E
hf : HasFDerivAt f f' x
hg : HasFDerivAt g g' x
h0 : f x ∈ slitPlane
⊢ HasFDerivAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') x

Tactic:
convert (@Complex.hasFDerivAt_cpow ((fun x => (f x, g x)) x) h0).comp x (hf.prod hg)

Result:
no goals
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem natSepDegree_zero : (0 : F[X]).natSepDegree = 0

Proof state:
F : Type u
inst✝ : Field F
⊢ natSepDegree 0 = 0

Tactic:
rw [← C_0, natSepDegree_C]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
theorem div_def (x y : ℤ[i]) :
    x / y = ⟨round ((x * star y).re / norm y : ℚ), round ((x * star y).im / norm y : ℚ)⟩ :=
  show Zsqrtd.mk _ _ = _ by simp [div_eq_mul_inv]

Proof state:
x y : ℤ[i]
⊢ { re := round (↑(x * star y).re * (↑(norm y))⁻¹), im := round (↑(x * star y).im * (↑(norm y))⁻¹) } =
    { re := round (↑(x * star y).re / ↑(norm y)), im := round (↑(x * star y).im / ↑(norm y)) }

Tactic:
simp [div_eq_mul_inv]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem Associated.mul_left [Monoid M] (a : M) {b c : M} (h : b ~ᵤ c) : a * b ~ᵤ a * c

Proof state:
M : Type u_1
inst✝ : Monoid M
a b c : M
h : b ~ᵤ c
⊢ a * b ~ᵤ a * c

Tactic:
obtain ⟨d, rfl⟩ := h

Result:
case intro
M : Type u_1
inst✝ : Monoid M
a b : M
d : Mˣ
⊢ a * b ~ᵤ a * (b * ↑d)

Proof state:
case intro
M : Type u_1
inst✝ : Monoid M
a b : M
d : Mˣ
⊢ a * b ~ᵤ a * (b * ↑d)

Tactic:
exact ⟨d, mul_assoc _ _ _⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem umod_self {x : BitVec w} : x % x = 0#w

Proof state:
w : Nat
x : BitVec w
⊢ x % x = 0#w

Tactic:
simp [bv_toNat]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {v : β} :
    get? (m.insertIfNew k v) a = if k == a ∧ m.contains k = false then some v else get? m a

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k a : α
v : β
⊢ get? (m.insertIfNew k v) a = if (k == a) = true ∧ m.contains k = false then some v else get? m a

Tactic:
simp_to_model [insertIfNew] using List.getValue?_insertEntryIfNew

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean
theorem eLpNorm_add_lt_top {f g : α → E} (hf : MemLp f p μ) (hg : MemLp g p μ) :
    eLpNorm (f + g) p μ < ∞ :=
  calc
    eLpNorm (f + g) p μ ≤ LpAddConst p * (eLpNorm f p μ + eLpNorm g p μ) :=
      eLpNorm_add_le' hf.aestronglyMeasurable hg.aestronglyMeasurable p
    _ < ∞

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : α → E
hf : MemLp f p μ
hg : MemLp g p μ
⊢ eLpNorm f p μ + eLpNorm g p μ < ⊤

Tactic:
exact ENNReal.add_lt_top.2 ⟨hf.2, hg.2⟩

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : α → E
hf : MemLp f p μ
hg : MemLp g p μ
⊢ LpAddConst p * (eLpNorm f p μ + eLpNorm g p μ) < ⊤

Tactic:
apply ENNReal.mul_lt_top (LpAddConst_lt_top p)

Result:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : α → E
hf : MemLp f p μ
hg : MemLp g p μ
⊢ eLpNorm f p μ + eLpNorm g p μ < ⊤
-- Mathlib/FieldTheory/Finite/Polynomial.lean
theorem range_evalᵢ [Finite σ] : range (evalᵢ σ K) = ⊤

Proof state:
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
⊢ Submodule.map (evalₗ K σ) (restrictDegree σ K (Fintype.card K - 1)) = ⊤

Tactic:
exact map_restrict_dom_evalₗ K σ

Result:
no goals

Proof state:
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
⊢ range (evalᵢ σ K) = ⊤

Tactic:
rw [evalᵢ, LinearMap.range_comp, range_subtype]

Result:
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
⊢ Submodule.map (evalₗ K σ) (restrictDegree σ K (Fintype.card K - 1)) = ⊤
-- Mathlib/ModelTheory/Basic.lean
theorem toHom_comp_injective (h : N ↪[L] P) :
    Function.Injective (h.toHom.comp : (M →[L] N) →  (M →[L] P))

Proof state:
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : N ↪[L] P
f g : M →[L] N
hfg : h.toHom.comp f = h.toHom.comp g
⊢ f = g

Tactic:
ext x

Result:
case h
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : N ↪[L] P
f g : M →[L] N
hfg : h.toHom.comp f = h.toHom.comp g
x : M
⊢ f x = g x

Proof state:
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : N ↪[L] P
⊢ Function.Injective h.toHom.comp

Tactic:
intro f g hfg

Result:
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : N ↪[L] P
f g : M →[L] N
hfg : h.toHom.comp f = h.toHom.comp g
⊢ f = g

Proof state:
case h
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : N ↪[L] P
f g : M →[L] N
hfg : h.toHom.comp f = h.toHom.comp g
x : M
⊢ f x = g x

Tactic:
exact h.injective (DFunLike.congr_fun hfg x)

Result:
no goals
-- Mathlib/Analysis/Convex/Gauge.lean
theorem gauge_pos (hs : Absorbent ℝ s) (hb : Bornology.IsVonNBounded ℝ s) :
    0 < gauge s x ↔ x ≠ 0

Proof state:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
x : E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
hs : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
⊢ 0 < gauge s x ↔ x ≠ 0

Tactic:
simp only [(gauge_nonneg _).gt_iff_ne, Ne, gauge_eq_zero hs hb]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Triangle.lean
theorem angle_sub_eq_angle_sub_rev_of_norm_eq {x y : V} (h : ‖x‖ = ‖y‖) :
    angle x (x - y) = angle y (y - x)

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ‖x‖ = ‖y‖
⊢ Real.cos (angle x (x - y)) = Real.cos (angle y (y - x))

Tactic:
rw [cos_angle, cos_angle, h, ← neg_sub, norm_neg, neg_sub, inner_sub_right, inner_sub_right,
  real_inner_self_eq_norm_mul_norm, real_inner_self_eq_norm_mul_norm, h, real_inner_comm x y]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ‖x‖ = ‖y‖
⊢ angle x (x - y) = angle y (y - x)

Tactic:
refine Real.injOn_cos ⟨angle_nonneg _ _, angle_le_pi _ _⟩ ⟨angle_nonneg _ _, angle_le_pi _ _⟩ ?_

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ‖x‖ = ‖y‖
⊢ Real.cos (angle x (x - y)) = Real.cos (angle y (y - x))
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma map_ψ (n : ℤ) : (W.map f).ψ n = (W.ψ n).map (mapRingHom f)

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ (W.map f).ψ n = Polynomial.map (mapRingHom f) (W.ψ n)

Tactic:
simp only [ψ, map_ψ₂, map_Ψ₃, map_preΨ₄, ← coe_mapRingHom, map_normEDS]

Result:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ normEDS ((mapRingHom (mapRingHom f)) W.ψ₂) (C ((mapRingHom f) W.Ψ₃)) (C ((mapRingHom f) W.preΨ₄)) n =
    normEDS ((mapRingHom (mapRingHom f)) W.ψ₂) ((mapRingHom (mapRingHom f)) (C W.Ψ₃))
      ((mapRingHom (mapRingHom f)) (C W.preΨ₄)) n

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ normEDS ((mapRingHom (mapRingHom f)) W.ψ₂) (C ((mapRingHom f) W.Ψ₃)) (C ((mapRingHom f) W.preΨ₄)) n =
    normEDS ((mapRingHom (mapRingHom f)) W.ψ₂) ((mapRingHom (mapRingHom f)) (C W.Ψ₃))
      ((mapRingHom (mapRingHom f)) (C W.preΨ₄)) n

Tactic:
map_simp

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem semiconj₂_conj : Semiconj₂ e f (e.arrowCongr e.conj f) := fun x y => by simp [arrowCongr]

Proof state:
α₁ : Type u_9
β₁ : Type u_10
e : α₁ ≃ β₁
f : α₁ → α₁ → α₁
x y : α₁
⊢ e (f x y) = (e.arrowCongr e.conj) f (e x) (e y)

Tactic:
simp [arrowCongr]

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Reflective.lean
theorem Functor.essImage.unit_isIso [Reflective i] {A : C} (h : i.essImage A) :
    IsIso ((reflectorAdjunction i).unit.app A)

Proof state:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
i : D ⥤ C
inst✝ : Reflective i
A : C
h : i.essImage A
⊢ IsIso ((reflectorAdjunction i).unit.app A)

Tactic:
rwa [isIso_unit_app_iff_mem_essImage]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/LDL.lean
theorem LDL.lowerInv_triangular {i j : n} (hij : i < j) : LDL.lowerInv hS i j = 0

Proof state:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : WellFoundedLT n
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
i j : n
hij : i < j
⊢ lowerInv hS i j = 0

Tactic:
rw [←
  @gramSchmidt_triangular 𝕜 (n → 𝕜) _ (_ :) (InnerProductSpace.ofMatrix hS.transpose) n _ _ _
    i j hij (Pi.basisFun 𝕜 n),
  Pi.basisFun_repr, LDL.lowerInv]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean
theorem eval_comp
    {η η' : f ⟶ g} {θ θ' : g ⟶ h} {ι : f ⟶ h}
    (e_η : η = η') (e_θ : θ = θ') (e_ηθ : η' ≫ θ' = ι) :
    η ≫ θ = ι

Proof state:
C : Type u
inst✝ : Category.{v, u} C
f g h : C
η η' : f ⟶ g
θ θ' : g ⟶ h
ι : f ⟶ h
e_η : η = η'
e_θ : θ = θ'
e_ηθ : η' ≫ θ' = ι
⊢ η ≫ θ = ι

Tactic:
simp [e_η, e_θ, e_ηθ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem beq_self_eq_true' [DecidableEq α] (a : α) : (a == a) = true

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
⊢ (a == a) = true

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/Bifunctor.lean
@[reassoc (attr := simp)]
lemma ι_D₂ :
    ιMapBifunctor K₁ K₂ F c i₁ i₂ j h ≫ D₂ K₁ K₂ F c j j' = d₂ K₁ K₂ F c i₁ i₂ j'

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝¹⁰ : Category.{u_9, u_1} C₁
inst✝⁹ : Category.{u_8, u_2} C₂
inst✝⁸ : Category.{u_7, u_3} D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst✝⁷ : HasZeroMorphisms C₁
inst✝⁶ : HasZeroMorphisms C₂
inst✝⁵ : Preadditive D
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
c : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : DecidableEq J
j j' : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
⊢ K₁.ιMapBifunctor K₂ F c i₁ i₂ j h ≫ D₂ K₁ K₂ F c j j' = d₂ K₁ K₂ F c i₁ i₂ j'

Tactic:
apply HomologicalComplex₂.ι_D₂

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ico_union_right (hab : a ≤ b) : Ico a b ∪ {b} = Icc a b

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b : α
hab : a ≤ b
⊢ Ico a b ∪ {b} = Icc a b

Tactic:
simpa only [dual_Ioc, dual_Icc] using Ioc_union_left hab.dual

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_neg_iff (h : 0 < x) : logb b x < 0 ↔ x < 1

Proof state:
b x : ℝ
hb : 1 < b
h : 0 < x
⊢ logb b x < logb ?m.19457 1 ↔ x < 1

b x : ℝ
hb : 1 < b
h : 0 < x
⊢ ℝ

Tactic:
exact logb_lt_logb_iff hb h zero_lt_one

Result:
no goals

Proof state:
b x : ℝ
hb : 1 < b
h : 0 < x
⊢ logb b x < 0 ↔ x < 1

Tactic:
rw [← logb_one]

Result:
b x : ℝ
hb : 1 < b
h : 0 < x
⊢ logb b x < logb ?m.19457 1 ↔ x < 1

b x : ℝ
hb : 1 < b
h : 0 < x
⊢ ℝ
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem sum_multiset_singleton (s : Finset α) : ∑ a ∈ s, {a} = s.val

Proof state:
α : Type u_3
s : Finset α
⊢ ∑ a ∈ s, {a} = s.val

Tactic:
simp only [sum_eq_multiset_sum, Multiset.sum_map_singleton]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isBigOWith_principal {s : Set α} : IsBigOWith c (𝓟 s) f g ↔ ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c : ℝ
f : α → E
g : α → F
s : Set α
⊢ IsBigOWith c (𝓟 s) f g ↔ ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖

Tactic:
rw [IsBigOWith_def, eventually_principal]

Result:
no goals