harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Group/Submonoid/BigOperators.lean
theorem list_prod_mem {l : List M} (hl : ∀ x ∈ l, x ∈ s) : l.prod ∈ s

Proof state:
M : Type u_1
inst✝ : Monoid M
s : Submonoid M
l : List M
hl : ∀ x ∈ l, x ∈ s
⊢ l.prod ∈ s

Tactic:
lift l to List s using hl

Result:
case intro
M : Type u_1
inst✝ : Monoid M
s : Submonoid M
l : List ↥s
⊢ (List.map Subtype.val l).prod ∈ s

Proof state:
case intro
M : Type u_1
inst✝ : Monoid M
s : Submonoid M
l : List ↥s
⊢ ↑l.prod ∈ s

Tactic:
exact l.prod.coe_prop

Result:
no goals

Proof state:
case intro
M : Type u_1
inst✝ : Monoid M
s : Submonoid M
l : List ↥s
⊢ (List.map Subtype.val l).prod ∈ s

Tactic:
rw [← coe_list_prod]

Result:
case intro
M : Type u_1
inst✝ : Monoid M
s : Submonoid M
l : List ↥s
⊢ ↑l.prod ∈ s
-- Mathlib/Topology/Compactness/SigmaCompact.lean
/-- A closed subset of a σ-compact set is σ-compact. -/
lemma IsSigmaCompact.of_isClosed_subset {s t : Set X} (ht : IsSigmaCompact t)
    (hs : IsClosed s) (h : s ⊆ t) : IsSigmaCompact s

Proof state:
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsClosed s
h : s ⊆ t
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcov : ⋃ n, K n = t
⊢ s ∩ t = s

Tactic:
exact inter_eq_left.mpr h

Result:
no goals

Proof state:
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsClosed s
h : s ⊆ t
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcov : ⋃ n, K n = t
⊢ ⋃ n, (fun n => s ∩ K n) n = s

Tactic:
rw [← inter_iUnion, hcov]

Result:
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsClosed s
h : s ⊆ t
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcov : ⋃ n, K n = t
⊢ s ∩ t = s

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
ht : IsSigmaCompact t
hs : IsClosed s
h : s ⊆ t
⊢ IsSigmaCompact s

Tactic:
rcases ht with ⟨K, hcompact, hcov⟩

Result:
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsClosed s
h : s ⊆ t
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcov : ⋃ n, K n = t
⊢ IsSigmaCompact s

Proof state:
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsClosed s
h : s ⊆ t
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcov : ⋃ n, K n = t
⊢ IsSigmaCompact s

Tactic:
refine ⟨(fun n ↦ s ∩ (K n)), fun n ↦ (hcompact n).inter_left hs, ?_⟩

Result:
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsClosed s
h : s ⊆ t
K : ℕ → Set X
hcompact : ∀ (n : ℕ), IsCompact (K n)
hcov : ⋃ n, K n = t
⊢ ⋃ n, (fun n => s ∩ K n) n = s
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem reverse_balance2 (l : RBNode α) (v : α) (r : RBNode α) :
    (balance2 l v r).reverse = balance1 r.reverse v l.reverse

Proof state:
α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ (l.balance2 v r).reverse = (l.reverse.reverse.balance2 v r.reverse.reverse).reverse

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ (l.balance2 v r).reverse = r.reverse.balance1 v l.reverse

Tactic:
refine Eq.trans ?_ (reverse_reverse _)

Result:
α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ (l.balance2 v r).reverse = (r.reverse.balance1 v l.reverse).reverse.reverse

Proof state:
α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ (l.balance2 v r).reverse = (r.reverse.balance1 v l.reverse).reverse.reverse

Tactic:
rw [reverse_balance1]

Result:
α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ (l.balance2 v r).reverse = (l.reverse.reverse.balance2 v r.reverse.reverse).reverse
-- Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean
theorem toBaseChange_reverse (Q : QuadraticForm R V) (x : CliffordAlgebra (Q.baseChange A)) :
    toBaseChange A Q (reverse x) =
      TensorProduct.map LinearMap.id reverse (toBaseChange A Q x)

Proof state:
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
x : CliffordAlgebra (QuadraticForm.baseChange A Q)
⊢ (TensorProduct.AlgebraTensorModule.map (↑(opLinearEquiv A).symm ∘ₗ (↑(AlgEquiv.toOpposite A A)).toLinearMap)
        (↑(opLinearEquiv R).symm ∘ₗ reverseOp.toLinearMap))
      (↑(toBaseChange A Q) x) =
    (TensorProduct.map LinearMap.id reverse) ((toBaseChange A Q) x)

Tactic:
rw [reverse, ← AlgEquiv.toLinearMap, ← AlgEquiv.toLinearEquiv_toLinearMap,
  AlgEquiv.toLinearEquiv_toOpposite]

Result:
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
x : CliffordAlgebra (QuadraticForm.baseChange A Q)
⊢ (TensorProduct.AlgebraTensorModule.map (↑(opLinearEquiv A).symm ∘ₗ ↑(opLinearEquiv A))
        (↑(opLinearEquiv R).symm ∘ₗ reverseOp.toLinearMap))
      (↑(toBaseChange A Q) x) =
    (TensorProduct.map LinearMap.id (↑(opLinearEquiv R).symm ∘ₗ reverseOp.toLinearMap)) ((toBaseChange A Q) x)

Proof state:
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
x : CliffordAlgebra (QuadraticForm.baseChange A Q)
⊢ (toBaseChange A Q) (reverse x) = (TensorProduct.map LinearMap.id reverse) ((toBaseChange A Q) x)

Tactic:
have := DFunLike.congr_fun (toBaseChange_comp_reverseOp A Q) x

Result:
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
x : CliffordAlgebra (QuadraticForm.baseChange A Q)
this :
  ((AlgHom.op (toBaseChange A Q)).comp reverseOp) x =
    ((↑(Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q))).comp
        ((Algebra.TensorProduct.map (↑(AlgEquiv.toOpposite A A)) reverseOp).comp (toBaseChange A Q)))
      x
⊢ (toBaseChange A Q) (reverse x) = (TensorProduct.map LinearMap.id reverse) ((toBaseChange A Q) x)
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem eq_zero_of_not_dvd {z : ℤ} (h : ¬(p : ℤ) ∣ z) : padicValInt p z = 0

Proof state:
case h
p : ℕ
z : ℤ
h : ¬↑p ∣ z
⊢ z.natAbs = 0 ∨ ¬p ∣ z.natAbs

Tactic:
right

Result:
case h.h
p : ℕ
z : ℤ
h : ¬↑p ∣ z
⊢ ¬p ∣ z.natAbs

Proof state:
p : ℕ
z : ℤ
h : ¬↑p ∣ z
⊢ p = 1 ∨ z.natAbs = 0 ∨ ¬p ∣ z.natAbs

Tactic:
right

Result:
case h
p : ℕ
z : ℤ
h : ¬↑p ∣ z
⊢ z.natAbs = 0 ∨ ¬p ∣ z.natAbs

Proof state:
p : ℕ
z : ℤ
h : ¬↑p ∣ z
⊢ padicValInt p z = 0

Tactic:
rw [padicValInt, padicValNat.eq_zero_iff]

Result:
p : ℕ
z : ℤ
h : ¬↑p ∣ z
⊢ p = 1 ∨ z.natAbs = 0 ∨ ¬p ∣ z.natAbs

Proof state:
case h.h
p : ℕ
z : ℤ
h : ¬↑p ∣ z
⊢ ¬p ∣ z.natAbs

Tactic:
rwa [← Int.ofNat_dvd_left]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Verschiebung.lean
theorem ghostComponent_verschiebungFun [hp : Fact p.Prime] (x : 𝕎 R) (n : ℕ) :
    ghostComponent (n + 1) (verschiebungFun x) = p * ghostComponent n x

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
⊢ ∑ i ∈ Finset.range (n + 1 + 1), ↑p ^ i * x.verschiebungFun.coeff i ^ p ^ (n + 1 - i) =
    ↑p * ∑ i ∈ Finset.range (n + 1), ↑p ^ i * x.coeff i ^ p ^ (n - i)

Tactic:
rw [Finset.sum_range_succ', verschiebungFun_coeff, if_pos rfl,
  zero_pow (pow_ne_zero _ hp.1.ne_zero), mul_zero, add_zero, Finset.mul_sum, Finset.sum_congr rfl]

Result:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
⊢ ∀ x_1 ∈ Finset.range (n + 1),
    ↑p ^ (x_1 + 1) * x.verschiebungFun.coeff (x_1 + 1) ^ p ^ (n + 1 - (x_1 + 1)) =
      ↑p * (↑p ^ x_1 * x.coeff x_1 ^ p ^ (n - x_1))

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
n i : ℕ
⊢ ↑p ^ (i + 1) * x.verschiebungFun.coeff (i + 1) ^ p ^ (n + 1 - (i + 1)) = ↑p * (↑p ^ i * x.coeff i ^ p ^ (n - i))

Tactic:
simp only [pow_succ', verschiebungFun_coeff_succ, Nat.succ_sub_succ_eq_sub, mul_assoc]

Result:
no goals

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
⊢ (ghostComponent (n + 1)) x.verschiebungFun = ↑p * (ghostComponent n) x

Tactic:
simp only [ghostComponent_apply, aeval_wittPolynomial]

Result:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
⊢ ∑ i ∈ Finset.range (n + 1 + 1), ↑p ^ i * x.verschiebungFun.coeff i ^ p ^ (n + 1 - i) =
    ↑p * ∑ i ∈ Finset.range (n + 1), ↑p ^ i * x.coeff i ^ p ^ (n - i)

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
n : ℕ
⊢ ∀ x_1 ∈ Finset.range (n + 1),
    ↑p ^ (x_1 + 1) * x.verschiebungFun.coeff (x_1 + 1) ^ p ^ (n + 1 - (x_1 + 1)) =
      ↑p * (↑p ^ x_1 * x.coeff x_1 ^ p ^ (n - x_1))

Tactic:
rintro i -

Result:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
n i : ℕ
⊢ ↑p ^ (i + 1) * x.verschiebungFun.coeff (i + 1) ^ p ^ (n + 1 - (i + 1)) = ↑p * (↑p ^ i * x.coeff i ^ p ^ (n - i))
-- Mathlib/CategoryTheory/Monoidal/Bimod.lean
theorem triangle_bimod {X Y Z : Mon_ C} (M : Bimod X Y) (N : Bimod Y Z) :
    (associatorBimod M (regular Y) N).hom ≫ whiskerLeft M (leftUnitorBimod N).hom =
      whiskerRight (rightUnitorBimod M).hom N

Proof state:
case h.h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon_ C
M : Bimod X Y
N : Bimod Y Z
⊢ (α_ M.X Y.X N.X).hom ≫
      M.X ◁ coequalizer.π (Y.mul ▷ N.X) ((α_ Y.X Y.X N.X).hom ≫ Y.X ◁ N.actLeft) ≫
        M.X ◁ coequalizer.desc N.actLeft ⋯ ≫
          colimit.ι (parallelPair (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft)) WalkingParallelPair.one =
    coequalizer.π (M.actRight ▷ Y.X) ((α_ M.X Y.X Y.X).hom ≫ M.X ◁ Y.mul) ▷ N.X ≫
      coequalizer.desc M.actRight ⋯ ▷ N.X ≫
        colimit.ι (parallelPair (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft)) WalkingParallelPair.one

Tactic:
slice_lhs 2 3 => rw [← MonoidalCategory.whiskerLeft_comp, coequalizer.π_desc]

Result:
case h.h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon_ C
M : Bimod X Y
N : Bimod Y Z
⊢ (α_ M.X Y.X N.X).hom ≫
      M.X ◁ N.actLeft ≫
        colimit.ι (parallelPair (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft)) WalkingParallelPair.one =
    coequalizer.π (M.actRight ▷ Y.X) ((α_ M.X Y.X Y.X).hom ≫ M.X ◁ Y.mul) ▷ N.X ≫
      coequalizer.desc M.actRight ⋯ ▷ N.X ≫
        colimit.ι (parallelPair (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft)) WalkingParallelPair.one
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem oangle_sub_right_eq_arctan_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    o.oangle y (y - x) = Real.arctan (‖x‖ / ‖y‖)

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle y (y - x)).sign = 1

Tactic:
rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ o.oangle y (y - x) = ↑(Real.arctan (‖x‖ / ‖y‖))

Tactic:
have hs : (o.oangle y (y - x)).sign = 1 := by
  rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle y (y - x)).sign = 1
⊢ o.oangle y (y - x) = ↑(Real.arctan (‖x‖ / ‖y‖))

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle y (y - x)).sign = 1
⊢ o.oangle y (y - x) = ↑(Real.arctan (‖x‖ / ‖y‖))

Tactic:
rw [o.oangle_eq_angle_of_sign_eq_one hs,
  InnerProductGeometry.angle_sub_eq_arctan_of_inner_eq_zero
    (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h) (o.right_ne_zero_of_oangle_eq_pi_div_two h)]

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem restrict_le_restrict_iUnion {f : ℕ → Set α} (hf₁ : ∀ n, MeasurableSet (f n))
    (hf₂ : ∀ n, v ≤[f n] w) : v ≤[⋃ n, f n] w

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ n, f n
⊢ ↑v a ≤ ↑w a

Tactic:
have ha₃ : ⋃ n, a ∩ disjointed f n = a := by
  rwa [← Set.inter_iUnion, iUnion_disjointed, Set.inter_eq_left]

Result:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ n, f n
ha₃ : ⋃ n, a ∩ disjointed f n = a
⊢ ↑v a ≤ ↑w a

Proof state:
case refine_3.refine_2
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ n, f n
ha₃ : ⋃ n, a ∩ disjointed f n = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
⊢ Pairwise (Disjoint on fun i => a ∩ disjointed f i)

Tactic:
exact (disjoint_disjointed _).mono fun i j => Disjoint.mono inf_le_right inf_le_right

Result:
no goals

Proof state:
case refine_1
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommMonoid M
inst✝ : OrderClosedTopology M
v w : VectorMeasure α M
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ), v ≤[f n] w
a : Set α
ha₁ : MeasurableSet a
ha₂ : a ⊆ ⋃ n, f n
ha₃ : ⋃ n, a ∩ disjointed f n = a
ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n)
n : ℕ
⊢ MeasurableSet (a ∩ disjointed f n)

Tactic:
exact ha₁.inter (MeasurableSet.disjointed hf₁ n)

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem toAdd_multiset_sum (s : Multiset (Multiplicative α)) :
    s.prod.toAdd = (s.map toAdd).sum

Proof state:
α : Type u_3
inst✝ : AddCommMonoid α
s : Multiset (Multiplicative α)
⊢ toAdd s.prod = (Multiset.map (⇑toAdd) s).sum

Tactic:
simp [toAdd, ofAdd]

Result:
α : Type u_3
inst✝ : AddCommMonoid α
s : Multiset (Multiplicative α)
⊢ s.prod = s.sum

Proof state:
α : Type u_3
inst✝ : AddCommMonoid α
s : Multiset (Multiplicative α)
⊢ s.prod = s.sum

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNorm.lean
theorem of_int (z : ℤ) : padicNorm p z ≤ 1

Proof state:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : z ≠ 0
⊢ padicNorm p ↑z ≤ 1

Tactic:
rw [padicNorm, if_neg (mod_cast hz)]

Result:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : z ≠ 0
⊢ ↑p ^ (-padicValRat p ↑z) ≤ 1

Proof state:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : z ≠ 0
⊢ ↑p ^ (-padicValRat p ↑z) ≤ 1

Tactic:
exact zpow_le_one_of_nonpos₀ (mod_cast hp.1.one_le) (by simp)

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : z ≠ 0
⊢ -padicValRat p ↑z ≤ 0

Tactic:
simp

Result:
no goals

Proof state:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
⊢ padicNorm p ↑0 ≤ 1

Tactic:
simp

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
⊢ padicNorm p ↑z ≤ 1

Tactic:
obtain rfl | hz := eq_or_ne z 0

Result:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
⊢ padicNorm p ↑0 ≤ 1

case inr
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
hz : z ≠ 0
⊢ padicNorm p ↑z ≤ 1
-- Mathlib/Algebra/Polynomial/BigOperators.lean
theorem natDegree_prod (h : ∀ i ∈ s, f i ≠ 0) :
    (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree

Proof state:
case h
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
h : ∀ i ∈ s, f i ≠ 0
a✝ : Nontrivial R
⊢ ∏ i ∈ s, (f i).leadingCoeff ≠ 0

Tactic:
rw [prod_ne_zero_iff]

Result:
case h
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
h : ∀ i ∈ s, f i ≠ 0
a✝ : Nontrivial R
⊢ ∀ a ∈ s, (f a).leadingCoeff ≠ 0

Proof state:
case h
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
h : ∀ i ∈ s, f i ≠ 0
a✝ : Nontrivial R
⊢ ∀ a ∈ s, (f a).leadingCoeff ≠ 0

Tactic:
intro x hx

Result:
case h
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
h : ∀ i ∈ s, f i ≠ 0
a✝ : Nontrivial R
x : ι
hx : x ∈ s
⊢ (f x).leadingCoeff ≠ 0

Proof state:
case h
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
h : ∀ i ∈ s, f i ≠ 0
a✝ : Nontrivial R
x : ι
hx : x ∈ s
⊢ (f x).leadingCoeff ≠ 0

Tactic:
simp [h x hx]

Result:
no goals

Proof state:
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
h : ∀ i ∈ s, f i ≠ 0
⊢ (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree

Tactic:
nontriviality R

Result:
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
h : ∀ i ∈ s, f i ≠ 0
a✝ : Nontrivial R
⊢ (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree

Proof state:
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
h : ∀ i ∈ s, f i ≠ 0
a✝ : Nontrivial R
⊢ (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree

Tactic:
apply natDegree_prod'

Result:
case h
R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
h : ∀ i ∈ s, f i ≠ 0
a✝ : Nontrivial R
⊢ ∏ i ∈ s, (f i).leadingCoeff ≠ 0
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem lift_ord (c) : Ordinal.lift.{u,v} (ord c) = ord (lift.{u,v} c)

Proof state:
c : Cardinal.{v}
⊢ Ordinal.lift.{u, v} c.ord = (lift.{u, v} c).ord

Tactic:
refine le_antisymm (le_of_forall_lt fun a ha => ?_) ?_

Result:
case refine_1
c : Cardinal.{v}
a : Ordinal.{max v u}
ha : a < Ordinal.lift.{u, v} c.ord
⊢ a < (lift.{u, v} c).ord

case refine_2
c : Cardinal.{v}
⊢ (lift.{u, v} c).ord ≤ Ordinal.lift.{u, v} c.ord

Proof state:
case refine_1.intro.intro
c : Cardinal.{v}
a : Ordinal.{v}
left✝ : a < c.ord
ha : Ordinal.lift.{u, v} a < Ordinal.lift.{u, v} c.ord
⊢ Ordinal.lift.{u, v} a < (lift.{u, v} c).ord

Tactic:
rwa [lt_ord, ← lift_card, lift_lt, ← lt_ord, ← Ordinal.lift_lt]

Result:
no goals

Proof state:
case refine_1
c : Cardinal.{v}
a : Ordinal.{max v u}
ha : a < Ordinal.lift.{u, v} c.ord
⊢ a < (lift.{u, v} c).ord

Tactic:
rcases Ordinal.lt_lift_iff.1 ha with ⟨a, _, rfl⟩

Result:
case refine_1.intro.intro
c : Cardinal.{v}
a : Ordinal.{v}
left✝ : a < c.ord
ha : Ordinal.lift.{u, v} a < Ordinal.lift.{u, v} c.ord
⊢ Ordinal.lift.{u, v} a < (lift.{u, v} c).ord

Proof state:
case refine_2
c : Cardinal.{v}
⊢ (lift.{u, v} c).ord ≤ Ordinal.lift.{u, v} c.ord

Tactic:
rw [ord_le, ← lift_card, card_ord]

Result:
no goals
-- Mathlib/Data/Int/Lemmas.lean
theorem ediv_emod_unique' {a b r q : Int} (h : b ≠ 0) :
    a / b = q ∧ a % b = r ↔ r + b * q = a ∧ 0 ≤ r ∧ r < |b|

Proof state:
case mpr.right
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ (r + b * q) % b = r

Tactic:
rw [add_mul_emod_self_left, ← emod_abs, emod_eq_of_lt hz hb]

Result:
no goals

Proof state:
a b r q : ℤ
h : b ≠ 0
⊢ a / b = q ∧ a % b = r ↔ r + b * q = a ∧ 0 ≤ r ∧ r < |b|

Tactic:
constructor

Result:
case mp
a b r q : ℤ
h : b ≠ 0
⊢ a / b = q ∧ a % b = r → r + b * q = a ∧ 0 ≤ r ∧ r < |b|

case mpr
a b r q : ℤ
h : b ≠ 0
⊢ r + b * q = a ∧ 0 ≤ r ∧ r < |b| → a / b = q ∧ a % b = r

Proof state:
case mpr
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ (r + b * q) / b = q ∧ (r + b * q) % b = r

Tactic:
constructor

Result:
case mpr.left
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ (r + b * q) / b = q

case mpr.right
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ (r + b * q) % b = r

Proof state:
case mpr.left
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ (r + b * q) / b = q

Tactic:
rw [Int.add_mul_ediv_left r q h, ediv_eq_zero_of_lt_abs hz hb]

Result:
case mpr.left
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ 0 + q = q

Proof state:
case mpr.left
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ 0 + q = q

Tactic:
simp [Int.zero_add]

Result:
no goals

Proof state:
case mpr
a b r q : ℤ
h : b ≠ 0
⊢ r + b * q = a ∧ 0 ≤ r ∧ r < |b| → a / b = q ∧ a % b = r

Tactic:
intro ⟨rfl, hz, hb⟩

Result:
case mpr
a b r q : ℤ
h : b ≠ 0
hz : 0 ≤ r
hb : r < |b|
⊢ (r + b * q) / b = q ∧ (r + b * q) % b = r

Proof state:
case mp
a b r q : ℤ
h : b ≠ 0
⊢ a % b + b * (a / b) = a ∧ 0 ≤ a % b ∧ a % b < |b|

Tactic:
exact ⟨emod_add_ediv a b, emod_nonneg _ h, emod_lt _ h⟩

Result:
no goals

Proof state:
case mp
a b r q : ℤ
h : b ≠ 0
⊢ a / b = q ∧ a % b = r → r + b * q = a ∧ 0 ≤ r ∧ r < |b|

Tactic:
intro ⟨rfl, rfl⟩

Result:
case mp
a b r q : ℤ
h : b ≠ 0
⊢ a % b + b * (a / b) = a ∧ 0 ≤ a % b ∧ a % b < |b|
-- Mathlib/ModelTheory/Algebra/Field/CharP.lean
theorem realize_eqZero [CommRing K] [CompatibleRing K] (n : ℕ)
    (v : Empty → K) : (Formula.Realize (eqZero n) v) ↔ ((n : K) = 0)

Proof state:
K : Type u_1
inst✝¹ : CommRing K
inst✝ : CompatibleRing K
n : ℕ
v : Empty → K
⊢ Formula.Realize (eqZero n) v ↔ ↑n = 0

Tactic:
simp [eqZero, Term.realize]

Result:
no goals
-- Mathlib/Analysis/Analytic/Within.lean
/-- On open sets, `AnalyticOnNhd` and `AnalyticOn` coincide -/
lemma IsOpen.analyticOn_iff_analyticOnNhd {f : E → F} {s : Set E} (hs : IsOpen s) :
    AnalyticOn 𝕜 f s ↔ AnalyticOnNhd 𝕜 f s

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
hs : IsOpen s
hf : AnalyticOn 𝕜 f s
x : E
m : x ∈ s
r : ℝ
r0 : r > 0
rs : Metric.ball x r ⊆ s
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p s x t
y : E
ym : ‖y‖ < r ∧ edist y 0 < t
⊢ x + y ∈ insert x s

Tactic:
apply mem_insert_of_mem

Result:
case a
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
hs : IsOpen s
hf : AnalyticOn 𝕜 f s
x : E
m : x ∈ s
r : ℝ
r0 : r > 0
rs : Metric.ball x r ⊆ s
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p s x t
y : E
ym : ‖y‖ < r ∧ edist y 0 < t
⊢ x + y ∈ s

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
hs : IsOpen s
hf : AnalyticOn 𝕜 f s
x : E
m : x ∈ s
r : ℝ
r0 : r > 0
rs : Metric.ball x r ⊆ s
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p s x t
y : E
ym : y ∈ EMetric.ball 0 (ENNReal.ofReal r ⊓ t)
⊢ HasSum (fun n => (p n) fun x => y) (f (x + y))

Tactic:
simp only [EMetric.mem_ball, lt_min_iff, edist_lt_ofReal, dist_zero_right] at ym

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
hs : IsOpen s
hf : AnalyticOn 𝕜 f s
x : E
m : x ∈ s
r : ℝ
r0 : r > 0
rs : Metric.ball x r ⊆ s
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p s x t
y : E
ym : ‖y‖ < r ∧ edist y 0 < t
⊢ HasSum (fun n => (p n) fun x => y) (f (x + y))

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
hs : IsOpen s
hf : AnalyticOn 𝕜 f s
x : E
m : x ∈ s
r : ℝ
r0 : r > 0
rs : Metric.ball x r ⊆ s
p : FormalMultilinearSeries 𝕜 E F
t : ℝ≥0∞
fp : HasFPowerSeriesWithinOnBall f p s x t
⊢ 0 < ENNReal.ofReal r

Tactic:
positivity

Result:
no goals