harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/MvPowerSeries/Inverse.lean
theorem inv_eq_zero {φ : MvPowerSeries σ k} : φ⁻¹ = 0 ↔ constantCoeff σ k φ = 0 :=
  ⟨fun h => by simpa using congr_arg (constantCoeff σ k) h, fun h =>
    ext fun n => by
      classical
      rw [coeff_inv]
      split_ifs <;>
        simp only [h, map_zero, zero_mul, inv_zero, neg_zero]⟩

Proof state:
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
h : (constantCoeff σ k) φ = 0
n : σ →₀ ℕ
⊢ (coeff k n) φ⁻¹ = (coeff k n) 0

Tactic:
classical
rw [coeff_inv]
split_ifs <;>
  simp only [h, map_zero, zero_mul, inv_zero, neg_zero]

Result:
no goals

Proof state:
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
h : (constantCoeff σ k) φ = 0
n : σ →₀ ℕ
⊢ (if n = 0 then ((constantCoeff σ k) φ)⁻¹
    else
      -((constantCoeff σ k) φ)⁻¹ * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff k x.1) φ * (coeff k x.2) φ⁻¹ else 0) =
    (coeff k n) 0

Tactic:
split_ifs <;>
  simp only [h, map_zero, zero_mul, inv_zero, neg_zero]

Result:
no goals

Proof state:
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
h : φ⁻¹ = 0
⊢ (constantCoeff σ k) φ = 0

Tactic:
simpa using congr_arg (constantCoeff σ k) h

Result:
no goals

Proof state:
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
h : (constantCoeff σ k) φ = 0
n : σ →₀ ℕ
⊢ (coeff k n) φ⁻¹ = (coeff k n) 0

Tactic:
rw [coeff_inv]

Result:
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
h : (constantCoeff σ k) φ = 0
n : σ →₀ ℕ
⊢ (if n = 0 then ((constantCoeff σ k) φ)⁻¹
    else
      -((constantCoeff σ k) φ)⁻¹ * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff k x.1) φ * (coeff k x.2) φ⁻¹ else 0) =
    (coeff k n) 0
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem C_eq_smul_one : (C a : MvPolynomial σ R) = a • (1 : MvPolynomial σ R)

Proof state:
R : Type u
σ : Type u_1
a : R
inst✝ : CommSemiring R
⊢ C a = a • 1

Tactic:
rw [← C_mul', mul_one]

Result:
no goals
-- Mathlib/Algebra/Vertex/HVertexOperator.lean
theorem compHahnSeries_smul (r : R) (u : U) :
    compHahnSeries A B (r • u) = r • compHahnSeries A B u

Proof state:
case coeff.h.coeff.h
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : OrderedCancelAddCommMonoid Γ
inst✝⁷ : OrderedCancelAddCommMonoid Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
r : R
u : U
x✝¹ : Γ'
x✝ : Γ
⊢ (r • A (((of R).symm (B u)).coeff x✝¹)).coeff x✝ = r • (A (((of R).symm (B u)).coeff x✝¹)).coeff x✝

Tactic:
rw [← HahnSeries.coeff_smul]

Result:
no goals

Proof state:
case coeff.h.coeff.h
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : OrderedCancelAddCommMonoid Γ
inst✝⁷ : OrderedCancelAddCommMonoid Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
r : R
u : U
x✝¹ : Γ'
x✝ : Γ
⊢ ((A.compHahnSeries B (r • u)).coeff x✝¹).coeff x✝ = ((r • A.compHahnSeries B u).coeff x✝¹).coeff x✝

Tactic:
simp only [compHahnSeries_coeff, LinearMapClass.map_smul, coeff_apply, HahnSeries.coeff_smul]

Result:
case coeff.h.coeff.h
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : OrderedCancelAddCommMonoid Γ
inst✝⁷ : OrderedCancelAddCommMonoid Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
r : R
u : U
x✝¹ : Γ'
x✝ : Γ
⊢ (r • A (((of R).symm (B u)).coeff x✝¹)).coeff x✝ = r • (A (((of R).symm (B u)).coeff x✝¹)).coeff x✝

Proof state:
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : OrderedCancelAddCommMonoid Γ
inst✝⁷ : OrderedCancelAddCommMonoid Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
r : R
u : U
⊢ A.compHahnSeries B (r • u) = r • A.compHahnSeries B u

Tactic:
ext

Result:
case coeff.h.coeff.h
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : OrderedCancelAddCommMonoid Γ
inst✝⁷ : OrderedCancelAddCommMonoid Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
r : R
u : U
x✝¹ : Γ'
x✝ : Γ
⊢ ((A.compHahnSeries B (r • u)).coeff x✝¹).coeff x✝ = ((r • A.compHahnSeries B u).coeff x✝¹).coeff x✝
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
@[gcongr]
lemma arccos_le_arccos {x y : ℝ} (hlt : x ≤ y) : arccos y ≤ arccos x

Proof state:
x y : ℝ
hlt : x ≤ y
⊢ π / 2 - arcsin y ≤ π / 2 - arcsin x

Tactic:
gcongr

Result:
no goals

Proof state:
x y : ℝ
hlt : x ≤ y
⊢ arccos y ≤ arccos x

Tactic:
unfold arccos

Result:
x y : ℝ
hlt : x ≤ y
⊢ π / 2 - arcsin y ≤ π / 2 - arcsin x
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
theorem gc : GaloisConnection (adjoin R : Set A → NonUnitalStarSubalgebra R A) (↑)

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
S : NonUnitalStarSubalgebra R A
⊢ s ∪ star s ⊆ ↑S ↔ s ≤ ↑S

Tactic:
exact ⟨fun h => Set.subset_union_left.trans h,
  fun h => Set.union_subset h fun x hx => star_star x ▸ star_mem (show star x ∈ S from h hx)⟩

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
S : NonUnitalStarSubalgebra R A
⊢ adjoin R s ≤ S ↔ s ≤ ↑S

Tactic:
rw [← toNonUnitalSubalgebra_le_iff, adjoin_toNonUnitalSubalgebra,
  NonUnitalAlgebra.adjoin_le_iff, coe_toNonUnitalSubalgebra]

Result:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
S : NonUnitalStarSubalgebra R A
⊢ s ∪ star s ⊆ ↑S ↔ s ≤ ↑S

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
⊢ GaloisConnection (adjoin R) SetLike.coe

Tactic:
intro s S

Result:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
S : NonUnitalStarSubalgebra R A
⊢ adjoin R s ≤ S ↔ s ≤ ↑S
-- Mathlib/Analysis/Normed/Field/Lemmas.lean
/-- A normed field is either nontrivially normed or has a discrete topology.
In the discrete topology case, all the norms are 1, by `norm_eq_one_iff_ne_zero_of_discrete`.
The nontrivially normed field instance is provided by a subtype with a proof that the
forgetful inheritance to the existing `NormedField` instance is definitionally true.
This allows one to have the new `NontriviallyNormedField` instance without data clashes. -/
lemma discreteTopology_or_nontriviallyNormedField (𝕜 : Type*) [h : NormedField 𝕜] :
    DiscreteTopology 𝕜 ∨ Nonempty ({h' : NontriviallyNormedField 𝕜 // h'.toNormedField = h})

Proof state:
case neg
𝕜 : Type u_4
h : NormedField 𝕜
H : ∃ y, ‖y‖ < 1 ∧ y ≠ 0
⊢ ∃ x, x ≠ 0 ∧ ‖x‖ ≠ 1

Tactic:
refine H.imp ?_

Result:
case neg
𝕜 : Type u_4
h : NormedField 𝕜
H : ∃ y, ‖y‖ < 1 ∧ y ≠ 0
⊢ ∀ (a : 𝕜), ‖a‖ < 1 ∧ a ≠ 0 → a ≠ 0 ∧ ‖a‖ ≠ 1

Proof state:
case neg
𝕜 : Type u_4
h : NormedField 𝕜
H : ∃ y, ‖y‖ < 1 ∧ y ≠ 0
⊢ ∀ (a : 𝕜), ‖a‖ < 1 ∧ a ≠ 0 → a ≠ 0 ∧ ‖a‖ ≠ 1

Tactic:
simp (config := {contextual := true}) [add_comm, ne_of_lt]

Result:
no goals

Proof state:
𝕜 : Type u_4
h : NormedField 𝕜
⊢ DiscreteTopology 𝕜 ∨ Nonempty { h' // NontriviallyNormedField.toNormedField = h }

Tactic:
by_cases H : ∃ x : 𝕜, x ≠ 0 ∧ ‖x‖ ≠ 1

Result:
case pos
𝕜 : Type u_4
h : NormedField 𝕜
H : ∃ x, x ≠ 0 ∧ ‖x‖ ≠ 1
⊢ DiscreteTopology 𝕜 ∨ Nonempty { h' // NontriviallyNormedField.toNormedField = h }

case neg
𝕜 : Type u_4
h : NormedField 𝕜
H : ¬∃ x, x ≠ 0 ∧ ‖x‖ ≠ 1
⊢ DiscreteTopology 𝕜 ∨ Nonempty { h' // NontriviallyNormedField.toNormedField = h }

Proof state:
case neg
𝕜 : Type u_4
h : NormedField 𝕜
H : ¬∃ x, x ≠ 0 ∧ ‖x‖ ≠ 1
⊢ (∃ ε > 0, ∀ (y : 𝕜), ‖y‖ < ε → y = 0) ∨ Nonempty { h' // NontriviallyNormedField.toNormedField = h }

Tactic:
refine Or.inl ⟨1, zero_lt_one, ?_⟩

Result:
case neg
𝕜 : Type u_4
h : NormedField 𝕜
H : ¬∃ x, x ≠ 0 ∧ ‖x‖ ≠ 1
⊢ ∀ (y : 𝕜), ‖y‖ < 1 → y = 0

Proof state:
case neg
𝕜 : Type u_4
h : NormedField 𝕜
H : ¬∃ x, x ≠ 0 ∧ ‖x‖ ≠ 1
⊢ ∀ (y : 𝕜), ‖y‖ < 1 → y = 0

Tactic:
contrapose! H

Result:
case neg
𝕜 : Type u_4
h : NormedField 𝕜
H : ∃ y, ‖y‖ < 1 ∧ y ≠ 0
⊢ ∃ x, x ≠ 0 ∧ ‖x‖ ≠ 1

Proof state:
case pos
𝕜 : Type u_4
h : NormedField 𝕜
H : ∃ x, x ≠ 0 ∧ ‖x‖ ≠ 1
⊢ DiscreteTopology 𝕜 ∨ Nonempty { h' // NontriviallyNormedField.toNormedField = h }

Tactic:
exact Or.inr ⟨(⟨NontriviallyNormedField.ofNormNeOne H, rfl⟩)⟩

Result:
no goals

Proof state:
case neg
𝕜 : Type u_4
h : NormedField 𝕜
H : ¬∃ x, x ≠ 0 ∧ ‖x‖ ≠ 1
⊢ DiscreteTopology 𝕜 ∨ Nonempty { h' // NontriviallyNormedField.toNormedField = h }

Tactic:
simp_rw [discreteTopology_iff_isOpen_singleton_zero, Metric.isOpen_singleton_iff, dist_eq_norm,
         sub_zero]

Result:
case neg
𝕜 : Type u_4
h : NormedField 𝕜
H : ¬∃ x, x ≠ 0 ∧ ‖x‖ ≠ 1
⊢ (∃ ε > 0, ∀ (y : 𝕜), ‖y‖ < ε → y = 0) ∨ Nonempty { h' // NontriviallyNormedField.toNormedField = h }
-- Mathlib/RingTheory/Localization/InvSubmonoid.lean
theorem smul_toInvSubmonoid (m : M) : m • (toInvSubmonoid M S m : S) = 1

Proof state:
case h.e'_2.h.e.h
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
m : ↥M
x✝ : S
⊢ m • x✝ = (algebraMap R S) ↑m * x✝

Tactic:
rw [← Algebra.smul_def]

Result:
case h.e'_2.h.e.h
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
m : ↥M
x✝ : S
⊢ m • x✝ = ↑m • x✝

Proof state:
case h.e'_2.h.e.h
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
m : ↥M
x✝ : S
⊢ m • x✝ = ↑m • x✝

Tactic:
rfl

Result:
no goals

Proof state:
case h.e'_2.h.e
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
m : ↥M
⊢ HSMul.hSMul m = HMul.hMul ((algebraMap R S) ↑m)

Tactic:
ext

Result:
case h.e'_2.h.e.h
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
m : ↥M
x✝ : S
⊢ m • x✝ = (algebraMap R S) ↑m * x✝

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
m : ↥M
⊢ m • ↑((toInvSubmonoid M S) m) = 1

Tactic:
convert mul_toInvSubmonoid M S m

Result:
case h.e'_2.h.e
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
m : ↥M
⊢ HSMul.hSMul m = HMul.hMul ((algebraMap R S) ↑m)
-- Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
theorem gramSchmidtOrthonormalBasis_inv_triangular {i j : ι} (hij : i < j) :
    ⟪gramSchmidtOrthonormalBasis h f j, f i⟫ = 0

Proof state:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : WellFoundedLT ι
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i j : ι
hij : i < j
hi : ¬gramSchmidtNormed 𝕜 f j = 0
⊢ inner ((gramSchmidtOrthonormalBasis h f) j) (f i) = 0

Tactic:
simp [gramSchmidtOrthonormalBasis_apply h hi, gramSchmidtNormed, inner_smul_left,
  gramSchmidt_inv_triangular 𝕜 f hij]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : WellFoundedLT ι
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i j : ι
hij : i < j
⊢ inner ((gramSchmidtOrthonormalBasis h f) j) (f i) = 0

Tactic:
by_cases hi : gramSchmidtNormed 𝕜 f j = 0

Result:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : WellFoundedLT ι
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i j : ι
hij : i < j
hi : gramSchmidtNormed 𝕜 f j = 0
⊢ inner ((gramSchmidtOrthonormalBasis h f) j) (f i) = 0

case neg
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : WellFoundedLT ι
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i j : ι
hij : i < j
hi : ¬gramSchmidtNormed 𝕜 f j = 0
⊢ inner ((gramSchmidtOrthonormalBasis h f) j) (f i) = 0

Proof state:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : WellFoundedLT ι
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional 𝕜 E
h : finrank 𝕜 E = Fintype.card ι
f : ι → E
i j : ι
hij : i < j
hi : gramSchmidtNormed 𝕜 f j = 0
⊢ inner ((gramSchmidtOrthonormalBasis h f) j) (f i) = 0

Tactic:
rw [inner_gramSchmidtOrthonormalBasis_eq_zero h hi]

Result:
no goals
-- Mathlib/RingTheory/Perfectoid/Untilt.lean
lemma pow_dvd_one_untiltAux_sub_one (m : ℕ) :
    (p : O) ^ m ∣ (1 : PreTilt O p).untiltAux m - 1

Proof state:
case succ
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
m : ℕ
⊢ (Ideal.Quotient.mk (span {↑p})) (Quotient.out ((coeff (ModP O p) p m) 1)) = (Ideal.Quotient.mk (span {↑p})) 1

Tactic:
simp

Result:
no goals

Proof state:
case succ
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
m : ℕ
⊢ ↑p ^ (m + 1) ∣ untiltAux 1 (m + 1) - 1

Tactic:
simp only [untiltAux]

Result:
case succ
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
m : ℕ
⊢ ↑p ^ (m + 1) ∣ Quotient.out ((coeff (ModP O p) p m) 1) ^ p ^ m - 1

Proof state:
case succ
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
m : ℕ
⊢ ↑p ∣ Quotient.out ((coeff (ModP O p) p m) 1) - 1

Tactic:
rw [← mem_span_singleton, ← Ideal.Quotient.eq]

Result:
case succ
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
m : ℕ
⊢ (Ideal.Quotient.mk (span {↑p})) (Quotient.out ((coeff (ModP O p) p m) 1)) = (Ideal.Quotient.mk (span {↑p})) 1

Proof state:
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
m : ℕ
⊢ ↑p ^ m ∣ untiltAux 1 m - 1

Tactic:
cases m with
| zero => simp [untiltAux]
| succ m =>
  simp only [untiltAux]
  nth_rw 3 [← one_pow (p ^ m)]
  refine dvd_sub_pow_of_dvd_sub (R := O) ?_ m
  rw [← mem_span_singleton, ← Ideal.Quotient.eq]
  simp

Result:
no goals

Proof state:
case succ
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
m : ℕ
⊢ ↑p ^ (m + 1) ∣ Quotient.out ((coeff (ModP O p) p m) 1) ^ p ^ m - 1 ^ p ^ m

Tactic:
refine dvd_sub_pow_of_dvd_sub (R := O) ?_ m

Result:
case succ
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
m : ℕ
⊢ ↑p ∣ Quotient.out ((coeff (ModP O p) p m) 1) - 1

Proof state:
case zero
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
⊢ ↑p ^ 0 ∣ untiltAux 1 0 - 1

Tactic:
simp [untiltAux]

Result:
no goals

Proof state:
case succ
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
m : ℕ
⊢ ↑p ^ (m + 1) ∣ Quotient.out ((coeff (ModP O p) p m) 1) ^ p ^ m - 1

Tactic:
nth_rw 3 [← one_pow (p ^ m)]

Result:
case succ
O : Type u_1
inst✝² : CommRing O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
m : ℕ
⊢ ↑p ^ (m + 1) ∣ Quotient.out ((coeff (ModP O p) p m) 1) ^ p ^ m - 1 ^ p ^ m
-- Mathlib/Probability/Kernel/Basic.lean
theorem restrict_univ : κ.restrict MeasurableSet.univ = κ

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
⊢ (κ.restrict ⋯) a = κ a

Tactic:
rw [Kernel.restrict_apply, Measure.restrict_univ]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ κ.restrict ⋯ = κ

Tactic:
ext1 a

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
⊢ (κ.restrict ⋯) a = κ a
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem basicOpen :
    IsAffineOpen (X.basicOpen f)

Proof state:
case h.e'_2
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ PrimeSpectrum.basicOpen f =
    Scheme.Hom.opensRange (Spec.map (CommRingCat.ofHom (algebraMap (↑Γ(X, U)) (Localization.Away f))))

Tactic:
exact Opens.ext (PrimeSpectrum.localization_away_comap_range (Localization.Away f) f).symm

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ IsAffineOpen (PrimeSpectrum.basicOpen f)

Tactic:
convert isAffineOpen_opensRange
  (Spec.map (CommRingCat.ofHom <| algebraMap Γ(X, U) (Localization.Away f)))

Result:
case h.e'_2
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ PrimeSpectrum.basicOpen f =
    Scheme.Hom.opensRange (Spec.map (CommRingCat.ofHom (algebraMap (↑Γ(X, U)) (Localization.Away f))))

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ IsAffineOpen (X.basicOpen f)

Tactic:
rw [← hU.fromSpec_image_basicOpen, Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion]

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ IsAffineOpen (PrimeSpectrum.basicOpen f)
-- Mathlib/CategoryTheory/Limits/Lattice.lean
theorem finite_coproduct_eq_finset_sup [SemilatticeSup α] [OrderBot α] {ι : Type u} [Fintype ι]
    (f : ι → α) : ∐ f = Fintype.elems.sup f

Proof state:
α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ (finiteColimitCocone (Discrete.functor f)).cocone.pt = Fintype.elems.sup f

Tactic:
change Finset.univ.sup (f ∘ discreteEquiv.toEmbedding) = Fintype.elems.sup f

Result:
α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ Finset.univ.sup (f ∘ ⇑discreteEquiv.toEmbedding) = Fintype.elems.sup f

Proof state:
α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ ∐ f = Fintype.elems.sup f

Tactic:
trans

Result:
α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ ∐ f = ?m.28048

α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ ?m.28048 = Fintype.elems.sup f

α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ α

Proof state:
α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ ∐ f = ?m.28048

Tactic:
exact
  (IsColimit.coconePointUniqueUpToIso (colimit.isColimit _)
      (finiteColimitCocone (Discrete.functor f)).isColimit).to_eq

Result:
no goals

Proof state:
α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ Finset.univ.sup (f ∘ ⇑discreteEquiv.toEmbedding) = Fintype.elems.sup f

Tactic:
simp only [← Finset.sup_map, Finset.univ_map_equiv_to_embedding]

Result:
α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ Finset.univ.sup f = Fintype.elems.sup f

Proof state:
α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ Finset.univ.sup f = Fintype.elems.sup f

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean
theorem integral_comp_smul_of_nonneg (f : E → F) (R : ℝ) {hR : 0 ≤ R} :
    ∫ x, f (R • x) ∂μ = (R ^ finrank ℝ E)⁻¹ • ∫ x, f x ∂μ

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
R : ℝ
hR : 0 ≤ R
⊢ ∫ (x : E), f (R • x) ∂μ = (R ^ finrank ℝ E)⁻¹ • ∫ (x : E), f x ∂μ

Tactic:
rw [integral_comp_smul μ f R, abs_of_nonneg (inv_nonneg.2 (pow_nonneg hR _))]

Result:
no goals
-- Mathlib/Data/List/GetD.lean
theorem getI_zero_eq_headI : l.getI 0 = l.headI

Proof state:
α : Type u
l : List α
inst✝ : Inhabited α
⊢ l.getI 0 = l.headI

Tactic:
cases l <;> rfl

Result:
no goals
-- Mathlib/Combinatorics/HalesJewett.lean
lemma apply_inr (h : l.idxFun i = Sum.inr e) : l x i = x e

Proof state:
η : Type u_5
α : Type u_6
ι : Type u_7
l : Subspace η α ι
x : η → α
i : ι
e : η
h : l.idxFun i = Sum.inr e
⊢ ↑l x i = x e

Tactic:
simp [apply_def, h]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem HasStrictDerivAt.smul_const (hc : HasStrictDerivAt c c' x) (f : F) :
    HasStrictDerivAt (fun y => c y • f) (c' • f) x

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasStrictDerivAt c c' x
f : F
this : HasStrictDerivAt (fun y => c y • f) (c x • 0 + c' • f) x
⊢ HasStrictDerivAt (fun y => c y • f) (c' • f) x

Tactic:
rwa [smul_zero, zero_add] at this

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasStrictDerivAt c c' x
f : F
⊢ HasStrictDerivAt (fun y => c y • f) (c' • f) x

Tactic:
have := hc.smul (hasStrictDerivAt_const x f)

Result:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasStrictDerivAt c c' x
f : F
this : HasStrictDerivAt (fun y => c y • f) (c x • 0 + c' • f) x
⊢ HasStrictDerivAt (fun y => c y • f) (c' • f) x