harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Order/IntermediateValue.lean
theorem IsPreconnected.intermediate_value₂_eventually₂ {s : Set X} (hs : IsPreconnected s)
    {l₁ l₂ : Filter X} [NeBot l₁] [NeBot l₂] (hl₁ : l₁ ≤ 𝓟 s) (hl₂ : l₂ ≤ 𝓟 s) {f g : X → α}
    (hf : ContinuousOn f s) (hg : ContinuousOn g s) (he₁ : f ≤ᶠ[l₁] g) (he₂ : g ≤ᶠ[l₂] f) :
    ∃ x ∈ s, f x = g x

Proof state:
X : Type u
α : Type v
inst✝⁵ : TopologicalSpace X
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
l₁ l₂ : Filter X
inst✝¹ : l₁.NeBot
inst✝ : l₂.NeBot
hl₁ : l₁ ≤ 𝓟 s
hl₂ : l₂ ≤ 𝓟 s
f g : X → α
hf : Continuous (s.restrict f)
hg : Continuous (s.restrict g)
he₁ : f ≤ᶠ[l₁] g
he₂ : g ≤ᶠ[l₂] f
⊢ ∃ x ∈ s, f x = g x

Tactic:
obtain ⟨b, h⟩ :=
  @intermediate_value_univ₂_eventually₂ _ _ _ _ _ _ (Subtype.preconnectedSpace hs) _ _
    (comap_coe_neBot_of_le_principal hl₁) (comap_coe_neBot_of_le_principal hl₂) _ _ hf hg
    (he₁.comap _) (he₂.comap _)

Result:
case intro
X : Type u
α : Type v
inst✝⁵ : TopologicalSpace X
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
l₁ l₂ : Filter X
inst✝¹ : l₁.NeBot
inst✝ : l₂.NeBot
hl₁ : l₁ ≤ 𝓟 s
hl₂ : l₂ ≤ 𝓟 s
f g : X → α
hf : Continuous (s.restrict f)
hg : Continuous (s.restrict g)
he₁ : f ≤ᶠ[l₁] g
he₂ : g ≤ᶠ[l₂] f
b : ↑s
h : s.restrict f b = s.restrict g b
⊢ ∃ x ∈ s, f x = g x

Proof state:
case intro
X : Type u
α : Type v
inst✝⁵ : TopologicalSpace X
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
l₁ l₂ : Filter X
inst✝¹ : l₁.NeBot
inst✝ : l₂.NeBot
hl₁ : l₁ ≤ 𝓟 s
hl₂ : l₂ ≤ 𝓟 s
f g : X → α
hf : Continuous (s.restrict f)
hg : Continuous (s.restrict g)
he₁ : f ≤ᶠ[l₁] g
he₂ : g ≤ᶠ[l₂] f
b : ↑s
h : s.restrict f b = s.restrict g b
⊢ ∃ x ∈ s, f x = g x

Tactic:
exact ⟨b, b.prop, h⟩

Result:
no goals

Proof state:
X : Type u
α : Type v
inst✝⁵ : TopologicalSpace X
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
l₁ l₂ : Filter X
inst✝¹ : l₁.NeBot
inst✝ : l₂.NeBot
hl₁ : l₁ ≤ 𝓟 s
hl₂ : l₂ ≤ 𝓟 s
f g : X → α
hf : ContinuousOn f s
hg : ContinuousOn g s
he₁ : f ≤ᶠ[l₁] g
he₂ : g ≤ᶠ[l₂] f
⊢ ∃ x ∈ s, f x = g x

Tactic:
rw [continuousOn_iff_continuous_restrict] at hf hg

Result:
X : Type u
α : Type v
inst✝⁵ : TopologicalSpace X
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
l₁ l₂ : Filter X
inst✝¹ : l₁.NeBot
inst✝ : l₂.NeBot
hl₁ : l₁ ≤ 𝓟 s
hl₂ : l₂ ≤ 𝓟 s
f g : X → α
hf : Continuous (s.restrict f)
hg : Continuous (s.restrict g)
he₁ : f ≤ᶠ[l₁] g
he₂ : g ≤ᶠ[l₂] f
⊢ ∃ x ∈ s, f x = g x
-- Mathlib/RingTheory/Nilpotent/Exp.lean
theorem exp_add_of_commute {a b : A} (h₁ : Commute a b) (h₂ : IsNilpotent a) (h₃ : IsNilpotent b) :
    exp (a + b) = exp a * exp b

Proof state:
case calc_1
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := n₁ ⊔ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
⊢ ∑ i ∈ R2N, (↑i !)⁻¹ • (a + b) ^ i = ∑ i ∈ R2N, (↑i !)⁻¹ • ∑ j ∈ range (i + 1), a ^ j * b ^ (i - j) * ↑(i.choose j)

Tactic:
refine sum_congr rfl fun i _ ↦ ?_

Result:
case calc_1
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a b : A
h₁ : Commute a b
n₁ : ℕ
hn₁ : a ^ n₁ = 0
n₂ : ℕ
hn₂ : b ^ n₂ = 0
N : ℕ := n₁ ⊔ n₂
h₄ : a ^ (N + 1) = 0
h₅ : b ^ (N + 1) = 0
R2N : Finset ℕ := range (2 * N + 1)
hR2N : R2N = range (2 * N + 1)
RN : Finset ℕ := range (N + 1)
hRN : RN = range (N + 1)
i : ℕ
x✝ : i ∈ R2N
⊢ (↑i !)⁻¹ • (a + b) ^ i = (↑i !)⁻¹ • ∑ j ∈ range (i + 1), a ^ j * b ^ (i - j) * ↑(i.choose j)
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem log_one : log 1 = 0

Proof state:
⊢ log 1 = 0

Tactic:
simp [log]

Result:
no goals
-- Mathlib/Order/SupClosed.lean
lemma InfClosed.insert_upperBounds {s : Set α} {a : α} (hs : InfClosed s) (ha : a ∈ upperBounds s) :
    InfClosed (insert a s)

Proof state:
α : Type u_3
inst✝ : SemilatticeInf α
s : Set α
a : α
hs : InfClosed s
ha : a ∈ upperBounds s
⊢ InfClosed (insert a s)

Tactic:
rw [InfClosed]

Result:
α : Type u_3
inst✝ : SemilatticeInf α
s : Set α
a : α
hs : InfClosed s
ha : a ∈ upperBounds s
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ insert a s → ∀ ⦃b : α⦄, b ∈ insert a s → a_1 ⊓ b ∈ insert a s

Proof state:
α : Type u_3
inst✝ : SemilatticeInf α
s : Set α
a : α
hs : InfClosed s
ha : a ∈ upperBounds s
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ insert a s → ∀ ⦃b : α⦄, b ∈ insert a s → a_1 ⊓ b ∈ insert a s

Tactic:
have ha' : ∀ b ∈ s, b ≤ a := fun _ a ↦ ha a

Result:
α : Type u_3
inst✝ : SemilatticeInf α
s : Set α
a : α
hs : InfClosed s
ha : a ∈ upperBounds s
ha' : ∀ b ∈ s, b ≤ a
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ insert a s → ∀ ⦃b : α⦄, b ∈ insert a s → a_1 ⊓ b ∈ insert a s

Proof state:
α : Type u_3
inst✝ : SemilatticeInf α
s : Set α
a : α
hs : InfClosed s
ha : a ∈ upperBounds s
ha' : ∀ b ∈ s, b ≤ a
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ insert a s → ∀ ⦃b : α⦄, b ∈ insert a s → a_1 ⊓ b ∈ insert a s

Tactic:
aesop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Equal.lean
theorem BitVec.eq_neg_add_iff_add_eq (a b c : BitVec w) : (a == (~~~b + 1#w) + c) = (a + b == c)

Proof state:
w : Nat
a b c : BitVec w
⊢ (a == ~~~b + 1#w + c) = (a + b == c)

Tactic:
rw [BitVec.add_comm]

Result:
w : Nat
a b c : BitVec w
⊢ (a == c + (~~~b + 1#w)) = (a + b == c)

Proof state:
w : Nat
a b c : BitVec w
⊢ (a == c + (~~~b + 1#w)) = (a + b == c)

Tactic:
exact BitVec.eq_sub_iff_add_eq _ _ _

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem sup_mul_eq_of_coprime_left (h : I ⊔ J = ⊤) : I ⊔ J * K = I ⊔ K :=
  le_antisymm (sup_le_sup_left mul_le_left _) fun i hi => by
    rw [eq_top_iff_one] at h; rw [Submodule.mem_sup] at h hi ⊢
    obtain ⟨i1, hi1, j, hj, h⟩ := h; obtain ⟨i', hi', k, hk, hi⟩ := hi
    refine ⟨_, add_mem hi' (mul_mem_right k _ hi1), _, mul_mem_mul hj hk, ?_⟩
    rw [add_assoc, ← add_mul, h, one_mul, hi]

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommSemiring R
I J K : Ideal R
i i1 : R
hi1 : i1 ∈ I
j : R
hj : j ∈ J
h : i1 + j = 1
i' : R
hi' : i' ∈ I
k : R
hk : k ∈ K
hi : i' + k = i
⊢ i' + i1 * k + j * k = i

Tactic:
rw [add_assoc, ← add_mul, h, one_mul, hi]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
I J K : Ideal R
h : ∃ y ∈ I, ∃ z ∈ J, y + z = 1
i : R
hi : ∃ y ∈ I, ∃ z ∈ K, y + z = i
⊢ ∃ y ∈ I, ∃ z ∈ J * K, y + z = i

Tactic:
obtain ⟨i1, hi1, j, hj, h⟩ := h

Result:
case intro.intro.intro.intro
R : Type u
inst✝ : CommSemiring R
I J K : Ideal R
i : R
hi : ∃ y ∈ I, ∃ z ∈ K, y + z = i
i1 : R
hi1 : i1 ∈ I
j : R
hj : j ∈ J
h : i1 + j = 1
⊢ ∃ y ∈ I, ∃ z ∈ J * K, y + z = i

Proof state:
R : Type u
inst✝ : CommSemiring R
I J K : Ideal R
h : I ⊔ J = ⊤
i : R
hi : i ∈ I ⊔ K
⊢ i ∈ I ⊔ J * K

Tactic:
rw [eq_top_iff_one] at h

Result:
R : Type u
inst✝ : CommSemiring R
I J K : Ideal R
h : 1 ∈ I ⊔ J
i : R
hi : i ∈ I ⊔ K
⊢ i ∈ I ⊔ J * K

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommSemiring R
I J K : Ideal R
i i1 : R
hi1 : i1 ∈ I
j : R
hj : j ∈ J
h : i1 + j = 1
i' : R
hi' : i' ∈ I
k : R
hk : k ∈ K
hi : i' + k = i
⊢ ∃ y ∈ I, ∃ z ∈ J * K, y + z = i

Tactic:
refine ⟨_, add_mem hi' (mul_mem_right k _ hi1), _, mul_mem_mul hj hk, ?_⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommSemiring R
I J K : Ideal R
i i1 : R
hi1 : i1 ∈ I
j : R
hj : j ∈ J
h : i1 + j = 1
i' : R
hi' : i' ∈ I
k : R
hk : k ∈ K
hi : i' + k = i
⊢ i' + i1 * k + j * k = i

Proof state:
case intro.intro.intro.intro
R : Type u
inst✝ : CommSemiring R
I J K : Ideal R
i : R
hi : ∃ y ∈ I, ∃ z ∈ K, y + z = i
i1 : R
hi1 : i1 ∈ I
j : R
hj : j ∈ J
h : i1 + j = 1
⊢ ∃ y ∈ I, ∃ z ∈ J * K, y + z = i

Tactic:
obtain ⟨i', hi', k, hk, hi⟩ := hi

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommSemiring R
I J K : Ideal R
i i1 : R
hi1 : i1 ∈ I
j : R
hj : j ∈ J
h : i1 + j = 1
i' : R
hi' : i' ∈ I
k : R
hk : k ∈ K
hi : i' + k = i
⊢ ∃ y ∈ I, ∃ z ∈ J * K, y + z = i

Proof state:
R : Type u
inst✝ : CommSemiring R
I J K : Ideal R
h : 1 ∈ I ⊔ J
i : R
hi : i ∈ I ⊔ K
⊢ i ∈ I ⊔ J * K

Tactic:
rw [Submodule.mem_sup] at h hi ⊢

Result:
R : Type u
inst✝ : CommSemiring R
I J K : Ideal R
h : ∃ y ∈ I, ∃ z ∈ J, y + z = 1
i : R
hi : ∃ y ∈ I, ∃ z ∈ K, y + z = i
⊢ ∃ y ∈ I, ∃ z ∈ J * K, y + z = i
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem mod_right (a : ℤ) {b : ℕ} (hb : Odd b) : J(a | b) = J(a | b % (4 * a.natAbs))

Proof state:
a : ℤ
b : ℕ
hb : Odd b
⊢ J(a | b) = J(a | b % (4 * a.natAbs))

Tactic:
rcases Int.natAbs_eq a with ha | ha <;> nth_rw 2 [ha] <;> nth_rw 1 [ha]

Result:
case inl
a : ℤ
b : ℕ
hb : Odd b
ha : a = ↑a.natAbs
⊢ J(↑a.natAbs | b) = J(↑a.natAbs | b % (4 * a.natAbs))

case inr
a : ℤ
b : ℕ
hb : Odd b
ha : a = -↑a.natAbs
⊢ J(-↑a.natAbs | b) = J(-↑a.natAbs | b % (4 * a.natAbs))

Proof state:
a : ℤ
b : ℕ
hb : Odd b
ha : a = -↑a.natAbs
⊢ Even 4

Tactic:
decide

Result:
no goals

Proof state:
case inl
a : ℤ
b : ℕ
hb : Odd b
ha : a = ↑a.natAbs
⊢ J(↑a.natAbs | b) = J(↑a.natAbs | b % (4 * a.natAbs))

Tactic:
exact mod_right' a.natAbs hb

Result:
no goals

Proof state:
case inr
a : ℤ
b : ℕ
hb : Odd b
ha : a = -↑a.natAbs
hb' : Odd (b % (4 * a.natAbs))
⊢ J(-↑a.natAbs | b) = J(-↑a.natAbs | b % (4 * a.natAbs))

Tactic:
rw [jacobiSym.neg _ hb, jacobiSym.neg _ hb', mod_right' _ hb, χ₄_nat_mod_four,
  χ₄_nat_mod_four (b % (4 * _)), mod_mod_of_dvd b (dvd_mul_right 4 _)]

Result:
no goals

Proof state:
case inr
a : ℤ
b : ℕ
hb : Odd b
ha : a = -↑a.natAbs
⊢ J(-↑a.natAbs | b) = J(-↑a.natAbs | b % (4 * a.natAbs))

Tactic:
have hb' : Odd (b % (4 * a.natAbs)) := hb.mod_even (Even.mul_right (by decide) _)

Result:
case inr
a : ℤ
b : ℕ
hb : Odd b
ha : a = -↑a.natAbs
hb' : Odd (b % (4 * a.natAbs))
⊢ J(-↑a.natAbs | b) = J(-↑a.natAbs | b % (4 * a.natAbs))
-- Mathlib/Data/Set/Subset.lean
lemma eq_of_preimage_val_eq_of_subset (hB : B ⊆ A) (hC : C ⊆ A) (h : A ↓∩ B = A ↓∩ C) : B = C

Proof state:
α : Type u_2
A B C : Set α
hB : A ∩ B = B
hC : A ∩ C = C
h : B = C
⊢ B = C

Tactic:
exact h

Result:
no goals

Proof state:
α : Type u_2
A B C : Set α
hB : B ⊆ A
hC : C ⊆ A
h : A ↓∩ B = A ↓∩ C
⊢ B = C

Tactic:
simp only [← inter_eq_right] at hB hC

Result:
α : Type u_2
A B C : Set α
h : A ↓∩ B = A ↓∩ C
hB : A ∩ B = B
hC : A ∩ C = C
⊢ B = C

Proof state:
α : Type u_2
A B C : Set α
h : A ↓∩ B = A ↓∩ C
hB : A ∩ B = B
hC : A ∩ C = C
⊢ B = C

Tactic:
simp only [Subtype.preimage_val_eq_preimage_val_iff, hB, hC] at h

Result:
α : Type u_2
A B C : Set α
hB : A ∩ B = B
hC : A ∩ C = C
h : B = C
⊢ B = C
-- Mathlib/Topology/Compactness/Compact.lean
lemma Pi.isCompact_iff_of_isClosed {s : Set (Π i, X i)} (hs : IsClosed s) :
    IsCompact s ↔ ∀ i, IsCompact (eval i '' s)

Proof state:
case mp
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
hs : IsClosed s
H : IsCompact s
⊢ ∀ (i : ι), IsCompact (eval i '' s)

Tactic:
exact fun i ↦ H.image <| continuous_apply i

Result:
no goals

Proof state:
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
hs : IsClosed s
⊢ IsCompact s ↔ ∀ (i : ι), IsCompact (eval i '' s)

Tactic:
constructor <;> intro H

Result:
case mp
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
hs : IsClosed s
H : IsCompact s
⊢ ∀ (i : ι), IsCompact (eval i '' s)

case mpr
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
hs : IsClosed s
H : ∀ (i : ι), IsCompact (eval i '' s)
⊢ IsCompact s

Proof state:
case mpr
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
hs : IsClosed s
H : ∀ (i : ι), IsCompact (eval i '' s)
⊢ IsCompact s

Tactic:
exact IsCompact.of_isClosed_subset (isCompact_univ_pi H) hs (subset_pi_eval_image univ s)

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
lemma mul_lt_floor (hb₀ : 0 < b) (hb : b < 1) (hba : ⌈b / (1 - b)⌉ ≤ a) : b * a < ⌊a⌋

Proof state:
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a b : k
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉ ≤ a
⊢ b * (↑⌊a⌋ + 1) ≤ ↑⌊a⌋

Tactic:
rwa [_root_.mul_add_one, ← le_sub_iff_add_le', ← one_sub_mul, ← div_le_iff₀' (by linarith),
  ← ceil_le, le_floor]

Result:
no goals

Proof state:
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a b : k
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉ ≤ a
⊢ 0 < 1 - b

Tactic:
linarith

Result:
no goals

Proof state:
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a b : k
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉ ≤ a
⊢ b * a < ↑⌊a⌋

Tactic:
calc
  b * a < b * (⌊a⌋ + 1) := by gcongr; exacts [hb₀, lt_floor_add_one _]
  _ ≤ ⌊a⌋ := by
    rwa [_root_.mul_add_one, ← le_sub_iff_add_le', ← one_sub_mul, ← div_le_iff₀' (by linarith),
      ← ceil_le, le_floor]

Result:
no goals

Proof state:
case a0
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a b : k
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉ ≤ a
⊢ 0 < b

case bc
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a b : k
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉ ≤ a
⊢ a < ↑⌊a⌋ + 1

Tactic:
exacts [hb₀, lt_floor_add_one _]

Result:
no goals

Proof state:
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a b : k
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉ ≤ a
⊢ b * a < b * (↑⌊a⌋ + 1)

Tactic:
gcongr

Result:
case a0
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a b : k
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉ ≤ a
⊢ 0 < b

case bc
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a b : k
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉ ≤ a
⊢ a < ↑⌊a⌋ + 1
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem subalgebra_top_finrank_eq_submodule_top_finrank :
    finrank F (⊤ : Subalgebra F E) = finrank F (⊤ : Submodule F E)

Proof state:
F : Type u_2
E : Type u_3
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
⊢ finrank F ↥⊤ = finrank F ↥⊤

Tactic:
rw [← Algebra.top_toSubmodule]

Result:
F : Type u_2
E : Type u_3
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
⊢ finrank F ↥⊤ = finrank F ↥(Subalgebra.toSubmodule ⊤)

Proof state:
F : Type u_2
E : Type u_3
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
⊢ finrank F ↥⊤ = finrank F ↥(Subalgebra.toSubmodule ⊤)

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
theorem derivWithin_sub (hf : DifferentiableWithinAt 𝕜 f s x)
    (hg : DifferentiableWithinAt 𝕜 g s x) :
    derivWithin (fun y => f y - g y) s x = derivWithin f s x - derivWithin g s x

Proof state:
case inl
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : 𝕜 → F
x : 𝕜
s : Set 𝕜
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y => f y - g y) s x = derivWithin f s x - derivWithin g s x

Tactic:
exact (hf.hasDerivWithinAt.sub hg.hasDerivWithinAt).derivWithin hxs

Result:
no goals

Proof state:
case inr
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : 𝕜 → F
x : 𝕜
s : Set 𝕜
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun y => f y - g y) s x = derivWithin f s x - derivWithin g s x

Tactic:
simp [derivWithin_zero_of_isolated hxs]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : 𝕜 → F
x : 𝕜
s : Set 𝕜
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
⊢ derivWithin (fun y => f y - g y) s x = derivWithin f s x - derivWithin g s x

Tactic:
rcases uniqueDiffWithinAt_or_nhdsWithin_eq_bot s x with hxs | hxs

Result:
case inl
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : 𝕜 → F
x : 𝕜
s : Set 𝕜
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y => f y - g y) s x = derivWithin f s x - derivWithin g s x

case inr
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : 𝕜 → F
x : 𝕜
s : Set 𝕜
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun y => f y - g y) s x = derivWithin f s x - derivWithin g s x
-- Mathlib/Algebra/Ring/Center.lean
theorem natCast_mem_center [NonAssocSemiring M] (n : ℕ) : (n : M) ∈ Set.center M where
  comm _

Proof state:
M : Type u_1
inst✝ : NonAssocSemiring M
n : ℕ
x✝¹ x✝ : M
⊢ x✝¹ * ↑n * x✝ = x✝¹ * (↑n * x✝)

Tactic:
induction n with
| zero => rw [Nat.cast_zero, zero_mul, mul_zero, zero_mul]
| succ n ihn => rw [Nat.cast_succ, add_mul, mul_add, add_mul, ihn, mul_add, one_mul, mul_one]

Result:
no goals

Proof state:
case succ
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
n : ℕ
ihn : ↑n * (x✝¹ * x✝) = ↑n * x✝¹ * x✝
⊢ ↑(n + 1) * (x✝¹ * x✝) = ↑(n + 1) * x✝¹ * x✝

Tactic:
rw [Nat.cast_succ, add_mul, one_mul, ihn, add_mul, add_mul, one_mul]

Result:
no goals

Proof state:
case zero
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
⊢ x✝¹ * x✝ * ↑0 = x✝¹ * (x✝ * ↑0)

Tactic:
rw [Nat.cast_zero, mul_zero, mul_zero, mul_zero]

Result:
no goals

Proof state:
case zero
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
⊢ ↑0 * (x✝¹ * x✝) = ↑0 * x✝¹ * x✝

Tactic:
rw [Nat.cast_zero, zero_mul, zero_mul, zero_mul]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : NonAssocSemiring M
n : ℕ
x✝ : M
⊢ ↑n * x✝ = x✝ * ↑n

Tactic:
rw [Nat.commute_cast]

Result:
no goals

Proof state:
case zero
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
⊢ x✝¹ * ↑0 * x✝ = x✝¹ * (↑0 * x✝)

Tactic:
rw [Nat.cast_zero, zero_mul, mul_zero, zero_mul]

Result:
no goals

Proof state:
case succ
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
n : ℕ
ihn : x✝¹ * ↑n * x✝ = x✝¹ * (↑n * x✝)
⊢ x✝¹ * ↑(n + 1) * x✝ = x✝¹ * (↑(n + 1) * x✝)

Tactic:
rw [Nat.cast_succ, add_mul, mul_add, add_mul, ihn, mul_add, one_mul, mul_one]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : NonAssocSemiring M
n : ℕ
x✝¹ x✝ : M
⊢ ↑n * (x✝¹ * x✝) = ↑n * x✝¹ * x✝

Tactic:
induction n with
| zero => rw [Nat.cast_zero, zero_mul, zero_mul, zero_mul]
| succ n ihn => rw [Nat.cast_succ, add_mul, one_mul, ihn, add_mul, add_mul, one_mul]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : NonAssocSemiring M
n : ℕ
x✝¹ x✝ : M
⊢ x✝¹ * x✝ * ↑n = x✝¹ * (x✝ * ↑n)

Tactic:
induction n with
| zero => rw [Nat.cast_zero, mul_zero, mul_zero, mul_zero]
| succ n ihn => rw [Nat.cast_succ, mul_add, ihn, mul_add, mul_add, mul_one, mul_one]

Result:
no goals

Proof state:
case succ
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
n : ℕ
ihn : x✝¹ * x✝ * ↑n = x✝¹ * (x✝ * ↑n)
⊢ x✝¹ * x✝ * ↑(n + 1) = x✝¹ * (x✝ * ↑(n + 1))

Tactic:
rw [Nat.cast_succ, mul_add, ihn, mul_add, mul_add, mul_one, mul_one]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem comap_neBot_iff_frequently {f : Filter β} {m : α → β} :
    NeBot (comap m f) ↔ ∃ᶠ y in f, y ∈ range m

Proof state:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
⊢ (comap m f).NeBot ↔ ∃ᶠ (y : β) in f, y ∈ range m

Tactic:
simp only [comap_neBot_iff, frequently_iff, mem_range, @and_comm (_ ∈ _), exists_exists_eq_and]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem norm_le_iff [NumberField K] (x : K) (r : ℝ) :
    ‖canonicalEmbedding K x‖ ≤ r ↔ ∀ φ : K →+* ℂ, ‖φ x‖ ≤ r

Proof state:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : 0 ≤ r
⊢ ‖(canonicalEmbedding K) x‖ ≤ r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r

Tactic:
lift r to NNReal using hr

Result:
case inr.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : NNReal
⊢ ‖(canonicalEmbedding K) x‖ ≤ ↑r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ ↑r

Proof state:
case inr.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : NNReal
⊢ ‖(canonicalEmbedding K) x‖ ≤ ↑r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ ↑r

Tactic:
simp_rw [← coe_nnnorm, nnnorm_eq, NNReal.coe_le_coe, Finset.sup_le_iff, Finset.mem_univ,
  forall_true_left]

Result:
no goals

Proof state:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
⊢ ‖(canonicalEmbedding K) x‖ ≤ r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r

Tactic:
obtain ⟨φ⟩ := (inferInstance : Nonempty (K →+* ℂ))

Result:
case inl.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ ‖(canonicalEmbedding K) x‖ ≤ r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
⊢ ‖(canonicalEmbedding K) x‖ ≤ r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r

Tactic:
obtain hr | hr := lt_or_le r 0

Result:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
⊢ ‖(canonicalEmbedding K) x‖ ≤ r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r

case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : 0 ≤ r
⊢ ‖(canonicalEmbedding K) x‖ ≤ r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r

Proof state:
case inl.intro.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ ¬∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r

Tactic:
exact fun h => hr.not_le (le_trans (norm_nonneg _) (h φ))

Result:
no goals

Proof state:
case inl.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ ‖(canonicalEmbedding K) x‖ ≤ r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r

Tactic:
refine iff_of_false ?_ ?_

Result:
case inl.intro.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ ¬‖(canonicalEmbedding K) x‖ ≤ r

case inl.intro.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ ¬∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r

Proof state:
case inl.intro.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
hr : r < 0
φ : K →+* ℂ
⊢ ¬‖(canonicalEmbedding K) x‖ ≤ r

Tactic:
exact (hr.trans_le (norm_nonneg _)).not_le

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/FiniteField.lean
theorem ZMod.trace_pow_card {p : ℕ} [Fact p.Prime] (M : Matrix n n (ZMod p)) :
    trace (M ^ p) = trace M ^ p

Proof state:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
p : ℕ
inst✝ : Fact (Nat.Prime p)
M : Matrix n n (ZMod p)
⊢ (M ^ p).trace = M.trace ^ p

Tactic:
have h := FiniteField.trace_pow_card M

Result:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
p : ℕ
inst✝ : Fact (Nat.Prime p)
M : Matrix n n (ZMod p)
h : (M ^ Fintype.card (ZMod p)).trace = M.trace ^ Fintype.card (ZMod p)
⊢ (M ^ p).trace = M.trace ^ p

Proof state:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
p : ℕ
inst✝ : Fact (Nat.Prime p)
M : Matrix n n (ZMod p)
h : (M ^ Fintype.card (ZMod p)).trace = M.trace ^ Fintype.card (ZMod p)
⊢ (M ^ p).trace = M.trace ^ p

Tactic:
rwa [ZMod.card] at h

Result:
no goals