harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/PartENat.lean
theorem natCast_lt_top (x : ℕ) : (x : PartENat) < ⊤ :=
  Ne.lt_top fun h => absurd (congr_arg Dom h) <| by simp only [dom_natCast]; exact true_ne_false

Proof state:
x : ℕ
h : ↑x = ⊤
⊢ ¬(↑x).Dom = ⊤.Dom

Tactic:
simp only [dom_natCast]

Result:
x : ℕ
h : ↑x = ⊤
⊢ ¬True = ⊤.Dom

Proof state:
x : ℕ
h : ↑x = ⊤
⊢ ¬True = ⊤.Dom

Tactic:
exact true_ne_false

Result:
no goals
-- Mathlib/Data/Matroid/Map.lean
@[simp] lemma comap_emptyOn (f : α → β) : comap (emptyOn β) f = emptyOn α

Proof state:
α : Type u_1
β : Type u_2
f : α → β
⊢ (emptyOn β).comap f = emptyOn α

Tactic:
simp [← ground_eq_empty_iff]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma Z_eq_zero_of_equiv {P Q : Fin 3 → R} (h : P ≈ Q) : P z = 0 ↔ Q z = 0

Proof state:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
h : P ≈ Q
⊢ P z = 0 ↔ Q z = 0

Tactic:
rcases h with ⟨_, rfl⟩

Result:
case intro
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
w✝ : Rˣ
⊢ (fun m => m • Q) w✝ z = 0 ↔ Q z = 0

Proof state:
case intro
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
w✝ : Rˣ
⊢ (fun m => m • Q) w✝ z = 0 ↔ Q z = 0

Tactic:
simp only [Units.smul_def, smul_fin3_ext, Units.mul_right_eq_zero]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem bddAbove_iff_small {s : Set Cardinal.{u}} : BddAbove s ↔ Small.{u} s :=
  ⟨fun ⟨a, ha⟩ => @small_subset _ (Iic a) s (fun _ h => ha h) _, by
    rintro ⟨ι, ⟨e⟩⟩
    use sum.{u, u} fun x ↦ e.symm x
    intro a ha
    simpa using le_sum (fun x ↦ e.symm x) (e ⟨a, ha⟩)⟩

Proof state:
s : Set Cardinal.{u}
⊢ Small.{u, u + 1} ↑s → BddAbove s

Tactic:
rintro ⟨ι, ⟨e⟩⟩

Result:
case mk.intro.intro
s : Set Cardinal.{u}
ι : Type u
e : ↑s ≃ ι
⊢ BddAbove s

Proof state:
case h
s : Set Cardinal.{u}
ι : Type u
e : ↑s ≃ ι
⊢ (sum fun x => ↑(e.symm x)) ∈ upperBounds s

Tactic:
intro a ha

Result:
case h
s : Set Cardinal.{u}
ι : Type u
e : ↑s ≃ ι
a : Cardinal.{u}
ha : a ∈ s
⊢ a ≤ sum fun x => ↑(e.symm x)

Proof state:
case h
s : Set Cardinal.{u}
ι : Type u
e : ↑s ≃ ι
a : Cardinal.{u}
ha : a ∈ s
⊢ a ≤ sum fun x => ↑(e.symm x)

Tactic:
simpa using le_sum (fun x ↦ e.symm x) (e ⟨a, ha⟩)

Result:
no goals

Proof state:
case mk.intro.intro
s : Set Cardinal.{u}
ι : Type u
e : ↑s ≃ ι
⊢ BddAbove s

Tactic:
use sum.{u, u} fun x ↦ e.symm x

Result:
case h
s : Set Cardinal.{u}
ι : Type u
e : ↑s ≃ ι
⊢ (sum fun x => ↑(e.symm x)) ∈ upperBounds s
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.even_zsmul_periodic [AddGroup α] [InvolutiveNeg β] (h : Antiperiodic f c)
    (n : ℤ) : Periodic f ((2 * n) • c)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
⊢ Periodic f (n • 2 • c)

Tactic:
exact h.periodic.zsmul n

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
⊢ Periodic f ((2 * n) • c)

Tactic:
rw [mul_comm, mul_zsmul, two_zsmul, ← two_nsmul]

Result:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
⊢ Periodic f (n • 2 • c)
-- Mathlib/Logic/Equiv/Set.lean
theorem ofLeftInverse'_eq_ofInjective {α β : Type*} (f : α → β) (f_inv : β → α)
    (hf : LeftInverse f_inv f) : ofLeftInverse' f f_inv hf = ofInjective f hf.injective

Proof state:
α : Type u_1
β : Type u_2
f : α → β
f_inv : β → α
hf : LeftInverse f_inv f
⊢ ofLeftInverse' f f_inv hf = ofInjective f ⋯

Tactic:
ext

Result:
case H.a
α : Type u_1
β : Type u_2
f : α → β
f_inv : β → α
hf : LeftInverse f_inv f
x✝ : α
⊢ ↑((ofLeftInverse' f f_inv hf) x✝) = ↑((ofInjective f ⋯) x✝)

Proof state:
case H.a
α : Type u_1
β : Type u_2
f : α → β
f_inv : β → α
hf : LeftInverse f_inv f
x✝ : α
⊢ ↑((ofLeftInverse' f f_inv hf) x✝) = ↑((ofInjective f ⋯) x✝)

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem natDegree_cyclotomic' {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) :
    (cyclotomic' n R).natDegree = Nat.totient n

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ ∑ i ∈ primitiveRoots n R, (X - C i).natDegree = n.totient

Tactic:
simp only [IsPrimitiveRoot.card_primitiveRoots h, mul_one, natDegree_X_sub_C, Nat.cast_id,
  Finset.sum_const, nsmul_eq_mul]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ ∀ i ∈ primitiveRoots n R, X - C i ≠ 0

Tactic:
intro z _

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
z : R
a✝ : z ∈ primitiveRoots n R
⊢ X - C z ≠ 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ (cyclotomic' n R).natDegree = n.totient

Tactic:
rw [cyclotomic']

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ (∏ μ ∈ primitiveRoots n R, (X - C μ)).natDegree = n.totient

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
z : R
a✝ : z ∈ primitiveRoots n R
⊢ X - C z ≠ 0

Tactic:
exact X_sub_C_ne_zero z

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ (∏ μ ∈ primitiveRoots n R, (X - C μ)).natDegree = n.totient

Tactic:
rw [natDegree_prod (primitiveRoots n R) fun z : R => X - C z]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ ∑ i ∈ primitiveRoots n R, (X - C i).natDegree = n.totient

R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ ∀ i ∈ primitiveRoots n R, X - C i ≠ 0
-- Mathlib/RingTheory/Spectrum/Prime/ConstructibleSet.lean
@[simp]
lemma map_id [DecidableEq R] (s : ConstructibleSetData R) : s.map (.id _) = s

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq R
s : ConstructibleSetData R
⊢ map (RingHom.id R) s = s

Tactic:
simp [map]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem contains_iff_find? {t : RBMap α β cmp} :
    t.contains x ↔ ∃ v, t.find? x = some v

Proof state:
α : Type u_1
β : Type u_2
cmp : α → α → Ordering
x : α
t : RBMap α β cmp
⊢ t.contains x = true ↔ ∃ v, t.find? x = some v

Tactic:
simp only [contains_iff_findEntry?, Prod.exists, find?, Option.map_eq_some', and_comm,
  exists_eq_left]

Result:
α : Type u_1
β : Type u_2
cmp : α → α → Ordering
x : α
t : RBMap α β cmp
⊢ (∃ a b, t.findEntry? x = some (a, b)) ↔ ∃ v a, t.findEntry? x = some (a, v)

Proof state:
α : Type u_1
β : Type u_2
cmp : α → α → Ordering
x : α
t : RBMap α β cmp
⊢ (∃ a b, t.findEntry? x = some (a, b)) ↔ ∃ v a, t.findEntry? x = some (a, v)

Tactic:
rw [exists_comm]

Result:
no goals
-- Mathlib/Order/Filter/Extr.lean
theorem IsMaxOn.sub (hf : IsMaxOn f s a) (hg : IsMinOn g s a) :
    IsMaxOn (fun x => f x - g x) s a

Proof state:
α : Type u
β : Type v
inst✝ : OrderedAddCommGroup β
f g : α → β
a : α
s : Set α
hf : IsMaxOn f s a
hg : IsMinOn g s a
⊢ IsMaxOn (fun x => f x - g x) s a

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem eq_mkArray_of_mem {a : α} {l : Array α} (h : ∀ (b) (_ : b ∈ l), b = a) : l = mkArray l.size a

Proof state:
α : Type u_1
a : α
l : Array α
h : ∀ (b : α), b ∈ l → b = a
⊢ ∀ (b : α), b ∈ l.toList → b = a

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
a : α
l : Array α
h : ∀ (b : α), b ∈ l → b = a
⊢ l = mkArray l.size a

Tactic:
rw [← toList_inj]

Result:
α : Type u_1
a : α
l : Array α
h : ∀ (b : α), b ∈ l → b = a
⊢ l.toList = (mkArray l.size a).toList

Proof state:
α : Type u_1
a : α
l : Array α
h : ∀ (b : α), b ∈ l → b = a
⊢ l.toList = (mkArray l.size a).toList

Tactic:
simpa using List.eq_replicate_of_mem (by simpa using h)

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
theorem AnalyticWithinAt.div {f g : E → 𝕝} {s : Set E} {x : E}
    (fa : AnalyticWithinAt 𝕜 f s x) (ga : AnalyticWithinAt 𝕜 g s x) (g0 : g x ≠ 0) :
    AnalyticWithinAt 𝕜 (fun x ↦ f x / g x) s x

Proof state:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕝 : Type u_7
inst✝¹ : NontriviallyNormedField 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
f g : E → 𝕝
s : Set E
x : E
fa : AnalyticWithinAt 𝕜 f s x
ga : AnalyticWithinAt 𝕜 g s x
g0 : g x ≠ 0
⊢ AnalyticWithinAt 𝕜 (fun x => f x * (g x)⁻¹) s x

Tactic:
exact fa.mul (ga.inv g0)

Result:
no goals

Proof state:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕝 : Type u_7
inst✝¹ : NontriviallyNormedField 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
f g : E → 𝕝
s : Set E
x : E
fa : AnalyticWithinAt 𝕜 f s x
ga : AnalyticWithinAt 𝕜 g s x
g0 : g x ≠ 0
⊢ AnalyticWithinAt 𝕜 (fun x => f x / g x) s x

Tactic:
simp_rw [div_eq_mul_inv]

Result:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕝 : Type u_7
inst✝¹ : NontriviallyNormedField 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
f g : E → 𝕝
s : Set E
x : E
fa : AnalyticWithinAt 𝕜 f s x
ga : AnalyticWithinAt 𝕜 g s x
g0 : g x ≠ 0
⊢ AnalyticWithinAt 𝕜 (fun x => f x * (g x)⁻¹) s x
-- Mathlib/Data/Set/Prod.lean
theorem prod_eq_prod_iff :
    s ×ˢ t = s₁ ×ˢ t₁ ↔ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅)

Proof state:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
⊢ s ×ˢ t = s₁ ×ˢ t₁ ↔ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅)

Tactic:
symm

Result:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁

Proof state:
case inl
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s ×ˢ t = ∅
⊢ s = s₁ ∧ t = t₁ → s₁ = ∅ ∨ t₁ = ∅

Tactic:
rintro ⟨rfl, rfl⟩

Result:
case inl.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : s ×ˢ t = ∅
⊢ s = ∅ ∨ t = ∅

Proof state:
case inl
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s ×ˢ t = ∅
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁

Tactic:
simp_rw [h, @eq_comm _ ∅, prod_eq_empty_iff, prod_eq_empty_iff.mp h, true_and,
  or_iff_right_iff_imp]

Result:
case inl
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s ×ˢ t = ∅
⊢ s = s₁ ∧ t = t₁ → s₁ = ∅ ∨ t₁ = ∅

Proof state:
case inr
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : ¬(s = ∅ ∨ t = ∅)
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁

Tactic:
simp_rw [h, false_and, or_false]

Result:
no goals

Proof state:
case inl.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : s ×ˢ t = ∅
⊢ s = ∅ ∨ t = ∅

Tactic:
exact prod_eq_empty_iff.mp h

Result:
no goals

Proof state:
case inr
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁

Tactic:
rw [prod_eq_prod_iff_of_nonempty h]

Result:
case inr
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁

Proof state:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁

Tactic:
rcases eq_empty_or_nonempty (s ×ˢ t) with h | h

Result:
case inl
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s ×ˢ t = ∅
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁

case inr
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁

Proof state:
case inr
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁

Tactic:
rw [nonempty_iff_ne_empty, Ne, prod_eq_empty_iff] at h

Result:
case inr
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : ¬(s = ∅ ∨ t = ∅)
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem prod_dist_eq_card (f g : WithLp 0 (α × β)) : dist f g =
    (if dist f.fst g.fst = 0 then 0 else 1) + (if dist f.snd g.snd = 0 then 0 else 1)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Dist α
inst✝ : Dist β
f g : WithLp 0 (α × β)
⊢ dist f g = (if dist f.1 g.1 = 0 then 0 else 1) + if dist f.2 g.2 = 0 then 0 else 1

Tactic:
convert if_pos rfl

Result:
no goals
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem add_choose (i j : ℕ) : (i + j).choose j = (i + j)! / (i ! * j !)

Proof state:
i j : ℕ
⊢ (i + j).choose j = (i + j)! / (i ! * j !)

Tactic:
rw [choose_eq_factorial_div_factorial (Nat.le_add_left j i), Nat.add_sub_cancel_right,
  Nat.mul_comm]

Result:
no goals
-- Mathlib/Order/Interval/Set/OrdConnectedComponent.lean
theorem ordConnectedComponent_eq_empty : ordConnectedComponent s x = ∅ ↔ x ∉ s

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : α
⊢ s.ordConnectedComponent x = ∅ ↔ x ∉ s

Tactic:
rw [← not_nonempty_iff_eq_empty, nonempty_ordConnectedComponent]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast!_insertEntry_self [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α}
    [Inhabited (β k)] {v : β k} : getValueCast! k (insertEntry k v l) = v

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
l : List ((a : α) × β a)
k : α
inst✝ : Inhabited (β k)
v : β k
⊢ getValueCast! k (insertEntry k v l) = v

Tactic:
rw [getValueCast!_insertEntry, dif_pos BEq.refl, cast_eq]

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Dual.lean
lemma mem_polarSubmodule {S : Type*} [SetLike S E] [SMulMemClass S 𝕜 E] (m : S) (y : Dual 𝕜 E) :
    y ∈ polarSubmodule 𝕜 m ↔ ∀ x ∈ m, y x = 0

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
S : Type u_3
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
m : S
y : Dual 𝕜 E
⊢ y ∈ polarSubmodule 𝕜 m ↔ ∀ x ∈ m, y x = 0

Tactic:
have := polarSubmodule_eq_setOf 𝕜 m

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
S : Type u_3
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
m : S
y : Dual 𝕜 E
this : ↑(polarSubmodule 𝕜 m) = {y | ∀ x ∈ m, y x = 0}
⊢ y ∈ polarSubmodule 𝕜 m ↔ ∀ x ∈ m, y x = 0

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
S : Type u_3
inst✝¹ : SetLike S E
inst✝ : SMulMemClass S 𝕜 E
m : S
y : Dual 𝕜 E
this : (y ∈ ↑(polarSubmodule 𝕜 m)) = (y ∈ {y | ∀ x ∈ m, y x = 0})
⊢ y ∈ polarSubmodule 𝕜 m ↔ ∀ x ∈ m, y x = 0

Tactic:
rwa [propext_iff] at this

Result:
no goals
-- Mathlib/Algebra/Order/Archimedean/Basic.lean
theorem exists_mem_Ico_zpow (hx : 0 < x) (hy : 1 < y) : ∃ n : ℤ, x ∈ Ico (y ^ n) (y ^ (n + 1))

Proof state:
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
x y : α
inst✝ : ExistsAddOfLE α
hx : 0 < x
hy : 1 < y
⊢ ∃ n, x ∈ Ico (y ^ n) (y ^ (n + 1))

Tactic:
classical exact
    let ⟨N, hN⟩ := pow_unbounded_of_one_lt x⁻¹ hy
    have he : ∃ m : ℤ, y ^ m ≤ x :=
      ⟨-N,
        le_of_lt
          (by
            rw [zpow_neg y ↑N, zpow_natCast]
            exact (inv_lt_comm₀ hx (lt_trans (inv_pos.2 hx) hN)).1 hN)⟩
    let ⟨M, hM⟩ := pow_unbounded_of_one_lt x hy
    have hb : ∃ b : ℤ, ∀ m, y ^ m ≤ x → m ≤ b :=
      ⟨M, fun m hm =>
        le_of_not_lt fun hlt =>
          not_lt_of_ge (zpow_le_zpow_right₀ hy.le hlt.le)
            (lt_of_le_of_lt hm (by rwa [← zpow_natCast] at hM))⟩
    let ⟨n, hn₁, hn₂⟩ := Int.exists_greatest_of_bdd hb he
    ⟨n, hn₁, lt_of_not_ge fun hge => not_le_of_gt (Int.lt_succ _) (hn₂ _ hge)⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
x y : α
inst✝ : ExistsAddOfLE α
hx : 0 < x
hy : 1 < y
N : ℕ
hN : x⁻¹ < y ^ N
he : ∃ m, y ^ m ≤ x
M : ℕ
hM : x < y ^ M
m : ℤ
hm : y ^ m ≤ x
hlt : ↑M < m
⊢ x < y ^ ↑M

Tactic:
rwa [← zpow_natCast] at hM

Result:
no goals

Proof state:
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
x y : α
inst✝ : ExistsAddOfLE α
hx : 0 < x
hy : 1 < y
⊢ ∃ n, x ∈ Ico (y ^ n) (y ^ (n + 1))

Tactic:
exact
let ⟨N, hN⟩ := pow_unbounded_of_one_lt x⁻¹ hy
have he : ∃ m : ℤ, y ^ m ≤ x :=
⟨-N,
le_of_lt
(by
  rw [zpow_neg y ↑N, zpow_natCast]
  exact (inv_lt_comm₀ hx (lt_trans (inv_pos.2 hx) hN)).1 hN)⟩
let ⟨M, hM⟩ := pow_unbounded_of_one_lt x hy
have hb : ∃ b : ℤ, ∀ m, y ^ m ≤ x → m ≤ b :=
⟨M, fun m hm =>
le_of_not_lt fun hlt =>
not_lt_of_ge (zpow_le_zpow_right₀ hy.le hlt.le)
  (lt_of_le_of_lt hm (by rwa [← zpow_natCast] at hM))⟩
let ⟨n, hn₁, hn₂⟩ := Int.exists_greatest_of_bdd hb he
⟨n, hn₁, lt_of_not_ge fun hge => not_le_of_gt (Int.lt_succ _) (hn₂ _ hge)⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
x y : α
inst✝ : ExistsAddOfLE α
hx : 0 < x
hy : 1 < y
N : ℕ
hN : x⁻¹ < y ^ N
⊢ (y ^ N)⁻¹ < x

Tactic:
exact (inv_lt_comm₀ hx (lt_trans (inv_pos.2 hx) hN)).1 hN

Result:
no goals

Proof state:
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
x y : α
inst✝ : ExistsAddOfLE α
hx : 0 < x
hy : 1 < y
N : ℕ
hN : x⁻¹ < y ^ N
⊢ y ^ (-↑N) < x

Tactic:
rw [zpow_neg y ↑N, zpow_natCast]

Result:
α : Type u_1
inst✝² : LinearOrderedSemifield α
inst✝¹ : Archimedean α
x y : α
inst✝ : ExistsAddOfLE α
hx : 0 < x
hy : 1 < y
N : ℕ
hN : x⁻¹ < y ^ N
⊢ (y ^ N)⁻¹ < x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem reverse_drop {l : List α} {n : Nat} :
    (l.drop n).reverse = l.reverse.take (l.length - n)

Proof state:
case pos
α : Type u_1
l : List α
n : Nat
h : n ≤ l.length
⊢ (drop n l).reverse = (drop (l.length - (l.length - n)) l).reverse

Tactic:
congr

Result:
case pos.e_as.e_a
α : Type u_1
l : List α
n : Nat
h : n ≤ l.length
⊢ n = l.length - (l.length - n)

Proof state:
case pos
α : Type u_1
l : List α
n : Nat
h : n ≤ l.length
⊢ (drop n l).reverse = take (l.length - n) l.reverse

Tactic:
rw [take_reverse]

Result:
case pos
α : Type u_1
l : List α
n : Nat
h : n ≤ l.length
⊢ (drop n l).reverse = (drop (l.length - (l.length - n)) l).reverse

Proof state:
case neg
α : Type u_1
l : List α
n : Nat
h : ¬n ≤ l.length
w : l.length - n = 0
⊢ (drop n l).reverse = take (l.length - n) l.reverse

Tactic:
rw [w, take_zero, drop_of_length_le, reverse_nil]

Result:
case neg
α : Type u_1
l : List α
n : Nat
h : ¬n ≤ l.length
w : l.length - n = 0
⊢ l.length ≤ n

Proof state:
case neg
α : Type u_1
l : List α
n : Nat
h : ¬n ≤ l.length
⊢ (drop n l).reverse = take (l.length - n) l.reverse

Tactic:
have w : l.length - n = 0 := by omega

Result:
case neg
α : Type u_1
l : List α
n : Nat
h : ¬n ≤ l.length
w : l.length - n = 0
⊢ (drop n l).reverse = take (l.length - n) l.reverse

Proof state:
α : Type u_1
l : List α
n : Nat
h : ¬n ≤ l.length
⊢ l.length - n = 0

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
l : List α
n : Nat
⊢ (drop n l).reverse = take (l.length - n) l.reverse

Tactic:
by_cases h : n ≤ l.length

Result:
case pos
α : Type u_1
l : List α
n : Nat
h : n ≤ l.length
⊢ (drop n l).reverse = take (l.length - n) l.reverse

case neg
α : Type u_1
l : List α
n : Nat
h : ¬n ≤ l.length
⊢ (drop n l).reverse = take (l.length - n) l.reverse

Proof state:
case neg
α : Type u_1
l : List α
n : Nat
h : ¬n ≤ l.length
w : l.length - n = 0
⊢ l.length ≤ n

Tactic:
omega

Result:
no goals

Proof state:
case pos.e_as.e_a
α : Type u_1
l : List α
n : Nat
h : n ≤ l.length
⊢ n = l.length - (l.length - n)

Tactic:
omega

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem sup_lt_of_lt_sdiff_right (h : x < z \ y) (hyz : y ≤ z) : x ⊔ y < z

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
⊢ x ⊔ y < z

Tactic:
rw [← sdiff_sup_cancel hyz]

Result:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
⊢ x ⊔ y < z \ y ⊔ y

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
h' : z \ y ⊔ y ≤ x ⊔ y
⊢ z \ y ≤ x

Tactic:
rw [← sdiff_idem]

Result:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
h' : z \ y ⊔ y ≤ x ⊔ y
⊢ (z \ y) \ y ≤ x

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
⊢ x ⊔ y < z \ y ⊔ y

Tactic:
refine (sup_le_sup_right h.le _).lt_of_not_le fun h' => h.not_le ?_

Result:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
h' : z \ y ⊔ y ≤ x ⊔ y
⊢ z \ y ≤ x

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : x < z \ y
hyz : y ≤ z
h' : z \ y ⊔ y ≤ x ⊔ y
⊢ (z \ y) \ y ≤ x

Tactic:
exact (sdiff_le_sdiff_of_sup_le_sup_right h').trans sdiff_le

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
lemma lift_mk_le_lift_mk_of_injective {α : Type u} {β : Type v} {f : α → β} (hf : Injective f) :
    Cardinal.lift.{v} (#α) ≤ Cardinal.lift.{u} (#β)

Proof state:
α : Type u
β : Type v
f : α → β
hf : Injective f
⊢ lift.{v, u} #α ≤ lift.{u, v} #β

Tactic:
rw [← Cardinal.mk_range_eq_of_injective hf]

Result:
α : Type u
β : Type v
f : α → β
hf : Injective f
⊢ lift.{u, v} #↑(range f) ≤ lift.{u, v} #β

Proof state:
α : Type u
β : Type v
f : α → β
hf : Injective f
⊢ lift.{u, v} #↑(range f) ≤ lift.{u, v} #β

Tactic:
exact Cardinal.lift_le.2 (Cardinal.mk_set_le _)

Result:
no goals
-- Mathlib/RingTheory/Idempotents.lean
lemma CompleteOrthogonalIdempotents.option (he : OrthogonalIdempotents e) :
    CompleteOrthogonalIdempotents (Option.elim · (1 - ∑ i, e i) e) where
  __ := he.option _ he.isIdempotentElem_sum.one_sub
    (by simp [sub_mul, he.isIdempotentElem_sum.eq]) (by simp [mul_sub, he.isIdempotentElem_sum.eq])
  complete

Proof state:
R : Type u_1
inst✝¹ : Ring R
I : Type u_3
e : I → R
inst✝ : Fintype I
he : OrthogonalIdempotents e
⊢ (∑ i : I, e i) * (1 - ∑ i : I, e i) = 0

Tactic:
simp [mul_sub, he.isIdempotentElem_sum.eq]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Ring R
I : Type u_3
e : I → R
inst✝ : Fintype I
he : OrthogonalIdempotents e
⊢ (1 - ∑ i : I, e i) * ∑ i : I, e i = 0

Tactic:
simp [sub_mul, he.isIdempotentElem_sum.eq]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Ring R
I : Type u_3
e : I → R
inst✝ : Fintype I
he : OrthogonalIdempotents e
⊢ ∑ i : Option I, i.elim (1 - ∑ i : I, e i) e = 1

Tactic:
rw [Fintype.sum_option]

Result:
R : Type u_1
inst✝¹ : Ring R
I : Type u_3
e : I → R
inst✝ : Fintype I
he : OrthogonalIdempotents e
⊢ none.elim (1 - ∑ i : I, e i) e + ∑ i : I, (some i).elim (1 - ∑ i : I, e i) e = 1

Proof state:
R : Type u_1
inst✝¹ : Ring R
I : Type u_3
e : I → R
inst✝ : Fintype I
he : OrthogonalIdempotents e
⊢ none.elim (1 - ∑ i : I, e i) e + ∑ i : I, (some i).elim (1 - ∑ i : I, e i) e = 1

Tactic:
exact sub_add_cancel _ _

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Split.lean
theorem isPartition_splitMany (I : Box ι) (s : Finset (ι × ℝ)) : IsPartition (splitMany I s)

Proof state:
ι : Type u_1
I : Box ι
s : Finset (ι × ℝ)
⊢ (splitMany I s).IsPartition

Tactic:
classical
exact Finset.induction_on s (by simp only [splitMany_empty, isPartitionTop]) fun a s _ hs => by
  simpa only [splitMany_insert, inf_split] using hs.biUnion fun J _ => isPartitionSplit _ _ _

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
s : Finset (ι × ℝ)
⊢ (splitMany I s).IsPartition

Tactic:
exact Finset.induction_on s (by simp only [splitMany_empty, isPartitionTop]) fun a s _ hs => by
  simpa only [splitMany_insert, inf_split] using hs.biUnion fun J _ => isPartitionSplit _ _ _

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
s : Finset (ι × ℝ)
⊢ (splitMany I ∅).IsPartition

Tactic:
simp only [splitMany_empty, isPartitionTop]

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
s✝ : Finset (ι × ℝ)
a : ι × ℝ
s : Finset (ι × ℝ)
x✝ : a ∉ s
hs : (splitMany I s).IsPartition
⊢ (splitMany I (insert a s)).IsPartition

Tactic:
simpa only [splitMany_insert, inf_split] using hs.biUnion fun J _ => isPartitionSplit _ _ _

Result:
no goals