harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/FreeAbelianGroupFinsupp.lean
theorem support_zsmul (k : ℤ) (h : k ≠ 0) (a : FreeAbelianGroup X) :
    support (k • a) = support a

Proof state:
case h
X : Type u_1
k : ℤ
h : k ≠ 0
a : FreeAbelianGroup X
x : X
⊢ x ∈ (k • a).support ↔ x ∈ a.support

Tactic:
simp only [mem_support_iff, AddMonoidHom.map_zsmul]

Result:
case h
X : Type u_1
k : ℤ
h : k ≠ 0
a : FreeAbelianGroup X
x : X
⊢ k • (coeff x) a ≠ 0 ↔ (coeff x) a ≠ 0

Proof state:
X : Type u_1
k : ℤ
h : k ≠ 0
a : FreeAbelianGroup X
⊢ (k • a).support = a.support

Tactic:
ext x

Result:
case h
X : Type u_1
k : ℤ
h : k ≠ 0
a : FreeAbelianGroup X
x : X
⊢ x ∈ (k • a).support ↔ x ∈ a.support

Proof state:
case h
X : Type u_1
k : ℤ
h : k ≠ 0
a : FreeAbelianGroup X
x : X
⊢ k • (coeff x) a ≠ 0 ↔ (coeff x) a ≠ 0

Tactic:
simp only [h, zsmul_int_int, false_or, Ne, mul_eq_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Over.lean
@[simp]
lemma overEquiv_top {X : C} (Y : Over X) :
    overEquiv Y ⊤ = ⊤

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
Z : C
g : Z ⟶ Y.left
⊢ g = g ≫ (𝟙 Y).left

Tactic:
simp

Result:
no goals

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
Z : C
g : Z ⟶ Y.left
⊢ ((overEquiv Y) ⊤).arrows g ↔ ⊤.arrows g

Tactic:
simp only [top_apply, iff_true]

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
Z : C
g : Z ⟶ Y.left
⊢ ((overEquiv Y) ⊤).arrows g

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
Z : C
g : Z ⟶ Y.left
⊢ ((overEquiv Y) ⊤).arrows g

Tactic:
dsimp [overEquiv, Presieve.functorPushforward]

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
Z : C
g : Z ⟶ Y.left
⊢ ∃ Z_1 g_1 h, ⊤.arrows g_1 ∧ g = h ≫ g_1.left

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
Z : C
g : Z ⟶ Y.left
⊢ ∃ Z_1 g_1 h, ⊤.arrows g_1 ∧ g = h ≫ g_1.left

Tactic:
exact ⟨Y, 𝟙 Y, g, by simp, by simp⟩

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
⊢ (overEquiv Y) ⊤ = ⊤

Tactic:
ext Z g

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
Z : C
g : Z ⟶ Y.left
⊢ ((overEquiv Y) ⊤).arrows g ↔ ⊤.arrows g

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
Z : C
g : Z ⟶ Y.left
⊢ ⊤.arrows (𝟙 Y)

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
@[simp]
lemma valuation_pow (x : ℚ_[p]) : ∀ n : ℕ, (x ^ n).valuation = n * x.valuation
  | 0 => by simp
  | n + 1 => by
    obtain rfl | hx := eq_or_ne x 0
    · simp
    · simp [pow_succ, hx, valuation_mul, valuation_pow, _root_.add_one_mul]

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ (x ^ 0).valuation = ↑0 * x.valuation

Tactic:
simp

Result:
no goals

Proof state:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (0 ^ (n + 1)).valuation = ↑(n + 1) * valuation 0

Tactic:
simp

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℕ
⊢ (x ^ (n + 1)).valuation = ↑(n + 1) * x.valuation

Tactic:
obtain rfl | hx := eq_or_ne x 0

Result:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (0 ^ (n + 1)).valuation = ↑(n + 1) * valuation 0

case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℕ
hx : x ≠ 0
⊢ (x ^ (n + 1)).valuation = ↑(n + 1) * x.valuation

Proof state:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℕ
hx : x ≠ 0
⊢ (x ^ (n + 1)).valuation = ↑(n + 1) * x.valuation

Tactic:
simp [pow_succ, hx, valuation_mul, valuation_pow, _root_.add_one_mul]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/BigOperators.lean
theorem image_list_prod (f : F) :
    ∀ l : List (Set α), (f : α → β) '' l.prod = (l.map fun s => f '' s).prod
  | [] => image_one.trans <| congr_arg singleton (map_one f)
  | a :: as => by rw [List.map_cons, List.prod_cons, List.prod_cons, image_mul, image_list_prod _ _]

Proof state:
α : Type u_2
β : Type u_3
F : Type u_4
inst✝³ : FunLike F α β
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MonoidHomClass F α β
f : F
a : Set α
as : List (Set α)
⊢ ⇑f '' (a :: as).prod = (List.map (fun s => ⇑f '' s) (a :: as)).prod

Tactic:
rw [List.map_cons, List.prod_cons, List.prod_cons, image_mul, image_list_prod _ _]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/ConjAct.lean
theorem _root_.Subgroup.centralizer_eq_comap_stabilizer (g : G) :
    Subgroup.centralizer {g} = Subgroup.comap ConjAct.toConjAct.toMonoidHom
      (MulAction.stabilizer (ConjAct G) g)

Proof state:
case h
G : Type u_3
inst✝ : Group G
g k : G
⊢ g * k = k * g ↔ k ∈ comap toConjAct.toMonoidHom (stabilizer (ConjAct G) g)

Tactic:
rw [eq_comm]

Result:
case h
G : Type u_3
inst✝ : Group G
g k : G
⊢ k * g = g * k ↔ k ∈ comap toConjAct.toMonoidHom (stabilizer (ConjAct G) g)

Proof state:
case h
G : Type u_3
inst✝ : Group G
g k : G
⊢ k ∈ centralizer {g} ↔ k ∈ comap toConjAct.toMonoidHom (stabilizer (ConjAct G) g)

Tactic:
simp only [mem_centralizer_iff, Set.mem_singleton_iff, forall_eq, ConjAct.toConjAct_smul]

Result:
case h
G : Type u_3
inst✝ : Group G
g k : G
⊢ g * k = k * g ↔ k ∈ comap toConjAct.toMonoidHom (stabilizer (ConjAct G) g)

Proof state:
case h
G : Type u_3
inst✝ : Group G
g k : G
⊢ k * g = g * k ↔ k ∈ comap toConjAct.toMonoidHom (stabilizer (ConjAct G) g)

Tactic:
exact Iff.symm mul_inv_eq_iff_eq_mul

Result:
no goals

Proof state:
G : Type u_3
inst✝ : Group G
g : G
⊢ centralizer {g} = comap toConjAct.toMonoidHom (stabilizer (ConjAct G) g)

Tactic:
ext k

Result:
case h
G : Type u_3
inst✝ : Group G
g k : G
⊢ k ∈ centralizer {g} ↔ k ∈ comap toConjAct.toMonoidHom (stabilizer (ConjAct G) g)
-- Mathlib/Topology/ContinuousOn.lean
lemma Topology.IsEmbedding.map_nhdsWithin_eq {f : α → β} (hf : IsEmbedding f) (s : Set α) (x : α) :
    map f (𝓝[s] x) = 𝓝[f '' s] f x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsEmbedding f
s : Set α
x : α
⊢ map f (𝓝[s] x) = 𝓝[f '' s] f x

Tactic:
rw [nhdsWithin, Filter.map_inf hf.injective, hf.map_nhds_eq, map_principal, ← nhdsWithin_inter',
  inter_eq_self_of_subset_right (image_subset_range _ _)]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem mulVec_surjective_iff_isUnit {A : Matrix m m R} :
    Function.Surjective A.mulVec ↔ IsUnit A

Proof state:
m : Type u
inst✝² : DecidableEq m
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype m
A : Matrix m m R
⊢ Function.Surjective A.mulVec ↔ IsUnit A

Tactic:
rw [mulVec_surjective_iff_exists_right_inverse, exists_right_inverse_iff_isUnit]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem le_rank_root {self : UnionFind} {x : Nat} : self.rank x ≤ self.rank (self.rootD x)

Proof state:
self : UnionFind
x : Nat
h : ¬self.parent x = x
this : self.rankMax - self.rank (self.parent x) < self.rankMax - self.rank x
⊢ self.rank x ≤ self.rank (self.rootD x)

Tactic:
rw [← rootD_parent]

Result:
self : UnionFind
x : Nat
h : ¬self.parent x = x
this : self.rankMax - self.rank (self.parent x) < self.rankMax - self.rank x
⊢ self.rank x ≤ self.rank (self.rootD (self.parent x))

Proof state:
self : UnionFind
x : Nat
h : self.parent x = x
⊢ self.rank x ≤ self.rank (self.rootD x)

Tactic:
rw [rootD_eq_self.2 h]

Result:
self : UnionFind
x : Nat
h : self.parent x = x
⊢ self.rank x ≤ self.rank x

Proof state:
self : UnionFind
x : Nat
h : self.parent x = x
⊢ self.rank x ≤ self.rank x

Tactic:
exact Nat.le_refl ..

Result:
no goals

Proof state:
self : UnionFind
x : Nat
h : ¬self.parent x = x
this : self.rankMax - self.rank (self.parent x) < self.rankMax - self.rank x
⊢ self.rank x ≤ self.rank (self.rootD (self.parent x))

Tactic:
exact Nat.le_trans (Nat.le_of_lt (self.rank_lt h)) le_rank_root

Result:
no goals

Proof state:
self : UnionFind
x : Nat
h : ¬self.parent x = x
⊢ self.rank x ≤ self.rank (self.rootD x)

Tactic:
have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank_lt h)

Result:
self : UnionFind
x : Nat
h : ¬self.parent x = x
this : self.rankMax - self.rank (self.parent x) < self.rankMax - self.rank x
⊢ self.rank x ≤ self.rank (self.rootD x)

Proof state:
self : UnionFind
x : Nat
⊢ self.rank x ≤ self.rank (self.rootD x)

Tactic:
if h : self.parent x = x then
  rw [rootD_eq_self.2 h]; exact Nat.le_refl ..
else
  have := Nat.sub_lt_sub_left (self.lt_rankMax x) (self.rank_lt h)
  rw [← rootD_parent]
  exact Nat.le_trans (Nat.le_of_lt (self.rank_lt h)) le_rank_root

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey_modify (h : m.1.WF) [Inhabited α] {k k' : α} {f : β k → β k}
    (hc : (m.modify k f).contains k') :
    (m.modify k f).getKey k' hc =
      if heq : k == k' then
        k
      else
        haveI h' : m.contains k'

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.val.WF
inst✝ : Inhabited α
k k' : α
f : β k → β k
hc : (m.modify k f).contains k' = true
⊢ (m.modify k f).getKey k' hc = if heq : (k == k') = true then k else m.getKey k' ⋯

Tactic:
simp_to_model [modify] using List.getKey_modifyKey

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.val.WF
inst✝ : Inhabited α
k k' : α
f : β k → β k
hc : (m.modify k f).contains k' = true
heq : ¬(k == k') = true
⊢ m.contains k' = true

Tactic:
rwa [contains_modify _ h] at hc

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem Monic.natDegree_eq_zero (hf : p.Monic) : p.natDegree = 0 ↔ p = 1 :=
  ⟨eq_one_of_monic_natDegree_zero hf, by rintro rfl; simp⟩

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hf : p.Monic
⊢ p = 1 → p.natDegree = 0

Tactic:
rintro rfl

Result:
R : Type u
inst✝ : Semiring R
hf : Monic 1
⊢ natDegree 1 = 0

Proof state:
R : Type u
inst✝ : Semiring R
hf : Monic 1
⊢ natDegree 1 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Localization/FractionRing.lean
lemma fieldEquivOfAlgEquivHom_injective :
    Function.Injective (fieldEquivOfAlgEquivHom K L : (B ≃ₐ[A] B) →* (L ≃ₐ[K] L))

Proof state:
A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra A B
K : Type u_10
L : Type u_11
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsFractionRing A K
inst✝⁴ : IsFractionRing B L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A B L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower A K L
f g : B ≃ₐ[A] B
h : (fieldEquivOfAlgEquivHom K L) f = (fieldEquivOfAlgEquivHom K L) g
⊢ f = g

Tactic:
ext b

Result:
case h
A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra A B
K : Type u_10
L : Type u_11
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsFractionRing A K
inst✝⁴ : IsFractionRing B L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A B L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower A K L
f g : B ≃ₐ[A] B
h : (fieldEquivOfAlgEquivHom K L) f = (fieldEquivOfAlgEquivHom K L) g
b : B
⊢ f b = g b

Proof state:
case h
A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra A B
K : Type u_10
L : Type u_11
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsFractionRing A K
inst✝⁴ : IsFractionRing B L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A B L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower A K L
f g : B ≃ₐ[A] B
h : (fieldEquivOfAlgEquivHom K L) f = (fieldEquivOfAlgEquivHom K L) g
b : B
⊢ f b = g b

Tactic:
simpa using AlgEquiv.ext_iff.mp h (algebraMap B L b)

Result:
no goals

Proof state:
A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra A B
K : Type u_10
L : Type u_11
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsFractionRing A K
inst✝⁴ : IsFractionRing B L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A B L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower A K L
⊢ Injective ⇑(fieldEquivOfAlgEquivHom K L)

Tactic:
intro f g h

Result:
A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra A B
K : Type u_10
L : Type u_11
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsFractionRing A K
inst✝⁴ : IsFractionRing B L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A B L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower A K L
f g : B ≃ₐ[A] B
h : (fieldEquivOfAlgEquivHom K L) f = (fieldEquivOfAlgEquivHom K L) g
⊢ f = g
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
lemma nilRank_le_card {ι : Type*} [Fintype ι] (b : Basis ι R M) : nilRank φ ≤ Fintype.card ι

Proof state:
case h
R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Finite R L
inst✝² : Free R L
inst✝¹ : Nontrivial R
ι : Type u_8
inst✝ : Fintype ι
b : Basis ι R M
⊢ 1 ≠ 0

Tactic:
apply one_ne_zero

Result:
no goals

Proof state:
case h
R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Finite R L
inst✝² : Free R L
inst✝¹ : Nontrivial R
ι : Type u_8
inst✝ : Fintype ι
b : Basis ι R M
⊢ (φ.polyCharpoly (chooseBasis R L)).coeff (Fintype.card ι) ≠ 0

Tactic:
rw [← Module.finrank_eq_card_basis b, ← polyCharpoly_natDegree φ (chooseBasis R L),
  Polynomial.coeff_natDegree, (polyCharpoly_monic _ _).leadingCoeff]

Result:
case h
R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Finite R L
inst✝² : Free R L
inst✝¹ : Nontrivial R
ι : Type u_8
inst✝ : Fintype ι
b : Basis ι R M
⊢ 1 ≠ 0

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Finite R L
inst✝² : Free R L
inst✝¹ : Nontrivial R
ι : Type u_8
inst✝ : Fintype ι
b : Basis ι R M
⊢ φ.nilRank ≤ Fintype.card ι

Tactic:
apply Polynomial.natTrailingDegree_le_of_ne_zero

Result:
case h
R : Type u_1
L : Type u_2
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : Module.Finite R L
inst✝² : Free R L
inst✝¹ : Nontrivial R
ι : Type u_8
inst✝ : Fintype ι
b : Basis ι R M
⊢ (φ.polyCharpoly (chooseBasis R L)).coeff (Fintype.card ι) ≠ 0
-- Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
theorem isEquivalent_zero_iff_isBigO_zero : u ~[l] 0 ↔ u =O[l] (0 : α → β)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
h : u =O[l] 0
⊢ ∃ s ∈ l, Set.EqOn u 0 s

Tactic:
exact ⟨{ x : α | u x = 0 }, isBigO_zero_right_iff.mp h, fun x hx ↦ hx⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
h : u =O[l] 0
⊢ u ~[l] 0

Tactic:
rw [isEquivalent_zero_iff_eventually_zero, eventuallyEq_iff_exists_mem]

Result:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
h : u =O[l] 0
⊢ ∃ s ∈ l, Set.EqOn u 0 s

Proof state:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
⊢ u ~[l] 0 ↔ u =O[l] 0

Tactic:
refine ⟨IsEquivalent.isBigO, fun h ↦ ?_⟩

Result:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
h : u =O[l] 0
⊢ u ~[l] 0
-- Mathlib/Data/Num/Lemmas.lean
theorem cast_to_nat [AddMonoidWithOne α] : ∀ n : PosNum, ((n : ℕ) : α) = n
  | 1 => Nat.cast_one
  | bit0 p => by dsimp; rw [Nat.cast_add, p.cast_to_nat]
  | bit1 p => by dsimp; rw [Nat.cast_add, Nat.cast_add, Nat.cast_one, p.cast_to_nat]

Proof state:
α : Type u_1
inst✝ : AddMonoidWithOne α
p : PosNum
⊢ ↑(↑p + ↑p) = ↑p + ↑p

Tactic:
rw [Nat.cast_add, p.cast_to_nat]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : AddMonoidWithOne α
p : PosNum
⊢ ↑↑p.bit0 = ↑p.bit0

Tactic:
dsimp

Result:
α : Type u_1
inst✝ : AddMonoidWithOne α
p : PosNum
⊢ ↑(↑p + ↑p) = ↑p + ↑p

Proof state:
α : Type u_1
inst✝ : AddMonoidWithOne α
p : PosNum
⊢ ↑↑p.bit1 = ↑p.bit1

Tactic:
dsimp

Result:
α : Type u_1
inst✝ : AddMonoidWithOne α
p : PosNum
⊢ ↑(↑p + ↑p + 1) = ↑p + ↑p + 1

Proof state:
α : Type u_1
inst✝ : AddMonoidWithOne α
p : PosNum
⊢ ↑(↑p + ↑p + 1) = ↑p + ↑p + 1

Tactic:
rw [Nat.cast_add, Nat.cast_add, Nat.cast_one, p.cast_to_nat]

Result:
no goals
-- Mathlib/Analysis/RCLike/Inner.lean
lemma wInner_one_eq_sum (f g : ∀ i, E i) : ⟪f, g⟫_[𝕜] = ∑ i, inner (f i) (g i)

Proof state:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : RCLike 𝕜
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (E i)
f g : (i : ι) → E i
⊢ wInner 1 f g = ∑ i : ι, inner (f i) (g i)

Tactic:
simp [wInner]

Result:
no goals
-- Mathlib/Analysis/Calculus/AddTorsor/AffineMap.lean
theorem contDiff {n : WithTop ℕ∞} (f : V →ᴬ[𝕜] W) : ContDiff 𝕜 n f

Proof state:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace 𝕜 W
n : WithTop ℕ∞
f : V →ᴬ[𝕜] W
⊢ ContDiff 𝕜 n (⇑f.contLinear + Function.const V (f 0))

Tactic:
apply f.contLinear.contDiff.add

Result:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace 𝕜 W
n : WithTop ℕ∞
f : V →ᴬ[𝕜] W
⊢ ContDiff 𝕜 n (Function.const V (f 0))

Proof state:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace 𝕜 W
n : WithTop ℕ∞
f : V →ᴬ[𝕜] W
⊢ ContDiff 𝕜 n ⇑f

Tactic:
rw [f.decomp]

Result:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace 𝕜 W
n : WithTop ℕ∞
f : V →ᴬ[𝕜] W
⊢ ContDiff 𝕜 n (⇑f.contLinear + Function.const V (f 0))

Proof state:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace 𝕜 W
n : WithTop ℕ∞
f : V →ᴬ[𝕜] W
⊢ ContDiff 𝕜 n (Function.const V (f 0))

Tactic:
exact contDiff_const

Result:
no goals
-- Mathlib/FieldTheory/Finite/Basic.lean
theorem Nat.sq_add_sq_zmodEq (p : ℕ) [Fact p.Prime] (x : ℤ) :
    ∃ a b : ℕ, a ≤ p / 2 ∧ b ≤ p / 2 ∧ (a : ℤ) ^ 2 + (b : ℤ) ^ 2 ≡ x [ZMOD p]

Proof state:
case intro.intro
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : ↑a.valMinAbs ^ 2 + ↑b.valMinAbs ^ 2 = ↑x
⊢ ↑a.valMinAbs.natAbs ^ 2 + ↑b.valMinAbs.natAbs ^ 2 ≡ x [ZMOD ↑p]

Tactic:
push_cast

Result:
case intro.intro
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : ↑a.valMinAbs ^ 2 + ↑b.valMinAbs ^ 2 = ↑x
⊢ |a.valMinAbs| ^ 2 + |b.valMinAbs| ^ 2 ≡ x [ZMOD ↑p]

Proof state:
case intro.intro
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : ↑a.valMinAbs ^ 2 + ↑b.valMinAbs ^ 2 = ↑x
⊢ |a.valMinAbs| ^ 2 + |b.valMinAbs| ^ 2 ≡ x [ZMOD ↑p]

Tactic:
rw [sq_abs, sq_abs, ← ZMod.intCast_eq_intCast_iff]

Result:
case intro.intro
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : ↑a.valMinAbs ^ 2 + ↑b.valMinAbs ^ 2 = ↑x
⊢ ↑(a.valMinAbs ^ 2 + b.valMinAbs ^ 2) = ↑x

Proof state:
case intro.intro
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : ↑a.valMinAbs ^ 2 + ↑b.valMinAbs ^ 2 = ↑x
⊢ ↑(a.valMinAbs ^ 2 + b.valMinAbs ^ 2) = ↑x

Tactic:
exact mod_cast hx

Result:
no goals

Proof state:
case intro.intro
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : a ^ 2 + b ^ 2 = ↑x
⊢ ∃ a b, a ≤ p / 2 ∧ b ≤ p / 2 ∧ ↑a ^ 2 + ↑b ^ 2 ≡ x [ZMOD ↑p]

Tactic:
refine ⟨a.valMinAbs.natAbs, b.valMinAbs.natAbs, ZMod.natAbs_valMinAbs_le _,
  ZMod.natAbs_valMinAbs_le _, ?_⟩

Result:
case intro.intro
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : a ^ 2 + b ^ 2 = ↑x
⊢ ↑a.valMinAbs.natAbs ^ 2 + ↑b.valMinAbs.natAbs ^ 2 ≡ x [ZMOD ↑p]

Proof state:
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
⊢ ∃ a b, a ≤ p / 2 ∧ b ≤ p / 2 ∧ ↑a ^ 2 + ↑b ^ 2 ≡ x [ZMOD ↑p]

Tactic:
rcases ZMod.sq_add_sq p x with ⟨a, b, hx⟩

Result:
case intro.intro
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : a ^ 2 + b ^ 2 = ↑x
⊢ ∃ a b, a ≤ p / 2 ∧ b ≤ p / 2 ∧ ↑a ^ 2 + ↑b ^ 2 ≡ x [ZMOD ↑p]

Proof state:
case intro.intro
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : a ^ 2 + b ^ 2 = ↑x
⊢ ↑a.valMinAbs.natAbs ^ 2 + ↑b.valMinAbs.natAbs ^ 2 ≡ x [ZMOD ↑p]

Tactic:
rw [← a.coe_valMinAbs, ← b.coe_valMinAbs] at hx

Result:
case intro.intro
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : ↑a.valMinAbs ^ 2 + ↑b.valMinAbs ^ 2 = ↑x
⊢ ↑a.valMinAbs.natAbs ^ 2 + ↑b.valMinAbs.natAbs ^ 2 ≡ x [ZMOD ↑p]
-- Mathlib/LinearAlgebra/Reflection.lean
/-- A formula for $(r_1 r_2)^m$, where $m$ is a natural number. -/
lemma reflection_mul_reflection_pow (m : ℕ)
    (t : R := f y * g x - 2) (ht : t = f y * g x - 2

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
m : ℕ
t : optParam R (f y * g x - 2)
ht : autoParam (t = f y * g x - 2) _auto✝
z : M
⊢ ↑((reflection hf * reflection hg) ^ m) z =
    (LinearMap.id +
          (Polynomial.eval t (S R ((↑m - 2) / 2)) *
              (Polynomial.eval t (S R ((↑m - 1) / 2)) + Polynomial.eval t (S R ((↑m - 3) / 2)))) •
            (LinearMap.smulRight (g x • f - g) y - LinearMap.smulRight f x) +
        (Polynomial.eval t (S R ((↑m - 1) / 2)) *
            (Polynomial.eval t (S R (↑m / 2)) + Polynomial.eval t (S R ((↑m - 2) / 2)))) •
          (LinearMap.smulRight (f y • g - f) x - LinearMap.smulRight g y))
      z

Tactic:
simpa using reflection_mul_reflection_pow_apply hf hg m z t ht

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
m : ℕ
t : optParam R (f y * g x - 2)
ht : autoParam (t = f y * g x - 2) _auto✝
⊢ ↑((reflection hf * reflection hg) ^ m) =
    LinearMap.id +
        (Polynomial.eval t (S R ((↑m - 2) / 2)) *
            (Polynomial.eval t (S R ((↑m - 1) / 2)) + Polynomial.eval t (S R ((↑m - 3) / 2)))) •
          (LinearMap.smulRight (g x • f - g) y - LinearMap.smulRight f x) +
      (Polynomial.eval t (S R ((↑m - 1) / 2)) *
          (Polynomial.eval t (S R (↑m / 2)) + Polynomial.eval t (S R ((↑m - 2) / 2)))) •
        (LinearMap.smulRight (f y • g - f) x - LinearMap.smulRight g y)

Tactic:
ext z

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
f g : Dual R M
hf : f x = 2
hg : g y = 2
m : ℕ
t : optParam R (f y * g x - 2)
ht : autoParam (t = f y * g x - 2) _auto✝
z : M
⊢ ↑((reflection hf * reflection hg) ^ m) z =
    (LinearMap.id +
          (Polynomial.eval t (S R ((↑m - 2) / 2)) *
              (Polynomial.eval t (S R ((↑m - 1) / 2)) + Polynomial.eval t (S R ((↑m - 3) / 2)))) •
            (LinearMap.smulRight (g x • f - g) y - LinearMap.smulRight f x) +
        (Polynomial.eval t (S R ((↑m - 1) / 2)) *
            (Polynomial.eval t (S R (↑m / 2)) + Polynomial.eval t (S R ((↑m - 2) / 2)))) •
          (LinearMap.smulRight (f y • g - f) x - LinearMap.smulRight g y))
      z
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
lemma natDegree_ΨSq_le (n : ℤ) : (W.ΨSq n).natDegree ≤ n.natAbs ^ 2 - 1

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (W.ΨSq n).natDegree ≤ n.natAbs ^ 2 - 1

Tactic:
induction n using Int.negInduction with
| nat n => exact (W.natDegree_coeff_ΨSq_ofNat n).left
| neg ih => simp only [ΨSq_neg, Int.natAbs_neg, ih]

Result:
no goals

Proof state:
case nat
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ (W.ΨSq ↑n).natDegree ≤ (↑n).natAbs ^ 2 - 1

Tactic:
exact (W.natDegree_coeff_ΨSq_ofNat n).left

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), (W.ΨSq ↑n).natDegree ≤ (↑n).natAbs ^ 2 - 1
n✝ : ℕ
⊢ (W.ΨSq (-↑n✝)).natDegree ≤ (-↑n✝).natAbs ^ 2 - 1

Tactic:
simp only [ΨSq_neg, Int.natAbs_neg, ih]

Result:
no goals