harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem nodalWeight_ne_zero (hvs : Set.InjOn v s) (hi : i ∈ s) : nodalWeight s v i ≠ 0

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
hj : j ∈ s.erase i
⊢ (v i - v j)⁻¹ ≠ 0

Tactic:
rcases mem_erase.mp hj with ⟨hij, hj⟩

Result:
case intro
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
hj✝ : j ∈ s.erase i
hij : j ≠ i
hj : j ∈ s
⊢ (v i - v j)⁻¹ ≠ 0

Proof state:
case intro
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
hj✝ : j ∈ s.erase i
hij : j ≠ i
hj : j ∈ s
⊢ (v i - v j)⁻¹ ≠ 0

Tactic:
exact inv_ne_zero (sub_ne_zero_of_ne (mt (hvs.eq_iff hi hj).mp hij.symm))

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ nodalWeight s v i ≠ 0

Tactic:
rw [nodalWeight, prod_ne_zero_iff]

Result:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ ∀ a ∈ s.erase i, (v i - v a)⁻¹ ≠ 0

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ ∀ a ∈ s.erase i, (v i - v a)⁻¹ ≠ 0

Tactic:
intro j hj

Result:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
hj : j ∈ s.erase i
⊢ (v i - v j)⁻¹ ≠ 0
-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem AffineIndependent.not_mem_affineSpan_diff [Nontrivial k] {p : ι → P}
    (ha : AffineIndependent k p) (i : ι) (s : Set ι) : p i ∉ affineSpan k (p '' (s \ {i}))

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
i : ι
s : Set ι
⊢ p i ∉ affineSpan k (p '' (s \ {i}))

Tactic:
simp [ha]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem himp_left_comm (a b c : α) : a ⇨ b ⇨ c = b ⇨ a ⇨ c

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ a ⇨ b ⇨ c = b ⇨ a ⇨ c

Tactic:
simp_rw [himp_himp, inf_comm]

Result:
no goals
-- Mathlib/Combinatorics/Schnirelmann.lean
lemma schnirelmannDensity_le_div {n : ℕ} (hn : n ≠ 0) :
    schnirelmannDensity A ≤ #{a ∈ Ioc 0 n | a ∈ A} / n :=
  ciInf_le ⟨0, fun _ ⟨_, hx⟩ => hx ▸ by positivity⟩ (⟨n, hn.bot_lt⟩ : {n : ℕ // 0 < n})

Proof state:
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
n : ℕ
hn : n ≠ 0
x✝¹ : ℝ
x✝ : x✝¹ ∈ Set.range fun n => ↑(#(filter (fun a => a ∈ A) (Ioc 0 ↑n))) / ↑↑n
w✝ : { n // 0 < n }
hx : (fun n => ↑(#(filter (fun a => a ∈ A) (Ioc 0 ↑n))) / ↑↑n) w✝ = x✝¹
⊢ 0 ≤ (fun n => ↑(#(filter (fun a => a ∈ A) (Ioc 0 ↑n))) / ↑↑n) w✝

Tactic:
positivity

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
lemma det_mulLeft (a : R) : (mulLeft R a).det = a

Proof state:
R : Type u_1
inst✝ : CommRing R
a : R
⊢ LinearMap.det (mulLeft R a) = a

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Killing.lean
lemma root_apply_coroot {α : Weight K H L} (hα : α.IsNonZero) :
    α (coroot α) = 2

Proof state:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
⊢ α (coroot α) = 2

Tactic:
rw [← Weight.coe_coe]

Result:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
⊢ (Weight.toLinear K (↥H) L α) (coroot α) = 2

Proof state:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
⊢ (Weight.toLinear K (↥H) L α) (coroot α) = 2

Tactic:
simpa [coroot] using inv_mul_cancel₀ (root_apply_cartanEquivDual_symm_ne_zero hα)

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/WellOrderInductionData.lean
lemma sectionsMk_val_op_bot (val₀ : F.obj (op ⊥)) :
    (d.sectionsMk val₀).val (op ⊥) = val₀

Proof state:
J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
val₀ : F.obj (op ⊥)
⊢ ↑(d.sectionsMk val₀) (op ⊥) = val₀

Tactic:
simpa using (default : d.Extension val₀ ⊥).map_zero

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem ae_restrict_iff₀ {p : α → Prop} (hp : NullMeasurableSet { x | p x } (μ.restrict s)) :
    (∀ᵐ x ∂μ.restrict s, p x) ↔ ∀ᵐ x ∂μ, x ∈ s → p x

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hp : NullMeasurableSet {x | p x} (μ.restrict s)
⊢ (∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → p x

Tactic:
simp only [ae_iff, ← compl_setOf, Measure.restrict_apply₀ hp.compl]

Result:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hp : NullMeasurableSet {x | p x} (μ.restrict s)
⊢ μ ({x | p x}ᶜ ∩ s) = 0 ↔ μ {x | x ∈ s → p x}ᶜ = 0

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hp : NullMeasurableSet {x | p x} (μ.restrict s)
⊢ μ ({x | p x}ᶜ ∩ s) = 0 ↔ μ {x | x ∈ s → p x}ᶜ = 0

Tactic:
rw [iff_iff_eq]

Result:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hp : NullMeasurableSet {x | p x} (μ.restrict s)
⊢ (μ ({x | p x}ᶜ ∩ s) = 0) = (μ {x | x ∈ s → p x}ᶜ = 0)

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hp : NullMeasurableSet {x | p x} (μ.restrict s)
⊢ (μ ({x | p x}ᶜ ∩ s) = 0) = (μ {x | x ∈ s → p x}ᶜ = 0)

Tactic:
congr with x

Result:
case e_a.h.e_6.h.h
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hp : NullMeasurableSet {x | p x} (μ.restrict s)
x : α
⊢ x ∈ {x | p x}ᶜ ∩ s ↔ x ∈ {x | x ∈ s → p x}ᶜ

Proof state:
case e_a.h.e_6.h.h
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
hp : NullMeasurableSet {x | p x} (μ.restrict s)
x : α
⊢ x ∈ {x | p x}ᶜ ∩ s ↔ x ∈ {x | x ∈ s → p x}ᶜ

Tactic:
simp [and_comm]

Result:
no goals
-- Mathlib/Data/Nat/Prime/Defs.lean
theorem minFac_le_of_dvd {n : ℕ} : ∀ {m : ℕ}, 2 ≤ m → m ∣ n → minFac n ≤ m

Proof state:
n : ℕ
⊢ ∀ {m : ℕ}, 2 ≤ m → m ∣ n → n.minFac ≤ m

Tactic:
by_cases n1 : n = 1

Result:
case pos
n m✝ : ℕ
n1 : n = 1
⊢ 2 ≤ m✝ → m✝ ∣ n → n.minFac ≤ m✝

case neg
n m✝ : ℕ
n1 : ¬n = 1
⊢ 2 ≤ m✝ → m✝ ∣ n → n.minFac ≤ m✝

Proof state:
case neg
n m✝ : ℕ
n1 : ¬n = 1
⊢ 2 ≤ m✝ → m✝ ∣ n → n.minFac ≤ m✝

Tactic:
apply (minFac_has_prop n1).2.2

Result:
no goals

Proof state:
case pos
n m✝ : ℕ
n1 : n = 1
⊢ 2 ≤ m✝ → m✝ ∣ n → n.minFac ≤ m✝

Tactic:
exact fun m2 _ => n1.symm ▸ le_trans (by simp) m2

Result:
no goals

Proof state:
n m✝ : ℕ
n1 : n = 1
m2 : 2 ≤ m✝
x✝ : m✝ ∣ n
⊢ minFac 1 ≤ 2

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem HasFDerivAt.comp_hasDerivAt_of_eq
    (hl : HasFDerivAt l l' y) (hf : HasDerivAt f f' x) (hy : y = f x) :
    HasDerivAt (l ∘ f) (l' f') 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
f : 𝕜 → F
f' : F
x : 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
hl : HasFDerivAt l l' (f x)
hf : HasDerivAt f f' x
hy : y = f x
⊢ HasDerivAt (l ∘ f) (l' f') x

Tactic:
exact hl.comp_hasDerivAt x hf

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
hl : HasFDerivAt l l' y
hf : HasDerivAt f f' x
hy : y = f x
⊢ HasDerivAt (l ∘ f) (l' f') x

Tactic:
rw [hy] at hl

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → F
f' : F
x : 𝕜
l : F → E
l' : F →L[𝕜] E
y : F
hl : HasFDerivAt l l' (f x)
hf : HasDerivAt f f' x
hy : y = f x
⊢ HasDerivAt (l ∘ f) (l' f') x
-- Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
theorem snd_app_right (a) : K.ι.app (WalkingMultispan.left a) = I.snd a ≫ K.π _

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
a : J.L
⊢ I.multispan.map (WalkingMultispan.Hom.snd a) ≫ K.ι.app (WalkingMultispan.right (J.snd a)) = I.snd a ≫ K.π (J.snd a)

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
a : J.L
⊢ K.ι.app (WalkingMultispan.left a) = I.snd a ≫ K.π (J.snd a)

Tactic:
rw [← K.w (WalkingMultispan.Hom.snd a)]

Result:
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
a : J.L
⊢ I.multispan.map (WalkingMultispan.Hom.snd a) ≫ K.ι.app (WalkingMultispan.right (J.snd a)) = I.snd a ≫ K.π (J.snd a)
-- Mathlib/Data/Set/Prod.lean
theorem exists_prod_set {p : α × β → Prop} : (∃ x ∈ s ×ˢ t, p x) ↔ ∃ x ∈ s, ∃ y ∈ t, p (x, y)

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
p : α × β → Prop
⊢ (∃ x ∈ s ×ˢ t, p x) ↔ ∃ x ∈ s, ∃ y ∈ t, p (x, y)

Tactic:
simp [and_assoc]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem upperClosure_prod (s : Set α) (t : Set β) :
    upperClosure (s ×ˢ t) = upperClosure s ×ˢ upperClosure t

Proof state:
case a.h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
x✝ : α × β
⊢ x✝ ∈ ↑(upperClosure (s ×ˢ t)) ↔ x✝ ∈ ↑(upperClosure s ×ˢ upperClosure t)

Tactic:
simp [Prod.le_def, @and_and_and_comm _ (_ ∈ t)]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
⊢ upperClosure (s ×ˢ t) = upperClosure s ×ˢ upperClosure t

Tactic:
ext

Result:
case a.h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
x✝ : α × β
⊢ x✝ ∈ ↑(upperClosure (s ×ˢ t)) ↔ x✝ ∈ ↑(upperClosure s ×ˢ upperClosure t)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem exists_push {xs : Vector α (n + 1)} :
    ∃ (ys : Vector α n) (a : α), xs = ys.push a

Proof state:
case mk.intro.intro
α : Type u_1
n : Nat
xs : Array α
w : xs.size = n + 1
ys : Array α
a : α
h : xs = ys.push a
⊢ ∃ ys a, { toArray := xs, size_toArray := w } = ys.push a

Tactic:
exact ⟨⟨ys, by simp_all⟩, a, toArray_inj.1 h⟩

Result:
no goals

Proof state:
α : Type u_1
n : Nat
xs : Array α
w : xs.size = n + 1
ys : Array α
a : α
h : xs = ys.push a
⊢ ys.size = n

Tactic:
simp_all

Result:
no goals

Proof state:
case mk
α : Type u_1
n : Nat
xs : Array α
w : xs.size = n + 1
⊢ ∃ ys a, { toArray := xs, size_toArray := w } = ys.push a

Tactic:
obtain ⟨ys, a, h⟩ := Array.exists_push_of_size_eq_add_one w

Result:
case mk.intro.intro
α : Type u_1
n : Nat
xs : Array α
w : xs.size = n + 1
ys : Array α
a : α
h : xs = ys.push a
⊢ ∃ ys a, { toArray := xs, size_toArray := w } = ys.push a

Proof state:
α : Type u_1
n : Nat
xs : Vector α (n + 1)
⊢ ∃ ys a, xs = ys.push a

Tactic:
rcases xs with ⟨xs, w⟩

Result:
case mk
α : Type u_1
n : Nat
xs : Array α
w : xs.size = n + 1
⊢ ∃ ys a, { toArray := xs, size_toArray := w } = ys.push a
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem decide_eq_true_iff {p : Prop} [Decidable p] : (decide p = true) ↔ p

Proof state:
p : Prop
inst✝ : Decidable p
⊢ decide p = true ↔ p

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
theorem coeff_weightedHomogeneousComponent [DecidableEq M] (d : σ →₀ ℕ) :
    coeff d (weightedHomogeneousComponent w n φ) =
      if weight w d = n then coeff d φ else 0 :=
  letI := Classical.decEq M
  Finsupp.filter_apply (fun d : σ →₀ ℕ => weight w d = n) φ d |>.trans <| by convert rfl

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
inst✝¹ : AddCommMonoid M
w : σ → M
n : M
φ : MvPolynomial σ R
inst✝ : DecidableEq M
d : σ →₀ ℕ
this : DecidableEq M := Classical.decEq M
⊢ (if (weight w) d = n then φ d else 0) = if (weight w) d = n then coeff d φ else 0

Tactic:
convert rfl

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem add_mulVec [Fintype n] (A B : Matrix m n α) (x : n → α) :
    (A + B) *ᵥ x = A *ᵥ x + B *ᵥ x

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
A B : Matrix m n α
x : n → α
⊢ (A + B) *ᵥ x = A *ᵥ x + B *ᵥ x

Tactic:
ext

Result:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
A B : Matrix m n α
x : n → α
x✝ : m
⊢ ((A + B) *ᵥ x) x✝ = (A *ᵥ x + B *ᵥ x) x✝

Proof state:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
A B : Matrix m n α
x : n → α
x✝ : m
⊢ ((A + B) *ᵥ x) x✝ = (A *ᵥ x + B *ᵥ x) x✝

Tactic:
apply add_dotProduct

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma lintegral_density (hκν : fst κ ≤ ν) [IsFiniteKernel ν]
    (a : α) {s : Set β} (hs : MeasurableSet s) :
    ∫⁻ x, ENNReal.ofReal (density κ ν a x s) ∂(ν a) = κ a (univ ×ˢ s)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (x : γ), ENNReal.ofReal (κ.density ν a x s) ∂ν a = (κ a) (univ ×ˢ s)

Tactic:
rw [← setLIntegral_univ]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (x : γ) in univ, ENNReal.ofReal (κ.density ν a x s) ∂ν a = (κ a) (univ ×ˢ s)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (x : γ) in univ, ENNReal.ofReal (κ.density ν a x s) ∂ν a = (κ a) (univ ×ˢ s)

Tactic:
exact setLIntegral_density hκν a hs MeasurableSet.univ

Result:
no goals
-- Mathlib/Data/Rat/Cast/Order.lean
@[simp] lemma cast_lt_zero : (q : K) < 0 ↔ q < 0

Proof state:
q : ℚ
K : Type u_5
inst✝ : LinearOrderedField K
⊢ ↑q < 0 ↔ q < 0

Tactic:
norm_cast

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem cyclotomic'_splits (n : ℕ) : Splits (RingHom.id K) (cyclotomic' n K)

Proof state:
K : Type u_1
inst✝ : Field K
n : ℕ
⊢ Splits (RingHom.id K) (cyclotomic' n K)

Tactic:
apply splits_prod (RingHom.id K)

Result:
K : Type u_1
inst✝ : Field K
n : ℕ
⊢ ∀ j ∈ primitiveRoots n K, Splits (RingHom.id K) (X - C j)

Proof state:
K : Type u_1
inst✝ : Field K
n : ℕ
z : K
a✝ : z ∈ primitiveRoots n K
⊢ Splits (RingHom.id K) (X - C z)

Tactic:
simp only [splits_X_sub_C (RingHom.id K)]

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
n : ℕ
⊢ ∀ j ∈ primitiveRoots n K, Splits (RingHom.id K) (X - C j)

Tactic:
intro z _

Result:
K : Type u_1
inst✝ : Field K
n : ℕ
z : K
a✝ : z ∈ primitiveRoots n K
⊢ Splits (RingHom.id K) (X - C z)
-- Mathlib/Algebra/Order/Hom/Monoid.lean
theorem cancel_right {g₁ g₂ : β →*o γ} {f : α →*o β} (hf : Function.Surjective f) :
    g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
  ⟨fun h => ext <| hf.forall.2 <| DFunLike.ext_iff.1 h, fun _ => by congr⟩

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MulOneClass γ
g₁ g₂ : β →*o γ
f : α →*o β
hf : Surjective ⇑f
x✝ : g₁ = g₂
⊢ g₁.comp f = g₂.comp f

Tactic:
congr

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma _root_.NumberField.ComplexEmbedding.IsConj.isUnramified_mk_iff
    {φ : K →+* ℂ} (h : ComplexEmbedding.IsConj φ σ) :
    IsUnramified k (mk φ) ↔ σ = 1

Proof state:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
σ : K ≃ₐ[k] K
φ : K →+* ℂ
h : ComplexEmbedding.IsConj φ σ
⊢ IsUnramified k (mk φ) ↔ σ = 1

Tactic:
rw [h.ext_iff, ComplexEmbedding.isConj_one_iff, ← not_iff_not, not_isUnramified_iff,
  ← not_isReal_iff_isComplex, comap_mk, isReal_mk_iff, isReal_mk_iff, eq_true h.isReal_comp,
  and_true]

Result:
no goals
-- Mathlib/GroupTheory/FreeAbelianGroupFinsupp.lean
theorem Finsupp.toFreeAbelianGroup_toFinsupp {X} (x : FreeAbelianGroup X) :
    Finsupp.toFreeAbelianGroup (FreeAbelianGroup.toFinsupp x) = x

Proof state:
X : Type u_2
x : FreeAbelianGroup X
⊢ toFreeAbelianGroup (toFinsupp x) = x

Tactic:
rw [← AddMonoidHom.comp_apply, Finsupp.toFreeAbelianGroup_comp_toFinsupp, AddMonoidHom.id_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKeyD_insertMany_empty_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
    {l : List ((a : α) × β a)} {k fallback : α}
    (h : (l.map Sigma.fst).contains k = false) :
    (insertMany empty l).1.getKeyD k fallback = fallback

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
k fallback : α
h : (List.map Sigma.fst l).contains k = false
⊢ empty.getKeyD k fallback = fallback

Tactic:
apply getKeyD_empty

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
k fallback : α
h : (List.map Sigma.fst l).contains k = false
⊢ (empty.insertMany l).val.getKeyD k fallback = fallback

Tactic:
rw [getKeyD_insertMany_list_of_contains_eq_false _ Raw.WF.empty₀ h]

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
k fallback : α
h : (List.map Sigma.fst l).contains k = false
⊢ empty.getKeyD k fallback = fallback
-- Mathlib/Data/Finset/Option.lean
theorem eraseNone_union [DecidableEq (Option α)] [DecidableEq α] (s t : Finset (Option α)) :
    eraseNone (s ∪ t) = eraseNone s ∪ eraseNone t

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq (Option α)
inst✝ : DecidableEq α
s t : Finset (Option α)
a✝ : α
⊢ a✝ ∈ eraseNone (s ∪ t) ↔ a✝ ∈ eraseNone s ∪ eraseNone t

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq (Option α)
inst✝ : DecidableEq α
s t : Finset (Option α)
⊢ eraseNone (s ∪ t) = eraseNone s ∪ eraseNone t

Tactic:
ext

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq (Option α)
inst✝ : DecidableEq α
s t : Finset (Option α)
a✝ : α
⊢ a✝ ∈ eraseNone (s ∪ t) ↔ a✝ ∈ eraseNone s ∪ eraseNone t
-- Mathlib/Combinatorics/SimpleGraph/Trails.lean
theorem IsEulerian.edgesFinset_eq [Fintype G.edgeSet] {u v : V} {p : G.Walk u v}
    (h : p.IsEulerian) : h.isTrail.edgesFinset = G.edgeFinset

Proof state:
case h
V : Type u_1
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : Fintype ↑G.edgeSet
u v : V
p : G.Walk u v
h : p.IsEulerian
e : Sym2 V
⊢ e ∈ ⋯.edgesFinset ↔ e ∈ G.edgeFinset

Tactic:
simp [h.mem_edges_iff]

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : Fintype ↑G.edgeSet
u v : V
p : G.Walk u v
h : p.IsEulerian
⊢ ⋯.edgesFinset = G.edgeFinset

Tactic:
ext e

Result:
case h
V : Type u_1
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : Fintype ↑G.edgeSet
u v : V
p : G.Walk u v
h : p.IsEulerian
e : Sym2 V
⊢ e ∈ ⋯.edgesFinset ↔ e ∈ G.edgeFinset
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem derivWithin.scomp_of_eq (hg : DifferentiableWithinAt 𝕜' g₁ t' y)
    (hh : DifferentiableWithinAt 𝕜 h s x) (hs : MapsTo h s t')
    (hy : y = h x) :
    derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
t' : Set 𝕜'
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
y : 𝕜'
hg : DifferentiableWithinAt 𝕜' g₁ t' (h x)
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s t'
hy : y = h x
⊢ derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)

Tactic:
exact derivWithin.scomp x hg hh hs

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
t' : Set 𝕜'
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
y : 𝕜'
hg : DifferentiableWithinAt 𝕜' g₁ t' y
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s t'
hy : y = h x
⊢ derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)

Tactic:
rw [hy] at hg

Result:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
t' : Set 𝕜'
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
y : 𝕜'
hg : DifferentiableWithinAt 𝕜' g₁ t' (h x)
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s t'
hy : y = h x
⊢ derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_induction {f : α → M} (p : M → Prop) (hp₀ : p 1)
    (hp₁ : ∀ x y, p x → p y → p (x * y)) (hp₂ : ∀ i, p (f i)) : p (∏ᶠ i, f i)

Proof state:
case pos
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
h✝ : (mulSupport ((fun i => f i) ∘ PLift.down)).Finite
⊢ p (∏ i ∈ h✝.toFinset, f i.down)

case neg
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
h✝ : ¬(mulSupport ((fun i => f i) ∘ PLift.down)).Finite
⊢ p 1

Tactic:
exacts [Finset.prod_induction _ _ hp₁ hp₀ fun i _ => hp₂ _, hp₀]

Result:
no goals

Proof state:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
⊢ p (if h : (mulSupport ((fun i => f i) ∘ PLift.down)).Finite then ∏ i ∈ h.toFinset, f i.down else 1)

Tactic:
split_ifs

Result:
case pos
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
h✝ : (mulSupport ((fun i => f i) ∘ PLift.down)).Finite
⊢ p (∏ i ∈ h✝.toFinset, f i.down)

case neg
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
h✝ : ¬(mulSupport ((fun i => f i) ∘ PLift.down)).Finite
⊢ p 1

Proof state:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
⊢ p (∏ᶠ (i : α), f i)

Tactic:
rw [finprod]

Result:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
p : M → Prop
hp₀ : p 1
hp₁ : ∀ (x y : M), p x → p y → p (x * y)
hp₂ : ∀ (i : α), p (f i)
⊢ p (if h : (mulSupport ((fun i => f i) ∘ PLift.down)).Finite then ∏ i ∈ h.toFinset, f i.down else 1)