harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Basis/Basic.lean
theorem Basis.restrictScalars_apply (i : ι) : (b.restrictScalars R i : M) = b i

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst✝⁸ : CommRing R
inst✝⁷ : Ring S
inst✝⁶ : Nontrivial S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : IsScalarTower R S M
inst✝ : NoZeroSMulDivisors R S
b : Basis ι S M
i : ι
⊢ ↑((restrictScalars R b) i) = b i

Tactic:
simp only [Basis.restrictScalars, Basis.span_apply]

Result:
no goals
-- Mathlib/Data/Finset/Prod.lean
theorem diag_union : (s ∪ t).diag = s.diag ∪ t.diag

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ (s ∪ t).diag = s.diag ∪ t.diag

Tactic:
ext ⟨i, j⟩

Result:
case h.mk
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
i j : α
⊢ (i, j) ∈ (s ∪ t).diag ↔ (i, j) ∈ s.diag ∪ t.diag

Proof state:
case h.mk
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
i j : α
⊢ (i, j) ∈ (s ∪ t).diag ↔ (i, j) ∈ s.diag ∪ t.diag

Tactic:
simp only [mem_diag, mem_union, or_and_right]

Result:
no goals
-- Mathlib/Data/Nat/Sqrt.lean
lemma sqrt_lt' : sqrt m < n ↔ m < n ^ 2

Proof state:
m n : ℕ
⊢ m.sqrt < n ↔ m < n ^ 2

Tactic:
simp only [← not_le, le_sqrt']

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean
theorem CountablySeparated.mono {m m' : MeasurableSpace α} [hsep : @CountablySeparated _ m]
    (h : m ≤ m') : @CountablySeparated _ m'

Proof state:
α : Type u_1
m m' : MeasurableSpace α
h : m ≤ m'
hsep : HasCountableSeparatingOn α MeasurableSet univ
⊢ HasCountableSeparatingOn α MeasurableSet univ

Tactic:
rcases hsep with ⟨S, Sct, Smeas, hS⟩

Result:
case mk.intro.intro.intro
α : Type u_1
m m' : MeasurableSpace α
h : m ≤ m'
S : Set (Set α)
Sct : S.Countable
Smeas : ∀ s ∈ S, MeasurableSet s
hS : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ HasCountableSeparatingOn α MeasurableSet univ

Proof state:
case mk.intro.intro.intro
α : Type u_1
m m' : MeasurableSpace α
h : m ≤ m'
S : Set (Set α)
Sct : S.Countable
Smeas : ∀ s ∈ S, MeasurableSet s
hS : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ HasCountableSeparatingOn α MeasurableSet univ

Tactic:
use S, Sct, (fun s hs ↦ h _ <| Smeas _ hs), hS

Result:
no goals

Proof state:
α : Type u_1
m m' : MeasurableSpace α
hsep : CountablySeparated α
h : m ≤ m'
⊢ CountablySeparated α

Tactic:
simp_rw [countablySeparated_def] at *

Result:
α : Type u_1
m m' : MeasurableSpace α
h : m ≤ m'
hsep : HasCountableSeparatingOn α MeasurableSet univ
⊢ HasCountableSeparatingOn α MeasurableSet univ
-- Mathlib/LinearAlgebra/Span/Basic.lean
lemma isCompl_span_singleton_of_isCoatom_of_not_mem (hs : IsCoatom s) (hx : x ∉ s) :
    IsCompl s (K ∙ x)

Proof state:
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
hs : IsCoatom s
hx : x ∉ s
⊢ IsCompl s (span K {x})

Tactic:
refine ⟨disjoint_span_singleton_of_not_mem hx, ?_⟩

Result:
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
hs : IsCoatom s
hx : x ∉ s
⊢ Codisjoint s (span K {x})

Proof state:
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
hs : s ⋖ ⊤
hx : x ∉ s
⊢ Codisjoint s (span K {x})

Tactic:
simpa only [codisjoint_iff, sup_comm, not_lt_top_iff] using hs.2 (covBy_span_singleton_sup hx).1

Result:
no goals

Proof state:
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
hs : IsCoatom s
hx : x ∉ s
⊢ Codisjoint s (span K {x})

Tactic:
rw [← covBy_top_iff] at hs

Result:
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Submodule K V
x : V
hs : s ⋖ ⊤
hx : x ∉ s
⊢ Codisjoint s (span K {x})
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem ContDiffAt.analyticAt (h : ContDiffAt 𝕜 ω f x) : AnalyticAt 𝕜 f x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
h : ContDiffAt 𝕜 ω f x
⊢ AnalyticAt 𝕜 f x

Tactic:
rw [← contDiffWithinAt_univ] at h

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
h : ContDiffWithinAt 𝕜 ω f univ x
⊢ AnalyticAt 𝕜 f x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
h : ContDiffWithinAt 𝕜 ω f univ x
⊢ AnalyticAt 𝕜 f x

Tactic:
rw [← analyticWithinAt_univ]

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
h : ContDiffWithinAt 𝕜 ω f univ x
⊢ AnalyticWithinAt 𝕜 f univ x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
h : ContDiffWithinAt 𝕜 ω f univ x
⊢ AnalyticWithinAt 𝕜 f univ x

Tactic:
exact h.analyticWithinAt

Result:
no goals
-- Mathlib/Data/Real/Cardinality.lean
theorem mk_Ioo_real {a b : ℝ} (h : a < b) : #(Ioo a b) = 𝔠

Proof state:
a b : ℝ
h : a < b
h1 : #↑((fun x => x - a) '' Ioo a b) ≤ #↑(Ioo a b)
⊢ 𝔠 ≤ #↑(Ioo 0 (b - a))

Tactic:
replace h := sub_pos_of_lt h

Result:
a b : ℝ
h1 : #↑((fun x => x - a) '' Ioo a b) ≤ #↑(Ioo a b)
h : 0 < b - a
⊢ 𝔠 ≤ #↑(Ioo 0 (b - a))

Proof state:
a b : ℝ
h : a < b
h1 : #↑((fun x => x - a) '' Ioo a b) ≤ #↑(Ioo a b)
⊢ 𝔠 ≤ #↑((fun x => x - a) '' Ioo a b)

Tactic:
rw [image_sub_const_Ioo, sub_self]

Result:
a b : ℝ
h : a < b
h1 : #↑((fun x => x - a) '' Ioo a b) ≤ #↑(Ioo a b)
⊢ 𝔠 ≤ #↑(Ioo 0 (b - a))

Proof state:
a b : ℝ
h1 : #↑((fun x => x - a) '' Ioo a b) ≤ #↑(Ioo a b)
h : 0 < b - a
h2 : #↑(Inv.inv '' Ioo 0 (b - a)) ≤ #↑(Ioo 0 (b - a))
⊢ 𝔠 ≤ #↑(Inv.inv '' Ioo 0 (b - a))

Tactic:
rw [image_inv_eq_inv, inv_Ioo_0_left h, mk_Ioi_real]

Result:
no goals

Proof state:
a b : ℝ
h : a < b
⊢ 𝔠 ≤ #↑(Ioo a b)

Tactic:
have h1 : #((fun x => x - a) '' Ioo a b) ≤ #(Ioo a b) := mk_image_le

Result:
a b : ℝ
h : a < b
h1 : #↑((fun x => x - a) '' Ioo a b) ≤ #↑(Ioo a b)
⊢ 𝔠 ≤ #↑(Ioo a b)

Proof state:
a b : ℝ
h1 : #↑((fun x => x - a) '' Ioo a b) ≤ #↑(Ioo a b)
h : 0 < b - a
⊢ 𝔠 ≤ #↑(Ioo 0 (b - a))

Tactic:
have h2 : #(Inv.inv '' Ioo 0 (b - a)) ≤ #(Ioo 0 (b - a)) := mk_image_le

Result:
a b : ℝ
h1 : #↑((fun x => x - a) '' Ioo a b) ≤ #↑(Ioo a b)
h : 0 < b - a
h2 : #↑(Inv.inv '' Ioo 0 (b - a)) ≤ #↑(Ioo 0 (b - a))
⊢ 𝔠 ≤ #↑(Ioo 0 (b - a))

Proof state:
a b : ℝ
h1 : #↑((fun x => x - a) '' Ioo a b) ≤ #↑(Ioo a b)
h : 0 < b - a
h2 : #↑(Inv.inv '' Ioo 0 (b - a)) ≤ #↑(Ioo 0 (b - a))
⊢ 𝔠 ≤ #↑(Ioo 0 (b - a))

Tactic:
refine le_trans ?_ h2

Result:
a b : ℝ
h1 : #↑((fun x => x - a) '' Ioo a b) ≤ #↑(Ioo a b)
h : 0 < b - a
h2 : #↑(Inv.inv '' Ioo 0 (b - a)) ≤ #↑(Ioo 0 (b - a))
⊢ 𝔠 ≤ #↑(Inv.inv '' Ioo 0 (b - a))

Proof state:
a b : ℝ
h : a < b
h1 : #↑((fun x => x - a) '' Ioo a b) ≤ #↑(Ioo a b)
⊢ 𝔠 ≤ #↑(Ioo a b)

Tactic:
refine le_trans ?_ h1

Result:
a b : ℝ
h : a < b
h1 : #↑((fun x => x - a) '' Ioo a b) ≤ #↑(Ioo a b)
⊢ 𝔠 ≤ #↑((fun x => x - a) '' Ioo a b)

Proof state:
a b : ℝ
h : a < b
⊢ #↑(Ioo a b) = 𝔠

Tactic:
refine le_antisymm (mk_real ▸ mk_set_le _) ?_

Result:
a b : ℝ
h : a < b
⊢ 𝔠 ≤ #↑(Ioo a b)
-- Mathlib/Algebra/GeomSum.lean
theorem Commute.geom_sum₂_succ_eq {α : Type u} [Ring α] {x y : α} (h : Commute x y)
    {n : ℕ} :
    ∑ i ∈ range (n + 1), x ^ i * y ^ (n - i) =
      x ^ n + y * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)

Proof state:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
⊢ ∑ i ∈ range (n + 1), x ^ i * y ^ (n - i) = x ^ n + y * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)

Tactic:
simp_rw [mul_sum, sum_range_succ_comm, tsub_self, pow_zero, mul_one, add_right_inj, ← mul_assoc,
  (h.symm.pow_right _).eq, mul_assoc, ← pow_succ']

Result:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
⊢ ∑ i ∈ range n, x ^ i * y ^ (n - i) = ∑ x_1 ∈ range n, x ^ x_1 * y ^ (n - 1 - x_1 + 1)

Proof state:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n i : ℕ
hi : i ∈ range n
⊢ n - 1 - i + 1 = n - i

Tactic:
rw [Finset.mem_range] at hi

Result:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n i : ℕ
hi : i < n
⊢ n - 1 - i + 1 = n - i

Proof state:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
⊢ ∑ i ∈ range n, x ^ i * y ^ (n - i) = ∑ x_1 ∈ range n, x ^ x_1 * y ^ (n - 1 - x_1 + 1)

Tactic:
refine sum_congr rfl fun i hi => ?_

Result:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n i : ℕ
hi : i ∈ range n
⊢ x ^ i * y ^ (n - i) = x ^ i * y ^ (n - 1 - i + 1)

Proof state:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n i : ℕ
hi : i < n
⊢ n - 1 - i + 1 = n - i

Tactic:
omega

Result:
no goals

Proof state:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n i : ℕ
hi : i ∈ range n
this : n - 1 - i + 1 = n - i
⊢ x ^ i * y ^ (n - i) = x ^ i * y ^ (n - 1 - i + 1)

Tactic:
rw [this]

Result:
no goals

Proof state:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n i : ℕ
hi : i ∈ range n
⊢ x ^ i * y ^ (n - i) = x ^ i * y ^ (n - 1 - i + 1)

Tactic:
suffices n - 1 - i + 1 = n - i by rw [this]

Result:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n i : ℕ
hi : i ∈ range n
⊢ n - 1 - i + 1 = n - i
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem IsInfix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) :
    l₁.filter p <:+: l₂.filter p

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
h : l₁ <:+: l₂
⊢ List.filter p l₁ <:+: List.filter p l₂

Tactic:
obtain ⟨xs, ys, rfl⟩ := h

Result:
case intro.intro
α : Type u_1
p : α → Bool
l₁ xs ys : List α
⊢ List.filter p l₁ <:+: List.filter p (xs ++ l₁ ++ ys)

Proof state:
case intro.intro
α : Type u_1
p : α → Bool
l₁ xs ys : List α
⊢ List.filter p l₁ <:+: List.filter p xs ++ List.filter p l₁ ++ List.filter p ys

Tactic:
apply infix_append _

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
p : α → Bool
l₁ xs ys : List α
⊢ List.filter p l₁ <:+: List.filter p (xs ++ l₁ ++ ys)

Tactic:
rw [filter_append, filter_append]

Result:
case intro.intro
α : Type u_1
p : α → Bool
l₁ xs ys : List α
⊢ List.filter p l₁ <:+: List.filter p xs ++ List.filter p l₁ ++ List.filter p ys
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem derivWithin_clm_comp (hc : DifferentiableWithinAt 𝕜 c s x)
    (hd : DifferentiableWithinAt 𝕜 d s x) :
    derivWithin (fun y => (c y).comp (d y)) s x =
      (derivWithin c s x).comp (d x) + (c x).comp (derivWithin d s x)

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : 𝕜
s : Set 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
⊢ derivWithin (fun y => (c y).comp (d y)) s x = (derivWithin c s x).comp (d x) + (c x).comp (derivWithin d 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
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : 𝕜
s : Set 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y => (c y).comp (d y)) s x = (derivWithin c s x).comp (d x) + (c x).comp (derivWithin d s x)

case inr
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : 𝕜
s : Set 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun y => (c y).comp (d y)) s x = (derivWithin c s x).comp (d x) + (c x).comp (derivWithin d s x)

Proof state:
case inr
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : 𝕜
s : Set 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun y => (c y).comp (d y)) s x = (derivWithin c s x).comp (d x) + (c x).comp (derivWithin d s x)

Tactic:
simp [derivWithin_zero_of_isolated hxs]

Result:
no goals

Proof state:
case inl
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : 𝕜
s : Set 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y => (c y).comp (d y)) s x = (derivWithin c s x).comp (d x) + (c x).comp (derivWithin d s x)

Tactic:
exact (hc.hasDerivWithinAt.clm_comp hd.hasDerivWithinAt).derivWithin hxs

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Completion.lean
theorem subfield_ne_real_of_isComplex {v : InfinitePlace K} (hv : IsComplex v) :
    (extensionEmbedding v).fieldRange ≠ Complex.ofRealHom.fieldRange

Proof state:
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : (extensionEmbedding v).fieldRange = Complex.ofRealHom.fieldRange
⊢ ¬v.IsComplex

Tactic:
simp only [not_isComplex_iff_isReal, isReal_iff]

Result:
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : (extensionEmbedding v).fieldRange = Complex.ofRealHom.fieldRange
⊢ ComplexEmbedding.IsReal v.embedding

Proof state:
case a.intro
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : (extensionEmbedding v).fieldRange = Complex.ofRealHom.fieldRange
x : K
r : ℝ
hr : Complex.ofRealHom r = v.embedding x
⊢ (star v.embedding) x = v.embedding x

Tactic:
simp only [ComplexEmbedding.conjugate_coe_eq, ← hr, Complex.ofRealHom_eq_coe, Complex.conj_ofReal]

Result:
no goals

Proof state:
case a
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : (extensionEmbedding v).fieldRange = Complex.ofRealHom.fieldRange
x : K
⊢ (star v.embedding) x = v.embedding x

Tactic:
obtain ⟨r, hr⟩ := hv ▸ extensionEmbedding_coe v x ▸ RingHom.mem_fieldRange_self _ _

Result:
case a.intro
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : (extensionEmbedding v).fieldRange = Complex.ofRealHom.fieldRange
x : K
r : ℝ
hr : Complex.ofRealHom r = v.embedding x
⊢ (star v.embedding) x = v.embedding x

Proof state:
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : v.IsComplex
⊢ (extensionEmbedding v).fieldRange ≠ Complex.ofRealHom.fieldRange

Tactic:
contrapose! hv

Result:
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : (extensionEmbedding v).fieldRange = Complex.ofRealHom.fieldRange
⊢ ¬v.IsComplex

Proof state:
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : (extensionEmbedding v).fieldRange = Complex.ofRealHom.fieldRange
⊢ ComplexEmbedding.IsReal v.embedding

Tactic:
ext x

Result:
case a
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : (extensionEmbedding v).fieldRange = Complex.ofRealHom.fieldRange
x : K
⊢ (star v.embedding) x = v.embedding x
-- Mathlib/FieldTheory/Relrank.lean
theorem relfinrank_comap_comap_eq_relfinrank_of_surjective
    (f : L →+* E) (h : Function.Surjective f) :
    relfinrank (A.comap f) (B.comap f) = relfinrank A B

Proof state:
E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A B : Subfield E
f : L →+* E
h : Function.Surjective ⇑f
⊢ (comap f A).relfinrank (comap f B) = A.relfinrank B

Tactic:
simpa using congr(toNat $(lift_relrank_comap_comap_eq_lift_relrank_of_surjective A B f h))

Result:
no goals
-- Mathlib/Order/PartialSups.lean
lemma partialSups_eq_sUnion_image [DecidableEq (Set α)] (s : ℕ → Set α) (n : ℕ) :
    partialSups s n = ⋃₀ ↑((Finset.range (n + 1)).image s)

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq (Set α)
s : ℕ → Set α
n : ℕ
x✝ : α
⊢ x✝ ∈ (partialSups s) n ↔ x✝ ∈ ⋃₀ ↑(image s (range (n + 1)))

Tactic:
simp [partialSups_eq_biSup, Nat.lt_succ_iff]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq (Set α)
s : ℕ → Set α
n : ℕ
⊢ (partialSups s) n = ⋃₀ ↑(image s (range (n + 1)))

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : DecidableEq (Set α)
s : ℕ → Set α
n : ℕ
x✝ : α
⊢ x✝ ∈ (partialSups s) n ↔ x✝ ∈ ⋃₀ ↑(image s (range (n + 1)))
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
lemma image_basicOpen_eq_basicOpen (a : A) (i : ℕ) :
    toSpec 𝒜 f '' (Subtype.val ⁻¹' (pbo (decompose 𝒜 a i) : Set (ProjectiveSpectrum 𝒜))) =
    (PrimeSpectrum.basicOpen (R := A⁰_ f) <|
      HomogeneousLocalization.mk
        ⟨m * i, ⟨decompose 𝒜 a i ^ m,
          smul_eq_mul m i ▸ SetLike.pow_mem_graded _ (Submodule.coe_mem _)⟩,
          ⟨f^i, by rw [mul_comm]; exact SetLike.pow_mem_graded _ f_deg⟩, ⟨i, rfl⟩⟩).1 :=
  Set.preimage_injective.mpr (toSpec_surjective 𝒜 f_deg hm) <|
    Set.preimage_image_eq _ (toSpec_injective 𝒜 f_deg hm) ▸ by
  rw [Opens.carrier_eq_coe, toSpec_preimage_basicOpen, ProjectiveSpectrum.basicOpen_pow 𝒜 _ m hm]

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
a : A
i : ℕ
⊢ Subtype.val ⁻¹' ↑(pbo ↑(((decompose 𝒜) a) i)) =
    ⇑(ConcreteCategory.hom (toSpec 𝒜 f)) ⁻¹'
      (sbo
          HomogeneousLocalization.mk
            { deg := m * i, num := ⟨↑(((decompose 𝒜) a) i) ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }).carrier

Tactic:
rw [Opens.carrier_eq_coe, toSpec_preimage_basicOpen, ProjectiveSpectrum.basicOpen_pow 𝒜 _ m hm]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
a : A
i : ℕ
⊢ f ^ i ∈ 𝒜 (m * i)

Tactic:
rw [mul_comm]

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
a : A
i : ℕ
⊢ f ^ i ∈ 𝒜 (i * m)

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
a : A
i : ℕ
⊢ f ^ i ∈ 𝒜 (i * m)

Tactic:
exact SetLike.pow_mem_graded _ f_deg

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/Basic.lean
theorem symm_map_nhdsWithin_range (x : H) : map I.symm (𝓝[range I] I x) = 𝓝 x

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
x : H
⊢ map (↑I.symm) (𝓝[range ↑I] ↑I x) = 𝓝 x

Tactic:
rw [← I.map_nhds_eq, map_map, I.symm_comp_self, map_id]

Result:
no goals
-- Mathlib/Algebra/Lie/Derivation/AdjointAction.lean
/-- The definitions `LieDerivation.ad` and `LieAlgebra.ad` agree. -/
@[simp] lemma coe_ad_apply_eq_ad_apply (x : L) : ad R L x = LieAlgebra.ad R L x

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : L
⊢ ↑((ad R L) x) = (LieAlgebra.ad R L) x

Tactic:
ext

Result:
case h
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x x✝ : L
⊢ ↑((ad R L) x) x✝ = ((LieAlgebra.ad R L) x) x✝

Proof state:
case h
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x x✝ : L
⊢ ↑((ad R L) x) x✝ = ((LieAlgebra.ad R L) x) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Perm/Sign.lean
theorem signBijAux_mem {n : ℕ} {f : Perm (Fin n)} :
    ∀ a : Σ_ : Fin n, Fin n, a ∈ finPairsLT n → signBijAux f a ∈ finPairsLT n :=
  fun ⟨a₁, a₂⟩ ha => by
    unfold signBijAux
    split_ifs with h
    · exact mem_finPairsLT.2 h
    · exact mem_finPairsLT.2
        ((le_of_not_gt h).lt_of_ne fun h => (mem_finPairsLT.1 ha).ne (f.injective h.symm))

Proof state:
case pos
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩ ∈ finPairsLT n
h : f ⟨a₁, a₂⟩.snd < f ⟨a₁, a₂⟩.fst
⊢ ⟨f ⟨a₁, a₂⟩.fst, f ⟨a₁, a₂⟩.snd⟩ ∈ finPairsLT n

Tactic:
exact mem_finPairsLT.2 h

Result:
no goals

Proof state:
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩ ∈ finPairsLT n
⊢ f.signBijAux ⟨a₁, a₂⟩ ∈ finPairsLT n

Tactic:
unfold signBijAux

Result:
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩ ∈ finPairsLT n
⊢ (if x : f ⟨a₁, a₂⟩.snd < f ⟨a₁, a₂⟩.fst then ⟨f ⟨a₁, a₂⟩.fst, f ⟨a₁, a₂⟩.snd⟩ else ⟨f ⟨a₁, a₂⟩.snd, f ⟨a₁, a₂⟩.fst⟩) ∈
    finPairsLT n

Proof state:
case neg
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩ ∈ finPairsLT n
h : ¬f ⟨a₁, a₂⟩.snd < f ⟨a₁, a₂⟩.fst
⊢ ⟨f ⟨a₁, a₂⟩.snd, f ⟨a₁, a₂⟩.fst⟩ ∈ finPairsLT n

Tactic:
exact mem_finPairsLT.2
  ((le_of_not_gt h).lt_of_ne fun h => (mem_finPairsLT.1 ha).ne (f.injective h.symm))

Result:
no goals

Proof state:
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩ ∈ finPairsLT n
⊢ (if x : f ⟨a₁, a₂⟩.snd < f ⟨a₁, a₂⟩.fst then ⟨f ⟨a₁, a₂⟩.fst, f ⟨a₁, a₂⟩.snd⟩ else ⟨f ⟨a₁, a₂⟩.snd, f ⟨a₁, a₂⟩.fst⟩) ∈
    finPairsLT n

Tactic:
split_ifs with h

Result:
case pos
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩ ∈ finPairsLT n
h : f ⟨a₁, a₂⟩.snd < f ⟨a₁, a₂⟩.fst
⊢ ⟨f ⟨a₁, a₂⟩.fst, f ⟨a₁, a₂⟩.snd⟩ ∈ finPairsLT n

case neg
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩ ∈ finPairsLT n
h : ¬f ⟨a₁, a₂⟩.snd < f ⟨a₁, a₂⟩.fst
⊢ ⟨f ⟨a₁, a₂⟩.snd, f ⟨a₁, a₂⟩.fst⟩ ∈ finPairsLT n
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem UniformCauchySeqOn.cauchy_map [hp : NeBot p] (hf : UniformCauchySeqOn F p s) (hx : x ∈ s) :
    Cauchy (map (fun i => F i x) p)

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
x : α
p : Filter ι
hp : p.NeBot
hf : UniformCauchySeqOn F p s
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ (fun p => (F p.1 x, F p.2 x)) ⁻¹' u ∈ p ×ˢ p

Tactic:
filter_upwards [hf u hu] with p hp using hp x hx

Result:
no goals

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
x : α
p : Filter ι
hp : p.NeBot
hf : UniformCauchySeqOn F p s
hx : x ∈ s
⊢ Cauchy (map (fun i => F i x) p)

Tactic:
simp only [cauchy_map_iff, hp, true_and]

Result:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
x : α
p : Filter ι
hp : p.NeBot
hf : UniformCauchySeqOn F p s
hx : x ∈ s
⊢ Tendsto (fun p => (F p.1 x, F p.2 x)) (p ×ˢ p) (𝓤 β)

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
x : α
p : Filter ι
hp : p.NeBot
hf : UniformCauchySeqOn F p s
hx : x ∈ s
⊢ Tendsto (fun p => (F p.1 x, F p.2 x)) (p ×ˢ p) (𝓤 β)

Tactic:
intro u hu

Result:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
x : α
p : Filter ι
hp : p.NeBot
hf : UniformCauchySeqOn F p s
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ u ∈ map (fun p => (F p.1 x, F p.2 x)) (p ×ˢ p)

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
x : α
p : Filter ι
hp : p.NeBot
hf : UniformCauchySeqOn F p s
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ u ∈ map (fun p => (F p.1 x, F p.2 x)) (p ×ˢ p)

Tactic:
rw [mem_map]

Result:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
x : α
p : Filter ι
hp : p.NeBot
hf : UniformCauchySeqOn F p s
hx : x ∈ s
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ (fun p => (F p.1 x, F p.2 x)) ⁻¹' u ∈ p ×ˢ p