harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/GaussSum.lean
theorem quadraticChar_odd_prime [DecidableEq F] (hF : ringChar F ≠ 2) {p : ℕ} [Fact p.Prime]
    (hp₁ : p ≠ 2) (hp₂ : ringChar F ≠ p) :
    quadraticChar F p = quadraticChar (ZMod p) (χ₄ (Fintype.card F) * Fintype.card F)

Proof state:
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp₁ : p ≠ 2
hp₂ : ringChar F ≠ p
⊢ (quadraticChar F) ↑p = (quadraticChar (ZMod p)) (↑((quadraticChar F) (-1)) * ↑(Fintype.card F))

Tactic:
have h := quadraticChar_card_card hF (ne_of_eq_of_ne (ringChar_zmod_n p) hp₁)
  (ne_of_eq_of_ne (ringChar_zmod_n p) hp₂.symm)

Result:
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp₁ : p ≠ 2
hp₂ : ringChar F ≠ p
h :
  (quadraticChar F) ↑(Fintype.card (ZMod p)) = (quadraticChar (ZMod p)) (↑((quadraticChar F) (-1)) * ↑(Fintype.card F))
⊢ (quadraticChar F) ↑p = (quadraticChar (ZMod p)) (↑((quadraticChar F) (-1)) * ↑(Fintype.card F))

Proof state:
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp₁ : p ≠ 2
hp₂ : ringChar F ≠ p
h :
  (quadraticChar F) ↑(Fintype.card (ZMod p)) = (quadraticChar (ZMod p)) (↑((quadraticChar F) (-1)) * ↑(Fintype.card F))
⊢ (quadraticChar F) ↑p = (quadraticChar (ZMod p)) (↑((quadraticChar F) (-1)) * ↑(Fintype.card F))

Tactic:
rwa [card p] at h

Result:
no goals

Proof state:
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp₁ : p ≠ 2
hp₂ : ringChar F ≠ p
⊢ (quadraticChar F) ↑p = (quadraticChar (ZMod p)) (↑(χ₄ ↑(Fintype.card F)) * ↑(Fintype.card F))

Tactic:
rw [← quadraticChar_neg_one hF]

Result:
F : Type u_1
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
hF : ringChar F ≠ 2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp₁ : p ≠ 2
hp₂ : ringChar F ≠ p
⊢ (quadraticChar F) ↑p = (quadraticChar (ZMod p)) (↑((quadraticChar F) (-1)) * ↑(Fintype.card F))
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem Algebra.injective_of_transcendental [h : Algebra.Transcendental R A] :
    Function.Injective (algebraMap R A)

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
h : Algebra.Transcendental R A
⊢ Function.Injective ⇑(algebraMap R A)

Tactic:
rw [transcendental_iff_not_isAlgebraic] at h

Result:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
h : ¬Algebra.IsAlgebraic R A
⊢ Function.Injective ⇑(algebraMap R A)

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
h : ¬Function.Injective ⇑(algebraMap R A)
⊢ Algebra.IsAlgebraic R A

Tactic:
exact isAlgebraic_of_not_injective h

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
h : ¬Algebra.IsAlgebraic R A
⊢ Function.Injective ⇑(algebraMap R A)

Tactic:
contrapose! h

Result:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
h : ¬Function.Injective ⇑(algebraMap R A)
⊢ Algebra.IsAlgebraic R A
-- Mathlib/Topology/Bases.lean
lemma secondCountableTopology_iInf {α ι} [Countable ι] {t : ι → TopologicalSpace α}
    (ht : ∀ i, @SecondCountableTopology α (t i)) : @SecondCountableTopology α (⨅ i, t i)

Proof state:
α : Type u_1
ι : Sort u_2
inst✝ : Countable ι
t : ι → TopologicalSpace α
ht : ∀ (i : ι), SecondCountableTopology α
⊢ SecondCountableTopology α

Tactic:
exact SecondCountableTopology.mk' <|
  countable_iUnion fun i => @countable_countableBasis _ (t i) (ht i)

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
/-- **Cauchy-Schwarz inequality** for finsets using square roots in `ℝ≥0`. -/
lemma sum_sqrt_mul_sqrt_le (s : Finset ι) (f g : ι → ℝ≥0) :
    ∑ i ∈ s, sqrt (f i) * sqrt (g i) ≤ sqrt (∑ i ∈ s, f i) * sqrt (∑ i ∈ s, g i)

Proof state:
ι : Type u_2
s : Finset ι
f g : ι → ℝ≥0
⊢ ∑ i ∈ s, sqrt (f i) * sqrt (g i) ≤ sqrt (∑ i ∈ s, f i) * sqrt (∑ i ∈ s, g i)

Tactic:
simpa [*] using sum_mul_le_sqrt_mul_sqrt _ (fun x ↦ sqrt (f x)) (fun x ↦ sqrt (g x))

Result:
no goals
-- Mathlib/Analysis/Fourier/FiniteAbelian/Orthogonality.lean
lemma expect_eq_zero_iff_ne_zero : 𝔼 x, ψ x = 0 ↔ ψ ≠ 0

Proof state:
G : Type u_1
R : Type u_3
inst✝⁴ : AddGroup G
inst✝³ : Fintype G
inst✝² : Semifield R
inst✝¹ : IsDomain R
inst✝ : CharZero R
ψ : AddChar G R
⊢ 𝔼 x : G, ψ x = 0 ↔ ψ ≠ 0

Tactic:
rw [expect_eq_ite, one_ne_zero.ite_eq_right_iff]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem prod_sup_eq_top {s : Finset ι} {J : ι → Ideal R} (h : ∀ i, i ∈ s → J i ⊔ I = ⊤) :
    (∏ i ∈ s, J i) ⊔ I = ⊤

Proof state:
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
s : Finset ι
J : ι → Ideal R
h : ∀ i ∈ s, J i ⊔ I = ⊤
i : ι
hi : i ∈ s
⊢ I ⊔ J i = ⊤

Tactic:
rw [sup_comm, h i hi]

Result:
no goals

Proof state:
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
s : Finset ι
J : ι → Ideal R
h : ∀ i ∈ s, J i ⊔ I = ⊤
⊢ (∏ i ∈ s, J i) ⊔ I = ⊤

Tactic:
rw [sup_comm, sup_prod_eq_top]

Result:
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
s : Finset ι
J : ι → Ideal R
h : ∀ i ∈ s, J i ⊔ I = ⊤
⊢ ∀ i ∈ s, I ⊔ J i = ⊤

Proof state:
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
s : Finset ι
J : ι → Ideal R
h : ∀ i ∈ s, J i ⊔ I = ⊤
⊢ ∀ i ∈ s, I ⊔ J i = ⊤

Tactic:
intro i hi

Result:
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
s : Finset ι
J : ι → Ideal R
h : ∀ i ∈ s, J i ⊔ I = ⊤
i : ι
hi : i ∈ s
⊢ I ⊔ J i = ⊤
-- Mathlib/Data/List/Forall2.lean
theorem forall₂_eq_eq_eq : Forall₂ ((· = ·) : α → α → Prop) = Eq

Proof state:
case h.h.a.mpr
α : Type u_1
a : List α
⊢ Forall₂ (fun x1 x2 => x1 = x2) a a

Tactic:
exact forall₂_refl _

Result:
no goals

Proof state:
case h.h.a.mp.cons
α : Type u_1
a b : List α
a✝² b✝ : α
l₁✝ l₂✝ : List α
a✝¹ : a✝² = b✝
a✝ : Forall₂ (fun x1 x2 => x1 = x2) l₁✝ l₂✝
a_ih✝ : l₁✝ = l₂✝
⊢ a✝² :: l₁✝ = b✝ :: l₂✝

Tactic:
simp only [*]

Result:
no goals

Proof state:
case h.h.a
α : Type u_1
a b : List α
⊢ Forall₂ (fun x1 x2 => x1 = x2) a b ↔ a = b

Tactic:
constructor

Result:
case h.h.a.mp
α : Type u_1
a b : List α
⊢ Forall₂ (fun x1 x2 => x1 = x2) a b → a = b

case h.h.a.mpr
α : Type u_1
a b : List α
⊢ a = b → Forall₂ (fun x1 x2 => x1 = x2) a b

Proof state:
case h.h
α : Type u_1
a b : List α
⊢ Forall₂ (fun x1 x2 => x1 = x2) a b = (a = b)

Tactic:
apply propext

Result:
case h.h.a
α : Type u_1
a b : List α
⊢ Forall₂ (fun x1 x2 => x1 = x2) a b ↔ a = b

Proof state:
case h.h.a.mp.nil
α : Type u_1
a b : List α
⊢ [] = []

Tactic:
rfl

Result:
no goals

Proof state:
case h.h.a.mp
α : Type u_1
a b : List α
⊢ Forall₂ (fun x1 x2 => x1 = x2) a b → a = b

Tactic:
intro h

Result:
case h.h.a.mp
α : Type u_1
a b : List α
h : Forall₂ (fun x1 x2 => x1 = x2) a b
⊢ a = b

Proof state:
case h.h.a.mp
α : Type u_1
a b : List α
h : Forall₂ (fun x1 x2 => x1 = x2) a b
⊢ a = b

Tactic:
induction h

Result:
case h.h.a.mp.nil
α : Type u_1
a b : List α
⊢ [] = []

case h.h.a.mp.cons
α : Type u_1
a b : List α
a✝² b✝ : α
l₁✝ l₂✝ : List α
a✝¹ : a✝² = b✝
a✝ : Forall₂ (fun x1 x2 => x1 = x2) l₁✝ l₂✝
a_ih✝ : l₁✝ = l₂✝
⊢ a✝² :: l₁✝ = b✝ :: l₂✝

Proof state:
case h.h.a.mpr
α : Type u_1
a b : List α
⊢ a = b → Forall₂ (fun x1 x2 => x1 = x2) a b

Tactic:
rintro rfl

Result:
case h.h.a.mpr
α : Type u_1
a : List α
⊢ Forall₂ (fun x1 x2 => x1 = x2) a a

Proof state:
α : Type u_1
⊢ (Forall₂ fun x1 x2 => x1 = x2) = Eq

Tactic:
funext a b

Result:
case h.h
α : Type u_1
a b : List α
⊢ Forall₂ (fun x1 x2 => x1 = x2) a b = (a = b)
-- Mathlib/Analysis/Normed/Module/Ray.lean
theorem sameRay_iff_of_norm_eq (h : ‖x‖ = ‖y‖) : SameRay ℝ x y ↔ x = y

Proof state:
case inl
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
h : ‖x‖ = ‖0‖
⊢ SameRay ℝ x 0 ↔ x = 0

Tactic:
rw [norm_zero, norm_eq_zero] at h

Result:
case inl
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
h : x = 0
⊢ SameRay ℝ x 0 ↔ x = 0

Proof state:
case inr
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
h : ‖x‖ = ‖y‖
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ x = y

Tactic:
exact ⟨fun hxy => norm_injOn_ray_right hy hxy SameRay.rfl h, fun hxy => hxy ▸ SameRay.rfl⟩

Result:
no goals

Proof state:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
h : ‖x‖ = ‖y‖
⊢ SameRay ℝ x y ↔ x = y

Tactic:
obtain rfl | hy := eq_or_ne y 0

Result:
case inl
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
h : ‖x‖ = ‖0‖
⊢ SameRay ℝ x 0 ↔ x = 0

case inr
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
h : ‖x‖ = ‖y‖
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ x = y

Proof state:
case inl
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
h : x = 0
⊢ SameRay ℝ x 0 ↔ x = 0

Tactic:
exact iff_of_true (SameRay.zero_right _) h

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
/-- Consider two functions `f` and `g` which coincide on a set `s` and are continuous there.
Then there is an open neighborhood of `s` on which `f` and `g` are uniformly close. -/
lemma exists_is_open_mem_uniformity_of_forall_mem_eq
    [TopologicalSpace β] {r : Set (α × α)} {s : Set β}
    {f g : β → α} (hf : ∀ x ∈ s, ContinuousAt f x) (hg : ∀ x ∈ s, ContinuousAt g x)
    (hfg : s.EqOn f g) (hr : r ∈ 𝓤 α) :
    ∃ t, IsOpen t ∧ s ⊆ t ∧ ∀ x ∈ t, (f x, g x) ∈ r

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
r : Set (α × α)
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
x : β
hx : x ∈ s
t : Set (α × α)
ht : t ∈ 𝓤 α
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
A : {z | (f x, f z) ∈ t} ∈ 𝓝 x
B : {z | (g x, g z) ∈ t} ∈ 𝓝 x
u : Set β
hu : u ⊆ {z | (f x, f z) ∈ t} ∩ {z | (g x, g z) ∈ t}
u_open : IsOpen u
xu : x ∈ u
y : β
hy : y ∈ u
I1 : (f y, f x) ∈ t
I2 : (g x, g y) ∈ t
⊢ (f y, g y) ∈ r

Tactic:
rw [hfg hx] at I1

Result:
case intro.intro.intro.intro.intro.intro
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
r : Set (α × α)
s : Set β
f g : β → α
hf : ∀ x ∈ s, ContinuousAt f x
hg : ∀ x ∈ s, ContinuousAt g x
hfg : EqOn f g s
hr : r ∈ 𝓤 α
x : β
hx : x ∈ s
t : Set (α × α)
ht : t ∈ 𝓤 α
htsymm : SymmetricRel t
htr : t ○ t ⊆ r
A : {z | (f x, f z) ∈ t} ∈ 𝓝 x
B : {z | (g x, g z) ∈ t} ∈ 𝓝 x
u : Set β
hu : u ⊆ {z | (f x, f z) ∈ t} ∩ {z | (g x, g z) ∈ t}
u_open : IsOpen u
xu : x ∈ u
y : β
hy : y ∈ u
I1 : (f y, g x) ∈ t
I2 : (g x, g y) ∈ t
⊢ (f y, g y) ∈ r
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma nonsingular_zero_of_Δ_ne_zero (h : W'.Equation 0 0) (hΔ : W'.Δ ≠ 0) :
    W'.Nonsingular 0 0

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
h : W'.Equation 0 0
hΔ : Δ W' ≠ 0
⊢ W'.Nonsingular 0 0

Tactic:
simp only [equation_zero, nonsingular_zero] at *

Result:
R : Type r
inst✝ : CommRing R
W' : Affine R
hΔ : Δ W' ≠ 0
h : W'.a₆ = 0
⊢ W'.a₆ = 0 ∧ (W'.a₃ ≠ 0 ∨ W'.a₄ ≠ 0)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
hΔ : Δ W' ≠ 0
h : W'.a₆ = 0
⊢ W'.a₆ = 0 ∧ (W'.a₃ ≠ 0 ∨ W'.a₄ ≠ 0)

Tactic:
contrapose! hΔ

Result:
R : Type r
inst✝ : CommRing R
W' : Affine R
h : W'.a₆ = 0
hΔ : W'.a₆ = 0 → W'.a₃ = 0 ∧ W'.a₄ = 0
⊢ Δ W' = 0

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
h : W'.a₆ = 0
hΔ : W'.a₆ = 0 → W'.a₃ = 0 ∧ W'.a₄ = 0
⊢ -(W'.a₁ ^ 2 + 4 * W'.a₂) ^ 2 * (W'.a₁ ^ 2 * 0 + 4 * W'.a₂ * 0 - W'.a₁ * 0 * 0 + W'.a₂ * 0 ^ 2 - 0 ^ 2) -
          8 * (2 * 0 + W'.a₁ * 0) ^ 3 -
        27 * (0 ^ 2 + 4 * 0) ^ 2 +
      9 * (W'.a₁ ^ 2 + 4 * W'.a₂) * (2 * 0 + W'.a₁ * 0) * (0 ^ 2 + 4 * 0) =
    0

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
h : W'.a₆ = 0
hΔ : W'.a₆ = 0 → W'.a₃ = 0 ∧ W'.a₄ = 0
⊢ Δ W' = 0

Tactic:
simp only [b₂, b₄, b₆, b₈, Δ, h, hΔ]

Result:
R : Type r
inst✝ : CommRing R
W' : Affine R
h : W'.a₆ = 0
hΔ : W'.a₆ = 0 → W'.a₃ = 0 ∧ W'.a₄ = 0
⊢ -(W'.a₁ ^ 2 + 4 * W'.a₂) ^ 2 * (W'.a₁ ^ 2 * 0 + 4 * W'.a₂ * 0 - W'.a₁ * 0 * 0 + W'.a₂ * 0 ^ 2 - 0 ^ 2) -
          8 * (2 * 0 + W'.a₁ * 0) ^ 3 -
        27 * (0 ^ 2 + 4 * 0) ^ 2 +
      9 * (W'.a₁ ^ 2 + 4 * W'.a₂) * (2 * 0 + W'.a₁ * 0) * (0 ^ 2 + 4 * 0) =
    0
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem associated_unit_mul_left {N : Type*} [CommMonoid N] (a u : N) (hu : IsUnit u) :
    Associated (u * a) a

Proof state:
N : Type u_2
inst✝ : CommMonoid N
a u : N
hu : IsUnit u
⊢ u * a ~ᵤ a

Tactic:
rw [mul_comm]

Result:
N : Type u_2
inst✝ : CommMonoid N
a u : N
hu : IsUnit u
⊢ a * u ~ᵤ a

Proof state:
N : Type u_2
inst✝ : CommMonoid N
a u : N
hu : IsUnit u
⊢ a * u ~ᵤ a

Tactic:
exact associated_mul_unit_left _ _ hu

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem NF.of_dvd_omega0_opow {b e n a} (h : NF (ONote.oadd e n a))
    (d : ω ^ b ∣ repr (ONote.oadd e n a)) :
    b ≤ repr e ∧ ω ^ b ∣ repr a

Proof state:
b : Ordinal.{0}
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
d : ω ^ b ∣ (e.oadd n a).repr
this : ¬(e.oadd n a).repr = repr 0
L : b ≤ e.repr
⊢ b ≤ e.repr ∧ ω ^ b ∣ a.repr

Tactic:
simp only [repr] at d

Result:
b : Ordinal.{0}
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
d : ω ^ b ∣ ω ^ e.repr * ↑↑n + a.repr
this : ¬(e.oadd n a).repr = repr 0
L : b ≤ e.repr
⊢ b ≤ e.repr ∧ ω ^ b ∣ a.repr

Proof state:
b : Ordinal.{0}
e : ONote
n : ℕ+
a : ONote
h✝ : (e.oadd n a).NF
d : ω ^ b ∣ (e.oadd n a).repr
h : e.oadd n a = 0
⊢ False

Tactic:
injection h

Result:
no goals

Proof state:
b : Ordinal.{0}
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
d : ω ^ b ∣ (e.oadd n a).repr
this : ¬(e.oadd n a).repr = repr 0
⊢ b ≤ e.repr ∧ ω ^ b ∣ a.repr

Tactic:
have L := le_of_not_lt fun l => not_le_of_lt (h.below_of_lt l).repr_lt (le_of_dvd this d)

Result:
b : Ordinal.{0}
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
d : ω ^ b ∣ (e.oadd n a).repr
this : ¬(e.oadd n a).repr = repr 0
L : b ≤ e.repr
⊢ b ≤ e.repr ∧ ω ^ b ∣ a.repr

Proof state:
b : Ordinal.{0}
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
d : ω ^ b ∣ ω ^ e.repr * ↑↑n + a.repr
this : ¬(e.oadd n a).repr = repr 0
L : b ≤ e.repr
⊢ b ≤ e.repr ∧ ω ^ b ∣ a.repr

Tactic:
exact ⟨L, (dvd_add_iff <| (opow_dvd_opow _ L).mul_right _).1 d⟩

Result:
no goals

Proof state:
b : Ordinal.{0}
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
d : ω ^ b ∣ (e.oadd n a).repr
⊢ b ≤ e.repr ∧ ω ^ b ∣ a.repr

Tactic:
have := mt repr_inj.1 (fun h => by injection h : ONote.oadd e n a ≠ 0)

Result:
b : Ordinal.{0}
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
d : ω ^ b ∣ (e.oadd n a).repr
this : ¬(e.oadd n a).repr = repr 0
⊢ b ≤ e.repr ∧ ω ^ b ∣ a.repr
-- Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
/-- See `MvPolynomial.IsHomogeneous.funext_of_le_card`
for a version that assumes `n ≤ #R`. -/
lemma funext [Infinite R] {F G : MvPolynomial σ R} {n : ℕ}
    (hF : F.IsHomogeneous n) (hG : G.IsHomogeneous n)
    (h : ∀ r : σ → R, eval r F = eval r G) : F = G

Proof state:
R : Type u_5
σ : Type u_6
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
F G : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
hG : G.IsHomogeneous n
h : ∀ (r : σ → R), (eval r) F = (eval r) G
⊢ F = G

Tactic:
apply funext_of_le_card hF hG h

Result:
R : Type u_5
σ : Type u_6
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
F G : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
hG : G.IsHomogeneous n
h : ∀ (r : σ → R), (eval r) F = (eval r) G
⊢ ↑n ≤ #R

Proof state:
R : Type u_5
σ : Type u_6
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
F G : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
hG : G.IsHomogeneous n
h : ∀ (r : σ → R), (eval r) F = (eval r) G
⊢ ↑n ≤ #R

Tactic:
exact (Cardinal.nat_lt_aleph0 _).le.trans <| Cardinal.infinite_iff.mp ‹Infinite R›

Result:
no goals
-- Mathlib/Tactic/NormNum/LegendreSymbol.lean
theorem jacobiSymNat.even_odd₃ (a b c : ℕ) (r : ℤ) (ha : a % 2 = 0) (hb : b % 8 = 3)
    (hc : a / 2 = c) (hr : jacobiSymNat c b = r) : jacobiSymNat a b = -r

Proof state:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSym (↑a) b = -jacobiSym (↑a / 2) b

Tactic:
rw [← jacobiSym.even_odd (mod_cast ha), if_pos (by simp [hb])]

Result:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 2 = 1

Proof state:
case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 2 ∣ 8

Tactic:
norm_num

Result:
no goals

Proof state:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 2 = 1

Tactic:
rw [← Nat.mod_mod_of_dvd, hb]

Result:
case h
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ 2 ∣ 8

Proof state:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSymNat a b = -r

Tactic:
simp only [jacobiSymNat, ← hr, ← hc, Int.ofNat_ediv, Nat.cast_ofNat]

Result:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ jacobiSym (↑a) b = -jacobiSym (↑a / 2) b

Proof state:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 8 = 3 ∨ b % 8 = 5

Tactic:
simp [hb]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Portmanteau.lean
/-- One implication of the portmanteau theorem:
Assuming that for all Borel sets E whose boundary ∂E carries no probability mass under a
candidate limit probability measure μ we have convergence of the measures μsᵢ(E) to μ(E),
then for all closed sets F we have the limsup condition limsup μsᵢ(F) ≤ μ(F). -/
lemma limsup_measure_closed_le_of_forall_tendsto_measure
    {Ω ι : Type*} {L : Filter ι} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω]
    {μ : Measure Ω} [IsFiniteMeasure μ] {μs : ι → Measure Ω}
    (h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 →
            Tendsto (fun i ↦ μs i E) L (𝓝 (μ E)))
    (F : Set Ω) (F_closed : IsClosed F) :
    L.limsup (fun i ↦ μs i F) ≤ μ F

Proof state:
case inr.h.intro
Ω : Type u_2
ι : Type u_3
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
μs : ι → Measure Ω
h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))
F : Set Ω
F_closed : IsClosed F
h✝ : L.NeBot
ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0
rs : ℕ → ℝ := Classical.choose ex
rs_pos : ∀ (n : ℕ), 0 < rs n
rs_null : ∀ (n : ℕ), μ (frontier (Metric.thickening (rs n) F)) = 0
Fthicks_open : ∀ (n : ℕ), IsOpen (Metric.thickening (rs n) F)
key : ∀ (n : ℕ), Tendsto (fun i => (μs i) (Metric.thickening (rs n) F)) L (𝓝 (μ (Metric.thickening (rs n) F)))
ε : ℝ≥0
ε_pos : 0 < ε
μF_finite : μ F < ⊤
keyB : Tendsto (fun r => μ (Metric.cthickening r F)) (𝓝 0) (𝓝 (μ F))
nhd : Iio (μ F + ↑ε) ∈ 𝓝 (μ F)
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → μ (Metric.cthickening (rs b) F) < μ F + ↑ε
aux : (fun i => (μs i) F) ≤ᶠ[L] fun i => (μs i) (Metric.thickening (rs m) F)
⊢ limsup (fun i => (μs i) F) L ≤ μ F + ↑ε

Tactic:
refine (limsup_le_limsup aux).trans ?_

Result:
case inr.h.intro
Ω : Type u_2
ι : Type u_3
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
μs : ι → Measure Ω
h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))
F : Set Ω
F_closed : IsClosed F
h✝ : L.NeBot
ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0
rs : ℕ → ℝ := Classical.choose ex
rs_pos : ∀ (n : ℕ), 0 < rs n
rs_null : ∀ (n : ℕ), μ (frontier (Metric.thickening (rs n) F)) = 0
Fthicks_open : ∀ (n : ℕ), IsOpen (Metric.thickening (rs n) F)
key : ∀ (n : ℕ), Tendsto (fun i => (μs i) (Metric.thickening (rs n) F)) L (𝓝 (μ (Metric.thickening (rs n) F)))
ε : ℝ≥0
ε_pos : 0 < ε
μF_finite : μ F < ⊤
keyB : Tendsto (fun r => μ (Metric.cthickening r F)) (𝓝 0) (𝓝 (μ F))
nhd : Iio (μ F + ↑ε) ∈ 𝓝 (μ F)
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → μ (Metric.cthickening (rs b) F) < μ F + ↑ε
aux : (fun i => (μs i) F) ≤ᶠ[L] fun i => (μs i) (Metric.thickening (rs m) F)
⊢ limsup (fun i => (μs i) (Metric.thickening (rs m) F)) L ≤ μ F + ↑ε
-- Mathlib/LinearAlgebra/Prod.lean
theorem comap_fst : p.comap (fst R M M₂) = prod p ⊤

Proof state:
case h.mk
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
x : M
y : M₂
⊢ (x, y) ∈ comap (fst R M M₂) p ↔ (x, y) ∈ p.prod ⊤

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
⊢ comap (fst R M M₂) p = p.prod ⊤

Tactic:
ext ⟨x, y⟩

Result:
case h.mk
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
x : M
y : M₂
⊢ (x, y) ∈ comap (fst R M M₂) p ↔ (x, y) ∈ p.prod ⊤
-- Mathlib/Algebra/Ring/Parity.lean
lemma even_neg_two : Even (-2 : α)

Proof state:
α : Type u_2
inst✝ : Ring α
⊢ Even (-2)

Tactic:
simp only [even_neg, even_two]

Result:
no goals
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
theorem nmem_nonZeroDivisors_iff {P : R[X]} : P ∉ R[X]⁰ ↔ ∃ a : R, a ≠ 0 ∧ a • P = 0

Proof state:
R : Type u
inst✝ : CommSemiring R
P : R[X]
hP : P ∉ R[X]⁰
h : ∀ (a : R), a ≠ 0 → a • P ≠ 0
⊢ False

Tactic:
obtain ⟨Q, hQ⟩ := _root_.nmem_nonZeroDivisors_iff.1 hP

Result:
case intro
R : Type u
inst✝ : CommSemiring R
P : R[X]
hP : P ∉ R[X]⁰
h : ∀ (a : R), a ≠ 0 → a • P ≠ 0
Q : R[X]
hQ : Q ∈ {s | s * P = 0 ∧ s ≠ 0}
⊢ False

Proof state:
case intro
R : Type u
inst✝ : CommSemiring R
P : R[X]
hP : P ∉ R[X]⁰
h : ∀ (a : R), a ≠ 0 → a • P ≠ 0
Q : R[X]
hQ : Q ∈ {s | s * P = 0 ∧ s ≠ 0}
⊢ False

Tactic:
refine hQ.2 (eq_zero_of_mul_eq_zero_of_smul P (fun a ha ↦ ?_) Q (mul_comm P _ ▸ hQ.1))

Result:
case intro
R : Type u
inst✝ : CommSemiring R
P : R[X]
hP : P ∉ R[X]⁰
h : ∀ (a : R), a ≠ 0 → a • P ≠ 0
Q : R[X]
hQ : Q ∈ {s | s * P = 0 ∧ s ≠ 0}
a : R
ha : a • P = 0
⊢ a = 0

Proof state:
case intro
R : Type u
inst✝ : CommSemiring R
P : R[X]
hP : P ∉ R[X]⁰
h : ∀ (a : R), a ≠ 0 → a • P ≠ 0
Q : R[X]
hQ : Q ∈ {s | s * P = 0 ∧ s ≠ 0}
a : R
ha : a • P = 0
⊢ a = 0

Tactic:
contrapose! ha

Result:
case intro
R : Type u
inst✝ : CommSemiring R
P : R[X]
hP : P ∉ R[X]⁰
h : ∀ (a : R), a ≠ 0 → a • P ≠ 0
Q : R[X]
hQ : Q ∈ {s | s * P = 0 ∧ s ≠ 0}
a : R
ha : a ≠ 0
⊢ a • P ≠ 0

Proof state:
R : Type u
inst✝ : CommSemiring R
P : R[X]
hP : P ∉ R[X]⁰
⊢ ∃ a, a ≠ 0 ∧ a • P = 0

Tactic:
by_contra! h

Result:
R : Type u
inst✝ : CommSemiring R
P : R[X]
hP : P ∉ R[X]⁰
h : ∀ (a : R), a ≠ 0 → a • P ≠ 0
⊢ False

Proof state:
R : Type u
inst✝ : CommSemiring R
P : R[X]
⊢ P ∉ R[X]⁰ ↔ ∃ a, a ≠ 0 ∧ a • P = 0

Tactic:
refine ⟨fun hP ↦ ?_, fun ⟨a, ha, h⟩ h1 ↦ ha <| C_eq_zero.1 <| (h1 _) <| smul_eq_C_mul a ▸ h⟩

Result:
R : Type u
inst✝ : CommSemiring R
P : R[X]
hP : P ∉ R[X]⁰
⊢ ∃ a, a ≠ 0 ∧ a • P = 0

Proof state:
case intro
R : Type u
inst✝ : CommSemiring R
P : R[X]
hP : P ∉ R[X]⁰
h : ∀ (a : R), a ≠ 0 → a • P ≠ 0
Q : R[X]
hQ : Q ∈ {s | s * P = 0 ∧ s ≠ 0}
a : R
ha : a ≠ 0
⊢ a • P ≠ 0

Tactic:
exact h a ha

Result:
no goals