harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma C_Ψ₂Sq : C W.Ψ₂Sq = W.ψ₂ ^ 2 - 4 * W.toAffine.polynomial

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ 4 * C X ^ 3 + (C (C W.a₁) ^ 2 + 4 * C (C W.a₂)) * C X ^ 2 + 2 * (2 * C (C W.a₄) + C (C W.a₁) * C (C W.a₃)) * C X +
      (C (C W.a₃) ^ 2 + 4 * C (C W.a₆)) =
    (2 * Y + (C (C W.toAffine.a₁) * C X + C (C W.toAffine.a₃))) ^ 2 -
      4 *
        (Y ^ 2 + (C (C W.toAffine.a₁) * C X + C (C W.toAffine.a₃)) * Y -
          (C X ^ 3 + C (C W.toAffine.a₂) * C X ^ 2 + C (C W.toAffine.a₄) * C X + C (C W.toAffine.a₆)))

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ C W.Ψ₂Sq = W.ψ₂ ^ 2 - 4 * W.toAffine.polynomial

Tactic:
rw [Ψ₂Sq, ψ₂, b₂, b₄, b₆, Affine.polynomialY, Affine.polynomial]

Result:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ C (C 4 * X ^ 3 + C (W.a₁ ^ 2 + 4 * W.a₂) * X ^ 2 + C (2 * (2 * W.a₄ + W.a₁ * W.a₃)) * X + C (W.a₃ ^ 2 + 4 * W.a₆)) =
    (C (C 2) * Y + C (C W.toAffine.a₁ * X + C W.toAffine.a₃)) ^ 2 -
      4 *
        (Y ^ 2 + C (C W.toAffine.a₁ * X + C W.toAffine.a₃) * Y -
          C (X ^ 3 + C W.toAffine.a₂ * X ^ 2 + C W.toAffine.a₄ * X + C W.toAffine.a₆))

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ C (C 4 * X ^ 3 + C (W.a₁ ^ 2 + 4 * W.a₂) * X ^ 2 + C (2 * (2 * W.a₄ + W.a₁ * W.a₃)) * X + C (W.a₃ ^ 2 + 4 * W.a₆)) =
    (C (C 2) * Y + C (C W.toAffine.a₁ * X + C W.toAffine.a₃)) ^ 2 -
      4 *
        (Y ^ 2 + C (C W.toAffine.a₁ * X + C W.toAffine.a₃) * Y -
          C (X ^ 3 + C W.toAffine.a₂ * X ^ 2 + C W.toAffine.a₄ * X + C W.toAffine.a₆))

Tactic:
C_simp

Result:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ 4 * C X ^ 3 + (C (C W.a₁) ^ 2 + 4 * C (C W.a₂)) * C X ^ 2 + 2 * (2 * C (C W.a₄) + C (C W.a₁) * C (C W.a₃)) * C X +
      (C (C W.a₃) ^ 2 + 4 * C (C W.a₆)) =
    (2 * Y + (C (C W.toAffine.a₁) * C X + C (C W.toAffine.a₃))) ^ 2 -
      4 *
        (Y ^ 2 + (C (C W.toAffine.a₁) * C X + C (C W.toAffine.a₃)) * Y -
          (C X ^ 3 + C (C W.toAffine.a₂) * C X ^ 2 + C (C W.toAffine.a₄) * C X + C (C W.toAffine.a₆)))
-- Mathlib/Algebra/MonoidAlgebra/Defs.lean
theorem prod_single [CommSemiring k] [AddCommMonoid G] {s : Finset ι} {a : ι → G} {b : ι → k} :
    (∏ i ∈ s, single (a i) (b i)) = single (∑ i ∈ s, a i) (∏ i ∈ s, b i) :=
  Finset.cons_induction_on s rfl fun a s has ih => by
    rw [prod_cons has, ih, single_mul_single, sum_cons has, prod_cons has]

Proof state:
k : Type u₁
G : Type u₂
ι : Type ui
inst✝¹ : CommSemiring k
inst✝ : AddCommMonoid G
s✝ : Finset ι
a✝ : ι → G
b : ι → k
a : ι
s : Finset ι
has : a ∉ s
ih : ∏ i ∈ s, single (a✝ i) (b i) = single (∑ i ∈ s, a✝ i) (∏ i ∈ s, b i)
⊢ ∏ i ∈ Finset.cons a s has, single (a✝ i) (b i) =
    single (∑ i ∈ Finset.cons a s has, a✝ i) (∏ i ∈ Finset.cons a s has, b i)

Tactic:
rw [prod_cons has, ih, single_mul_single, sum_cons has, prod_cons has]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean
theorem factors_pow {x : α} (n : ℕ) :
    Multiset.Rel Associated (factors (x ^ n)) (n • factors x)

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
n : ℕ
⊢ Multiset.Rel Associated (factors (x ^ 0)) (0 • factors x)

Tactic:
rw [zero_smul, pow_zero, factors_one, Multiset.rel_zero_right]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : ¬x = 0
⊢ Multiset.Rel Associated (factors (x ^ (n + 1))) ((n + 1) • factors x)

Tactic:
rw [pow_succ', succ_nsmul']

Result:
case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : ¬x = 0
⊢ Multiset.Rel Associated (factors (x * x ^ n)) (factors x + n • factors x)

Proof state:
case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : ¬x = 0
⊢ Multiset.Rel Associated (factors x + factors (x ^ n)) (factors x + n • factors x)

Tactic:
refine Multiset.Rel.add ?_ <| factors_pow n

Result:
case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : ¬x = 0
⊢ Multiset.Rel Associated (factors x) (factors x)

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
⊢ Multiset.Rel Associated (factors (x ^ (n + 1))) ((n + 1) • factors x)

Tactic:
by_cases h0 : x = 0

Result:
case pos
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : x = 0
⊢ Multiset.Rel Associated (factors (x ^ (n + 1))) ((n + 1) • factors x)

case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : ¬x = 0
⊢ Multiset.Rel Associated (factors (x ^ (n + 1))) ((n + 1) • factors x)

Proof state:
case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : ¬x = 0
⊢ Multiset.Rel Associated (factors x) (factors x)

Tactic:
exact Multiset.rel_refl_of_refl_on fun y _ => Associated.refl _

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : x = 0
⊢ Multiset.Rel Associated (factors (x ^ (n + 1))) ((n + 1) • factors x)

Tactic:
simp [h0, zero_pow n.succ_ne_zero, smul_zero]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : ¬x = 0
⊢ Multiset.Rel Associated (factors (x * x ^ n)) (factors x + n • factors x)

Tactic:
refine Multiset.Rel.trans _ (factors_mul h0 (pow_ne_zero n h0)) ?_

Result:
case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : α
n✝ n : ℕ
h0 : ¬x = 0
⊢ Multiset.Rel Associated (factors x + factors (x ^ n)) (factors x + n • factors x)
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_zero : ∫ _ : α, (0 : G) ∂μ = 0

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
hG : CompleteSpace G
⊢ ∫ (x : α), 0 ∂μ = 0

Tactic:
simp only [integral, hG, L1.integral]

Result:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
hG : CompleteSpace G
⊢ (if h : True then if hf : Integrable (fun x => 0) μ then L1.integralCLM (Integrable.toL1 (fun x => 0) hf) else 0
    else 0) =
    0

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
hG : CompleteSpace G
⊢ (if h : True then if hf : Integrable (fun x => 0) μ then L1.integralCLM (Integrable.toL1 (fun x => 0) hf) else 0
    else 0) =
    0

Tactic:
exact setToFun_zero (dominatedFinMeasAdditive_weightedSMul μ)

Result:
no goals

Proof state:
case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
hG : ¬CompleteSpace G
⊢ ∫ (x : α), 0 ∂μ = 0

Tactic:
simp [integral, hG]

Result:
no goals

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
⊢ ∫ (x : α), 0 ∂μ = 0

Tactic:
by_cases hG : CompleteSpace G

Result:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
hG : CompleteSpace G
⊢ ∫ (x : α), 0 ∂μ = 0

case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
hG : ¬CompleteSpace G
⊢ ∫ (x : α), 0 ∂μ = 0
-- Mathlib/Topology/Instances/RatLemmas.lean
theorem not_secondCountableTopology_opc : ¬SecondCountableTopology ℚ∞

Proof state:
a✝ : SecondCountableTopology ℚ∞
⊢ False

Tactic:
exact not_firstCountableTopology_opc inferInstance

Result:
no goals

Proof state:
⊢ ¬SecondCountableTopology ℚ∞

Tactic:
intro

Result:
a✝ : SecondCountableTopology ℚ∞
⊢ False
-- Mathlib/Data/NNReal/Defs.lean
theorem Real.exists_lt_of_strictMono [h : Nontrivial Γ₀ˣ] {f : Γ₀ →*₀ ℝ≥0} (hf : StrictMono f)
    {r : ℝ} (hr : 0 < r) : ∃ d : Γ₀ˣ, (f d : ℝ) < r

Proof state:
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ
hr : 0 < r
s : ℝ≥0 := ⟨r, ⋯⟩
⊢ ∃ d, ↑(f ↑d) < r

Tactic:
have hs : 0 < s := hr

Result:
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ
hr : 0 < r
s : ℝ≥0 := ⟨r, ⋯⟩
hs : 0 < s
⊢ ∃ d, ↑(f ↑d) < r

Proof state:
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ
hr : 0 < r
⊢ ∃ d, ↑(f ↑d) < r

Tactic:
set s : NNReal := ⟨r, le_of_lt hr⟩

Result:
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ
hr : 0 < r
s : ℝ≥0 := ⟨r, ⋯⟩
⊢ ∃ d, ↑(f ↑d) < r

Proof state:
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ
hr : 0 < r
s : ℝ≥0 := ⟨r, ⋯⟩
hs : 0 < s
⊢ ∃ d, ↑(f ↑d) < r

Tactic:
exact NNReal.exists_lt_of_strictMono hf hs

Result:
no goals
-- Mathlib/Data/Part.lean
theorem bind_toOption (f : α → Part β) (o : Part α) [Decidable o.Dom] [∀ a, Decidable (f a).Dom]
    [Decidable (o.bind f).Dom] :
    (o.bind f).toOption = o.toOption.elim Option.none fun a => (f a).toOption

Proof state:
case neg
α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (o.bind f).Dom
h : ¬o.Dom
⊢ (o.bind f).toOption = Option.none.elim Option.none fun a => (f a).toOption

Tactic:
exact Part.toOption_eq_none_iff.2 fun ho => h ho.of_bind

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (o.bind f).Dom
⊢ (o.bind f).toOption = o.toOption.elim Option.none fun a => (f a).toOption

Tactic:
by_cases h : o.Dom

Result:
case pos
α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (o.bind f).Dom
h : o.Dom
⊢ (o.bind f).toOption = o.toOption.elim Option.none fun a => (f a).toOption

case neg
α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (o.bind f).Dom
h : ¬o.Dom
⊢ (o.bind f).toOption = o.toOption.elim Option.none fun a => (f a).toOption

Proof state:
case neg
α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (o.bind f).Dom
h : ¬o.Dom
⊢ (o.bind f).toOption = o.toOption.elim Option.none fun a => (f a).toOption

Tactic:
rw [Part.toOption_eq_none_iff.2 h]

Result:
case neg
α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (o.bind f).Dom
h : ¬o.Dom
⊢ (o.bind f).toOption = Option.none.elim Option.none fun a => (f a).toOption

Proof state:
case pos
α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (o.bind f).Dom
h : o.Dom
⊢ (f (o.get h)).toOption = (Option.some (o.get h)).elim Option.none fun a => (f a).toOption

Tactic:
rfl

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (o.bind f).Dom
h : o.Dom
⊢ (o.bind f).toOption = o.toOption.elim Option.none fun a => (f a).toOption

Tactic:
simp_rw [h.toOption, h.bind]

Result:
case pos
α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (o.bind f).Dom
h : o.Dom
⊢ (f (o.get h)).toOption = (Option.some (o.get h)).elim Option.none fun a => (f a).toOption
-- Mathlib/Algebra/Order/Antidiag/Nat.lean
theorem primeFactorsPiBij_img (d n : ℕ) (hn : Squarefree n)
  (f : (p : ℕ) → p ∈ n.primeFactors → Fin d) (hf : f ∈ pi n.primeFactors fun _ => univ) :
    Nat.primeFactorsPiBij d n f hf ∈ finMulAntidiag d n

Proof state:
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
⊢ ∏ i : Fin d, ∏ p ∈ filter (fun p => f ↑p ⋯ = i) n.primeFactors.attach, ↑p = n

Tactic:
rw [prod_fiberwise_of_maps_to, prod_attach (f := fun x => x)]

Result:
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
⊢ ∏ x ∈ n.primeFactors, x = n

case h
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
⊢ ∀ i ∈ n.primeFactors.attach, f ↑i ⋯ ∈ univ

Proof state:
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
⊢ Nat.primeFactorsPiBij d n f hf ∈ d.finMulAntidiag n

Tactic:
rw [mem_finMulAntidiag]

Result:
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
⊢ ∏ i : Fin d, Nat.primeFactorsPiBij d n f hf i = n ∧ n ≠ 0

Proof state:
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
⊢ ∏ i : Fin d, Nat.primeFactorsPiBij d n f hf i = n

Tactic:
unfold Nat.primeFactorsPiBij

Result:
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
⊢ ∏ i : Fin d, ∏ p ∈ filter (fun p => f ↑p ⋯ = i) n.primeFactors.attach, ↑p = n

Proof state:
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
⊢ ∏ i : Fin d, Nat.primeFactorsPiBij d n f hf i = n ∧ n ≠ 0

Tactic:
refine ⟨?_, hn.ne_zero⟩

Result:
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
⊢ ∏ i : Fin d, Nat.primeFactorsPiBij d n f hf i = n

Proof state:
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
⊢ ∏ x ∈ n.primeFactors, x = n

Tactic:
apply prod_primeFactors_of_squarefree hn

Result:
no goals

Proof state:
case h
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
⊢ ∀ i ∈ n.primeFactors.attach, f ↑i ⋯ ∈ univ

Tactic:
apply fun _ _ => mem_univ _

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/SmallDegree.lean
theorem degree_cubic (ha : a ≠ 0) : degree (C a * X ^ 3 + C b * X ^ 2 + C c * X + C d) = 3

Proof state:
R : Type u
a b c d : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a * X ^ 3 + C b * X ^ 2 + C c * X + C d).degree = 3

Tactic:
rw [add_assoc, add_assoc, ← add_assoc (C b * X ^ 2),
  degree_add_eq_left_of_degree_lt <| degree_quadratic_lt_degree_C_mul_X_cb ha,
  degree_C_mul_X_pow 3 ha]

Result:
R : Type u
a b c d : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ ↑3 = 3

Proof state:
R : Type u
a b c d : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ ↑3 = 3

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean
theorem liftIsometry_apply_apply (f : ContinuousMultilinearMap 𝕜 E F) (x : ⨂[𝕜] i, E i) :
    liftIsometry 𝕜 E F f x = lift f.toMultilinearMap x

Proof state:
ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
F : Type uF
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ContinuousMultilinearMap 𝕜 E F
x : ⨂[𝕜] (i : ι), E i
⊢ ((liftIsometry 𝕜 E F) f) x = (lift f.toMultilinearMap) x

Tactic:
simp only [liftIsometry, LinearIsometryEquiv.coe_mk, liftEquiv_apply,
  LinearMap.mkContinuous_apply]

Result:
no goals
-- Mathlib/NumberTheory/Fermat.lean
theorem pow_of_pow_add_prime {a n : ℕ} (ha : 1 < a) (hn : n ≠ 0) (hP : (a ^ n + 1).Prime) :
    ∃ m : ℕ, n = 2 ^ m

Proof state:
case h
a k m : ℕ
hm : Odd m
hn : 2 ^ k * m ≠ 0
hP : Prime ((a ^ 2 ^ k) ^ m + 1)
ha : 1 < a ^ 2 ^ k
⊢ 2 ^ k * m = 2 ^ k

Tactic:
let h := hm.nat_add_dvd_pow_add_pow (a ^ 2 ^ k) 1

Result:
case h
a k m : ℕ
hm : Odd m
hn : 2 ^ k * m ≠ 0
hP : Prime ((a ^ 2 ^ k) ^ m + 1)
ha : 1 < a ^ 2 ^ k
h : a ^ 2 ^ k + 1 ∣ (a ^ 2 ^ k) ^ m + 1 ^ m := Odd.nat_add_dvd_pow_add_pow (a ^ 2 ^ k) 1 hm
⊢ 2 ^ k * m = 2 ^ k

Proof state:
a n : ℕ
ha : 1 < a
hn : n ≠ 0
hP : Prime (a ^ n + 1)
⊢ ∃ m, n = 2 ^ m

Tactic:
obtain ⟨k, m, hm, rfl⟩ := exists_eq_two_pow_mul_odd hn

Result:
case intro.intro.intro
a : ℕ
ha : 1 < a
k m : ℕ
hm : Odd m
hn : 2 ^ k * m ≠ 0
hP : Prime (a ^ (2 ^ k * m) + 1)
⊢ ∃ m_1, 2 ^ k * m = 2 ^ m_1

Proof state:
case intro.intro.intro
a : ℕ
ha : 1 < a
k m : ℕ
hm : Odd m
hn : 2 ^ k * m ≠ 0
hP : Prime (a ^ (2 ^ k * m) + 1)
⊢ ∃ m_1, 2 ^ k * m = 2 ^ m_1

Tactic:
rw [pow_mul] at hP

Result:
case intro.intro.intro
a : ℕ
ha : 1 < a
k m : ℕ
hm : Odd m
hn : 2 ^ k * m ≠ 0
hP : Prime ((a ^ 2 ^ k) ^ m + 1)
⊢ ∃ m_1, 2 ^ k * m = 2 ^ m_1

Proof state:
case h
a : ℕ
ha : 1 < a
k m : ℕ
hm : Odd m
hn : 2 ^ k * m ≠ 0
hP : Prime ((a ^ 2 ^ k) ^ m + 1)
⊢ 2 ^ k * m = 2 ^ k

Tactic:
replace ha : 1 < a ^ 2 ^ k := one_lt_pow (pow_ne_zero k two_ne_zero) ha

Result:
case h
a k m : ℕ
hm : Odd m
hn : 2 ^ k * m ≠ 0
hP : Prime ((a ^ 2 ^ k) ^ m + 1)
ha : 1 < a ^ 2 ^ k
⊢ 2 ^ k * m = 2 ^ k

Proof state:
case h
a k m : ℕ
hm : Odd m
hn : 2 ^ k * m ≠ 0
hP : Prime ((a ^ 2 ^ k) ^ m + 1)
ha : 1 < a ^ 2 ^ k
h : m = 1
⊢ 2 ^ k * m = 2 ^ k

Tactic:
rw [h, mul_one]

Result:
no goals

Proof state:
case intro.intro.intro
a : ℕ
ha : 1 < a
k m : ℕ
hm : Odd m
hn : 2 ^ k * m ≠ 0
hP : Prime ((a ^ 2 ^ k) ^ m + 1)
⊢ ∃ m_1, 2 ^ k * m = 2 ^ m_1

Tactic:
use k

Result:
case h
a : ℕ
ha : 1 < a
k m : ℕ
hm : Odd m
hn : 2 ^ k * m ≠ 0
hP : Prime ((a ^ 2 ^ k) ^ m + 1)
⊢ 2 ^ k * m = 2 ^ k

Proof state:
case h
a k m : ℕ
hm : Odd m
hn : 2 ^ k * m ≠ 0
hP : Prime ((a ^ 2 ^ k) ^ m + 1)
ha : 1 < a ^ 2 ^ k
h : a ^ 2 ^ k + 1 ∣ (a ^ 2 ^ k) ^ m + 1 ^ m := Odd.nat_add_dvd_pow_add_pow (a ^ 2 ^ k) 1 hm
⊢ 2 ^ k * m = 2 ^ k

Tactic:
rw [one_pow, hP.dvd_iff_eq (Nat.lt_add_right 1 ha).ne', add_left_inj, pow_eq_self_iff ha] at h

Result:
case h
a k m : ℕ
hm : Odd m
hn : 2 ^ k * m ≠ 0
hP : Prime ((a ^ 2 ^ k) ^ m + 1)
ha : 1 < a ^ 2 ^ k
h : m = 1
⊢ 2 ^ k * m = 2 ^ k
-- Mathlib/Data/Finset/Preimage.lean
lemma card_preimage (s : Finset β) (f : α → β) (hf) [DecidablePred (· ∈ Set.range f)] :
    (s.preimage f hf).card = {x ∈ s | x ∈ Set.range f}.card :=
  card_nbij f (by simp) (by simpa) (fun b hb ↦ by aesop)

Proof state:
α : Type u
β : Type v
s : Finset β
f : α → β
hf : InjOn f (f ⁻¹' ↑s)
inst✝ : DecidablePred fun x => x ∈ Set.range f
⊢ ∀ a ∈ s.preimage f hf, f a ∈ filter (fun x => x ∈ Set.range f) s

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : Type v
s : Finset β
f : α → β
hf : InjOn f (f ⁻¹' ↑s)
inst✝ : DecidablePred fun x => x ∈ Set.range f
⊢ InjOn f ↑(s.preimage f hf)

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u
β : Type v
s : Finset β
f : α → β
hf : InjOn f (f ⁻¹' ↑s)
inst✝ : DecidablePred fun x => x ∈ Set.range f
b : β
hb : b ∈ ↑(filter (fun x => x ∈ Set.range f) s)
⊢ b ∈ f '' ↑(s.preimage f hf)

Tactic:
aesop

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem isClosed_sigma_iff {s : Set (Sigma σ)} : IsClosed s ↔ ∀ i, IsClosed (Sigma.mk i ⁻¹' s)

Proof state:
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
s : Set (Sigma σ)
⊢ IsClosed s ↔ ∀ (i : ι), IsClosed (Sigma.mk i ⁻¹' s)

Tactic:
simp only [← isOpen_compl_iff, isOpen_sigma_iff, preimage_compl]

Result:
no goals
-- Mathlib/LinearAlgebra/Projectivization/Subspace.lean
theorem mem_span {S : Set (ℙ K V)} (u : ℙ K V) :
    u ∈ span S ↔ ∀ W : Subspace K V, S ⊆ W → u ∈ W

Proof state:
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
u : ℙ K V
⊢ u ∈ span S ↔ ∀ (W : Subspace K V), S ⊆ ↑W → u ∈ W

Tactic:
simp_rw [← span_le_subspace_iff]

Result:
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
u : ℙ K V
⊢ u ∈ span S ↔ ∀ (W : Subspace K V), span S ≤ W → u ∈ W

Proof state:
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
u : ℙ K V
⊢ u ∈ span S ↔ ∀ (W : Subspace K V), span S ≤ W → u ∈ W

Tactic:
exact ⟨fun hu W hW => hW hu, fun W => W (span S) (le_refl _)⟩

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem fderivWithin_inter (ht : t ∈ 𝓝 x) : fderivWithin 𝕜 f (s ∩ t) x = fderivWithin 𝕜 f s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s t : Set E
ht : t ∈ 𝓝 x
⊢ fderivWithin 𝕜 f (s ∩ t) x = fderivWithin 𝕜 f s x

Tactic:
classical
simp [fderivWithin, hasFDerivWithinAt_inter ht, DifferentiableWithinAt]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s t : Set E
ht : t ∈ 𝓝 x
⊢ fderivWithin 𝕜 f (s ∩ t) x = fderivWithin 𝕜 f s x

Tactic:
simp [fderivWithin, hasFDerivWithinAt_inter ht, DifferentiableWithinAt]

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem dualBasis_equivFun [Finite ι] (l : Dual R M) (i : ι) :
    b.dualBasis.equivFun l i = l (b i)

Proof state:
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
l : Dual R M
i : ι
⊢ b.dualBasis.equivFun l i = l (b i)

Tactic:
rw [Basis.equivFun_apply, dualBasis_repr]

Result:
no goals
-- Mathlib/InformationTheory/KullbackLeibler/Basic.lean
lemma klDiv_ne_top_iff : klDiv μ ν ≠ ∞ ↔ μ ≪ ν ∧ Integrable (llr μ ν) μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
⊢ klDiv μ ν ≠ ⊤ ↔ μ ≪ ν ∧ Integrable (llr μ ν) μ

Tactic:
simp [ne_eq, klDiv_eq_top_iff]

Result:
no goals
-- Mathlib/Order/Partition/Finpartition.lean
theorem atomise_empty (hs : s.Nonempty) : (atomise s ∅).parts = {s}

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
⊢ (atomise s ∅).parts = {s}

Tactic:
simp only [atomise, powerset_empty, image_singleton, not_mem_empty, IsEmpty.forall_iff,
  imp_true_iff, filter_True]

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
⊢ (ofErase {s} ⋯ ⋯).parts = {s}

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
⊢ (ofErase {s} ⋯ ⋯).parts = {s}

Tactic:
exact erase_eq_of_not_mem (not_mem_singleton.2 hs.ne_empty.symm)

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
theorem rel_iff {x y z w : α} : Rel α (x, y) (z, w) ↔ x = z ∧ y = w ∨ x = w ∧ y = z

Proof state:
α : Type u_1
x y z w : α
⊢ Rel α (x, y) (z, w) ↔ x = z ∧ y = w ∨ x = w ∧ y = z

Tactic:
simp

Result:
no goals