harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/LemmasAux.lean
theorem toNat_sub_self_max (a : Int) : (a - max 0 a).toNat = 0

Proof state:
a : Int
⊢ (a - max 0 a).toNat = 0

Tactic:
simp [toNat]

Result:
a : Int
⊢ (match a - max 0 a with
    | ofNat n => n
    | -[a+1] => 0) =
    0

Proof state:
a : Int
⊢ (match a - max 0 a with
    | ofNat n => n
    | -[a+1] => 0) =
    0

Tactic:
split <;> simp_all <;> omega

Result:
no goals
-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem preimage_symm_proj_inter (s : Set B) :
    e.toPartialEquiv.symm ⁻¹' (proj ⁻¹' s) ∩ e.baseSet ×ˢ univ = (s ∩ e.baseSet) ×ˢ univ

Proof state:
case h.mk
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
s : Set B
x : B
y : F
h : x ∈ e.baseSet
⊢ proj (↑e.symm (x, y)) ∈ s ↔ x ∈ s

Tactic:
rw [e.proj_symm_apply' h]

Result:
no goals

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
s : Set B
x : B
y : F
this : x ∈ e.baseSet → (proj (↑e.symm (x, y)) ∈ s ↔ x ∈ s)
⊢ (x, y) ∈ ↑e.symm ⁻¹' (proj ⁻¹' s) ∩ e.baseSet ×ˢ univ ↔ (x, y) ∈ (s ∩ e.baseSet) ×ˢ univ

Tactic:
simpa only [prod_mk_mem_set_prod_eq, mem_inter_iff, and_true, mem_univ, and_congr_left_iff]

Result:
no goals

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
s : Set B
⊢ ↑e.symm ⁻¹' (proj ⁻¹' s) ∩ e.baseSet ×ˢ univ = (s ∩ e.baseSet) ×ˢ univ

Tactic:
ext ⟨x, y⟩

Result:
case h.mk
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
s : Set B
x : B
y : F
⊢ (x, y) ∈ ↑e.symm ⁻¹' (proj ⁻¹' s) ∩ e.baseSet ×ˢ univ ↔ (x, y) ∈ (s ∩ e.baseSet) ×ˢ univ

Proof state:
case h.mk
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
s : Set B
x : B
y : F
⊢ (x, y) ∈ ↑e.symm ⁻¹' (proj ⁻¹' s) ∩ e.baseSet ×ˢ univ ↔ (x, y) ∈ (s ∩ e.baseSet) ×ˢ univ

Tactic:
suffices x ∈ e.baseSet → (proj (e.toPartialEquiv.symm (x, y)) ∈ s ↔ x ∈ s) by
  simpa only [prod_mk_mem_set_prod_eq, mem_inter_iff, and_true, mem_univ, and_congr_left_iff]

Result:
case h.mk
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
s : Set B
x : B
y : F
⊢ x ∈ e.baseSet → (proj (↑e.symm (x, y)) ∈ s ↔ x ∈ s)

Proof state:
case h.mk
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
s : Set B
x : B
y : F
⊢ x ∈ e.baseSet → (proj (↑e.symm (x, y)) ∈ s ↔ x ∈ s)

Tactic:
intro h

Result:
case h.mk
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
s : Set B
x : B
y : F
h : x ∈ e.baseSet
⊢ proj (↑e.symm (x, y)) ∈ s ↔ x ∈ s
-- Mathlib/Data/Fin/Basic.lean
theorem pred_castSucc_lt_iff {a b : Fin (n + 1)} (ha : castSucc a ≠ 0) :
    (castSucc a).pred ha < b ↔ a ≤ b

Proof state:
n : ℕ
a b : Fin (n + 1)
ha : a.castSucc ≠ 0
⊢ a.castSucc.pred ha < b ↔ a ≤ b

Tactic:
rw [pred_lt_iff, castSucc_lt_succ_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean
theorem reverse_apply (x : CliffordAlgebra Q) : reverse (R := ℝ) x = x

Proof state:
case mul
x₁ x₂ : CliffordAlgebra Q
hx₁ : reverse x₁ = x₁
hx₂ : reverse x₂ = x₂
⊢ reverse (x₁ * x₂) = x₁ * x₂

Tactic:
rw [reverse.map_mul, mul_comm, hx₁, hx₂]

Result:
no goals

Proof state:
x : CliffordAlgebra Q
⊢ reverse x = x

Tactic:
induction x using CliffordAlgebra.induction with
| algebraMap r => exact reverse.commutes _
| ι x => rw [reverse_ι]
| mul x₁ x₂ hx₁ hx₂ => rw [reverse.map_mul, mul_comm, hx₁, hx₂]
| add x₁ x₂ hx₁ hx₂ => rw [reverse.map_add, hx₁, hx₂]

Result:
no goals

Proof state:
case add
x₁ x₂ : CliffordAlgebra Q
hx₁ : reverse x₁ = x₁
hx₂ : reverse x₂ = x₂
⊢ reverse (x₁ + x₂) = x₁ + x₂

Tactic:
rw [reverse.map_add, hx₁, hx₂]

Result:
no goals

Proof state:
case algebraMap
r : ℝ
⊢ reverse ((algebraMap ℝ (CliffordAlgebra Q)) r) = (algebraMap ℝ (CliffordAlgebra Q)) r

Tactic:
exact reverse.commutes _

Result:
no goals

Proof state:
case ι
x : ℝ
⊢ reverse ((ι Q) x) = (ι Q) x

Tactic:
rw [reverse_ι]

Result:
no goals
-- Mathlib/Data/Finsupp/AList.lean
theorem lookupFinsupp_eq_iff_of_ne_zero [DecidableEq α] {l : AList fun _x : α => M} {a : α} {x : M}
    (hx : x ≠ 0) : l.lookupFinsupp a = x ↔ x ∈ l.lookup a

Proof state:
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
x : M
hx : x ≠ 0
⊢ (lookup a l).getD 0 = x ↔ x ∈ lookup a l

Tactic:
rcases lookup a l with - | m <;> simp [hx.symm]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
x : M
hx : x ≠ 0
⊢ l.lookupFinsupp a = x ↔ x ∈ lookup a l

Tactic:
rw [lookupFinsupp_apply]

Result:
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
x : M
hx : x ≠ 0
⊢ (lookup a l).getD 0 = x ↔ x ∈ lookup a l
-- Mathlib/Algebra/CharP/Basic.lean
/-- If a ring `R` is of characteristic `p`, then for any prime number `q` different from `p`,
it is not zero in `R`. -/
lemma cast_ne_zero_of_ne_of_prime [Nontrivial R]
    {p q : ℕ} [CharP R p] (hq : q.Prime) (hneq : p ≠ q) : (q : R) ≠ 0 := fun h ↦ by
  rw [cast_eq_zero_iff R p q] at h
  rcases hq.eq_one_or_self_of_dvd _ h with h | h
  · subst h
    exact false_of_nontrivial_of_char_one (R := R)
  · exact hneq h

Proof state:
case inr
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
p q : ℕ
inst✝ : CharP R p
hq : Nat.Prime q
hneq : p ≠ q
h✝ : p ∣ q
h : p = q
⊢ False

Tactic:
exact hneq h

Result:
no goals

Proof state:
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
p q : ℕ
inst✝ : CharP R p
hq : Nat.Prime q
hneq : p ≠ q
h : p ∣ q
⊢ False

Tactic:
rcases hq.eq_one_or_self_of_dvd _ h with h | h

Result:
case inl
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
p q : ℕ
inst✝ : CharP R p
hq : Nat.Prime q
hneq : p ≠ q
h✝ : p ∣ q
h : p = 1
⊢ False

case inr
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
p q : ℕ
inst✝ : CharP R p
hq : Nat.Prime q
hneq : p ≠ q
h✝ : p ∣ q
h : p = q
⊢ False

Proof state:
case inl
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
p q : ℕ
inst✝ : CharP R p
hq : Nat.Prime q
hneq : p ≠ q
h✝ : p ∣ q
h : p = 1
⊢ False

Tactic:
subst h

Result:
case inl
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
q : ℕ
hq : Nat.Prime q
inst✝ : CharP R 1
hneq : 1 ≠ q
h : 1 ∣ q
⊢ False

Proof state:
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
p q : ℕ
inst✝ : CharP R p
hq : Nat.Prime q
hneq : p ≠ q
h : ↑q = 0
⊢ False

Tactic:
rw [cast_eq_zero_iff R p q] at h

Result:
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
p q : ℕ
inst✝ : CharP R p
hq : Nat.Prime q
hneq : p ≠ q
h : p ∣ q
⊢ False

Proof state:
case inl
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : Nontrivial R
q : ℕ
hq : Nat.Prime q
inst✝ : CharP R 1
hneq : 1 ≠ q
h : 1 ∣ q
⊢ False

Tactic:
exact false_of_nontrivial_of_char_one (R := R)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey_modifyKey [BEq α] [LawfulBEq α] [Inhabited α] {k k' : α} {f : β k → β k}
    (l : List ((a : α) × β a)) (hl : DistinctKeys l) (h : containsKey k' (modifyKey k f l)) :
    getKey k' (modifyKey k f l) h =
      if k == k' then
        k
      else
        haveI h' : containsKey k' l

Proof state:
α : Type u
β : α → Type v
γ : α → Type w
inst✝² : BEq α
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : β k → β k
l : List ((a : α) × β a)
hl : DistinctKeys l
h : containsKey k' (modifyKey k f l) = true
⊢ containsKey k' l = true

Tactic:
rwa [containsKey_modifyKey] at h

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : β k → β k
l : List ((a : α) × β a)
hl : DistinctKeys l
h : containsKey k' (modifyKey k f l) = true
⊢ getKey k' (modifyKey k f l) h = if (k == k') = true then k else getKey k' l ⋯

Tactic:
simp [modifyKey_eq_alterKey, getKey_alterKey, hl, ← dite_eq_ite]

Result:
no goals
-- Mathlib/Algebra/Ring/Units.lean
theorem divp_sub (a b : α) (u : αˣ) : a /ₚ u - b = (a - b * u) /ₚ u

Proof state:
α : Type u
inst✝ : Ring α
a b : α
u : αˣ
⊢ b = b * ↑u * ↑u⁻¹

Tactic:
rw [mul_assoc, Units.mul_inv, mul_one]

Result:
no goals

Proof state:
α : Type u
inst✝ : Ring α
a b : α
u : αˣ
⊢ a /ₚ u - b = (a - b * ↑u) /ₚ u

Tactic:
simp only [divp, sub_mul, sub_right_inj]

Result:
α : Type u
inst✝ : Ring α
a b : α
u : αˣ
⊢ b = b * ↑u * ↑u⁻¹
-- Mathlib/Algebra/Polynomial/Eval/SMul.lean
theorem smul_comp [Monoid S] [DistribMulAction S R] [IsScalarTower S R R] (s : S) (p q : R[X]) :
    (s • p).comp q = s • p.comp q

Proof state:
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Monoid S
inst✝¹ : DistribMulAction S R
inst✝ : IsScalarTower S R R
s : S
p q : R[X]
⊢ (s • p).comp q = s • p.comp q

Tactic:
rw [← smul_one_smul R s p, comp, comp, eval₂_smul, ← smul_eq_C_mul, smul_assoc, one_smul]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Basis.lean
theorem toMatrix_map_vecMul {S : Type*} [Ring S] [Algebra R S] [Fintype ι] (b : Basis ι R S)
    (v : ι' → S) : b ᵥ* ((b.toMatrix v).map <| algebraMap R S) = v

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_5
inst✝³ : CommSemiring R
S : Type u_9
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
v : ι' → S
⊢ ⇑b ᵥ* (b.toMatrix v).map ⇑(algebraMap R S) = v

Tactic:
ext i

Result:
case h
ι : Type u_1
ι' : Type u_2
R : Type u_5
inst✝³ : CommSemiring R
S : Type u_9
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
v : ι' → S
i : ι'
⊢ (⇑b ᵥ* (b.toMatrix v).map ⇑(algebraMap R S)) i = v i

Proof state:
case h
ι : Type u_1
ι' : Type u_2
R : Type u_5
inst✝³ : CommSemiring R
S : Type u_9
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Fintype ι
b : Basis ι R S
v : ι' → S
i : ι'
⊢ (⇑b ᵥ* (b.toMatrix v).map ⇑(algebraMap R S)) i = v i

Tactic:
simp_rw [vecMul, dotProduct, Matrix.map_apply, ← Algebra.commutes, ← Algebra.smul_def,
  sum_toMatrix_smul_self]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Free.lean
/-- A free module of rank zero is trivial. -/
lemma subsingleton_of_rank_zero (h : Module.rank R M = 0) : Subsingleton M

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : StrongRankCondition R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
h : IsEmpty (ChooseBasisIndex R M)
⊢ Subsingleton M

Tactic:
exact (Module.Free.repr R M).subsingleton

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : StrongRankCondition R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
h : Module.rank R M = 0
⊢ Subsingleton M

Tactic:
rw [← Basis.mk_eq_rank'' (Module.Free.chooseBasis R M), Cardinal.mk_eq_zero_iff] at h

Result:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : StrongRankCondition R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
h : IsEmpty (ChooseBasisIndex R M)
⊢ Subsingleton M
-- Mathlib/Data/Nat/Order/Lemmas.lean
lemma exists_not_and_succ_of_not_zero_of_exists {p : ℕ → Prop} (H' : ¬ p 0) (H : ∃ n, p n) :
    ∃ n, ¬ p n ∧ p (n + 1)

Proof state:
p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
k : ℕ := Nat.find H
hk : p k
⊢ ∃ n, ¬p n ∧ p (n + 1)

Tactic:
suffices 0 < k from
  ⟨k - 1, Nat.find_min H <| Nat.pred_lt this.ne', by rwa [Nat.sub_add_cancel this]⟩

Result:
p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
k : ℕ := Nat.find H
hk : p k
⊢ 0 < k

Proof state:
p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
k : ℕ := Nat.find H
hk : p k
contra : k = 0
⊢ False

Tactic:
exact H' (contra ▸ hk)

Result:
no goals

Proof state:
p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
k : ℕ := Nat.find H
⊢ ∃ n, ¬p n ∧ p (n + 1)

Tactic:
have hk : p k := Nat.find_spec H

Result:
p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
k : ℕ := Nat.find H
hk : p k
⊢ ∃ n, ¬p n ∧ p (n + 1)

Proof state:
p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
k : ℕ := Nat.find H
hk : p k
this : 0 < k
⊢ p (k - 1 + 1)

Tactic:
rwa [Nat.sub_add_cancel this]

Result:
no goals

Proof state:
p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
k : ℕ := Nat.find H
hk : p k
contra : k ≤ 0
⊢ False

Tactic:
rw [le_zero_eq] at contra

Result:
p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
k : ℕ := Nat.find H
hk : p k
contra : k = 0
⊢ False

Proof state:
p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
k : ℕ := Nat.find H
hk : p k
⊢ 0 < k

Tactic:
by_contra! contra

Result:
p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
k : ℕ := Nat.find H
hk : p k
contra : k ≤ 0
⊢ False

Proof state:
p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
⊢ ∃ n, ¬p n ∧ p (n + 1)

Tactic:
let k := Nat.find H

Result:
p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
k : ℕ := Nat.find H
⊢ ∃ n, ¬p n ∧ p (n + 1)

Proof state:
p : ℕ → Prop
H' : ¬p 0
H : ∃ n, p n
⊢ ∃ n, ¬p n ∧ p (n + 1)

Tactic:
classical
let k := Nat.find H
have hk : p k := Nat.find_spec H
suffices 0 < k from
  ⟨k - 1, Nat.find_min H <| Nat.pred_lt this.ne', by rwa [Nat.sub_add_cancel this]⟩
by_contra! contra
rw [le_zero_eq] at contra
exact H' (contra ▸ hk)

Result:
no goals
-- Mathlib/Data/Multiset/Count.lean
theorem count_eq_card {a : α} {s} : count a s = card s ↔ ∀ x ∈ s, a = x

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ count a s = s.card ↔ ∀ x ∈ s, a = x

Tactic:
simp [countP_eq_card, count, @eq_comm _ a]

Result:
no goals
-- Mathlib/RingTheory/Valuation/Archimedean.lean
lemma wfDvdMonoid_iff_wellFounded_gt_on_v (hv : Integers v O) :
    WfDvdMonoid O ↔ WellFounded ((· > ·) on (v ∘ algebraMap O F))

Proof state:
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : CommRing O
inst✝ : Algebra O F
v : Valuation F Γ₀
hv : v.Integers O
⊢ WfDvdMonoid O ↔ WellFounded ((fun x1 x2 => x1 > x2) on ⇑v ∘ ⇑(algebraMap O F))

Tactic:
refine ⟨fun _ ↦ wellFounded_dvdNotUnit.mono ?_, fun h ↦ ⟨h.mono ?_⟩⟩ <;>
simp [Function.onFun, hv.dvdNotUnit_iff_lt]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem mul_pos {a b : Int} (ha : 0 < a) (hb : 0 < b) : 0 < a * b

Proof state:
a b : Int
ha : 0 < a
hb : 0 < b
n : Nat
hn : a = ↑n.succ
m : Nat
hm : b = ↑m.succ
⊢ 0 < ↑(n.succ * m.succ)

Tactic:
apply ofNat_succ_pos

Result:
no goals

Proof state:
a b : Int
ha : 0 < a
hb : 0 < b
⊢ 0 < a * b

Tactic:
let ⟨n, hn⟩ := eq_succ_of_zero_lt ha

Result:
a b : Int
ha : 0 < a
hb : 0 < b
n : Nat
hn : a = ↑n.succ
⊢ 0 < a * b

Proof state:
a b : Int
ha : 0 < a
hb : 0 < b
n : Nat
hn : a = ↑n.succ
⊢ 0 < a * b

Tactic:
let ⟨m, hm⟩ := eq_succ_of_zero_lt hb

Result:
a b : Int
ha : 0 < a
hb : 0 < b
n : Nat
hn : a = ↑n.succ
m : Nat
hm : b = ↑m.succ
⊢ 0 < a * b

Proof state:
a b : Int
ha : 0 < a
hb : 0 < b
n : Nat
hn : a = ↑n.succ
m : Nat
hm : b = ↑m.succ
⊢ 0 < a * b

Tactic:
rw [hn, hm, ← ofNat_mul]

Result:
a b : Int
ha : 0 < a
hb : 0 < b
n : Nat
hn : a = ↑n.succ
m : Nat
hm : b = ↑m.succ
⊢ 0 < ↑(n.succ * m.succ)
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
@[to_additive] lemma prod_range_succ (f : ℕ → M) (n : ℕ) :
    ((range n.succ).map f).prod = ((range n).map f).prod * f n

Proof state:
M : Type u_4
inst✝ : Monoid M
f : ℕ → M
n : ℕ
⊢ (map f (range n.succ)).prod = (map f (range n)).prod * f n

Tactic:
rw [range_succ, map_append, map_singleton, prod_append, prod_cons, prod_nil, mul_one]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Pi.lean
theorem MonoidHom.functions_ext [Finite I] (G : Type*) [CommMonoid G] (g h : (∀ i, Z i) →* G)
    (H : ∀ i x, g (Pi.mulSingle i x) = h (Pi.mulSingle i x)) : g = h

Proof state:
case intro.h
I : Type u_4
inst✝³ : DecidableEq I
Z : I → Type u_5
inst✝² : (i : I) → CommMonoid (Z i)
inst✝¹ : Finite I
G : Type u_6
inst✝ : CommMonoid G
g h : ((i : I) → Z i) →* G
H : ∀ (i : I) (x : Z i), g (Pi.mulSingle i x) = h (Pi.mulSingle i x)
val✝ : Fintype I
k : (i : I) → Z i
⊢ g k = h k

Tactic:
rw [← Finset.univ_prod_mulSingle k, map_prod, map_prod]

Result:
case intro.h
I : Type u_4
inst✝³ : DecidableEq I
Z : I → Type u_5
inst✝² : (i : I) → CommMonoid (Z i)
inst✝¹ : Finite I
G : Type u_6
inst✝ : CommMonoid G
g h : ((i : I) → Z i) →* G
H : ∀ (i : I) (x : Z i), g (Pi.mulSingle i x) = h (Pi.mulSingle i x)
val✝ : Fintype I
k : (i : I) → Z i
⊢ ∏ x : I, g (Pi.mulSingle x (k x)) = ∏ x : I, h (Pi.mulSingle x (k x))

Proof state:
I : Type u_4
inst✝³ : DecidableEq I
Z : I → Type u_5
inst✝² : (i : I) → CommMonoid (Z i)
inst✝¹ : Finite I
G : Type u_6
inst✝ : CommMonoid G
g h : ((i : I) → Z i) →* G
H : ∀ (i : I) (x : Z i), g (Pi.mulSingle i x) = h (Pi.mulSingle i x)
⊢ g = h

Tactic:
cases nonempty_fintype I

Result:
case intro
I : Type u_4
inst✝³ : DecidableEq I
Z : I → Type u_5
inst✝² : (i : I) → CommMonoid (Z i)
inst✝¹ : Finite I
G : Type u_6
inst✝ : CommMonoid G
g h : ((i : I) → Z i) →* G
H : ∀ (i : I) (x : Z i), g (Pi.mulSingle i x) = h (Pi.mulSingle i x)
val✝ : Fintype I
⊢ g = h

Proof state:
case intro.h
I : Type u_4
inst✝³ : DecidableEq I
Z : I → Type u_5
inst✝² : (i : I) → CommMonoid (Z i)
inst✝¹ : Finite I
G : Type u_6
inst✝ : CommMonoid G
g h : ((i : I) → Z i) →* G
H : ∀ (i : I) (x : Z i), g (Pi.mulSingle i x) = h (Pi.mulSingle i x)
val✝ : Fintype I
k : (i : I) → Z i
⊢ ∏ x : I, g (Pi.mulSingle x (k x)) = ∏ x : I, h (Pi.mulSingle x (k x))

Tactic:
simp only [H]

Result:
no goals

Proof state:
case intro
I : Type u_4
inst✝³ : DecidableEq I
Z : I → Type u_5
inst✝² : (i : I) → CommMonoid (Z i)
inst✝¹ : Finite I
G : Type u_6
inst✝ : CommMonoid G
g h : ((i : I) → Z i) →* G
H : ∀ (i : I) (x : Z i), g (Pi.mulSingle i x) = h (Pi.mulSingle i x)
val✝ : Fintype I
⊢ g = h

Tactic:
ext k

Result:
case intro.h
I : Type u_4
inst✝³ : DecidableEq I
Z : I → Type u_5
inst✝² : (i : I) → CommMonoid (Z i)
inst✝¹ : Finite I
G : Type u_6
inst✝ : CommMonoid G
g h : ((i : I) → Z i) →* G
H : ∀ (i : I) (x : Z i), g (Pi.mulSingle i x) = h (Pi.mulSingle i x)
val✝ : Fintype I
k : (i : I) → Z i
⊢ g k = h k
-- Mathlib/NumberTheory/LSeries/HurwitzZetaValues.lean
private lemma hurwitzZeta_one_sub_two_mul_nat (hk : k ≠ 0) (hx : x ∈ Icc (0 : ℝ) 1) :
    hurwitzZeta x (1 - 2 * k) =
      -1 / (2 * k) * ((Polynomial.bernoulli (2 * k)).map (algebraMap ℚ ℂ)).eval (x : ℂ)

Proof state:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ hurwitzZeta (↑x) (1 - 2 * ↑k) =
    -1 / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))

Tactic:
suffices hurwitzZetaOdd x (1 - 2 * k) = 0 by
  rw [hurwitzZeta, this, add_zero, hurwitzZetaEven_one_sub_two_mul_nat hk hx]

Result:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ hurwitzZetaOdd (↑x) (1 - 2 * ↑k) = 0

Proof state:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ hurwitzZetaOdd (↑x) (1 - 2 * ↑k) = 0

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hk

Result:
case intro
x : ℝ
hx : x ∈ Icc 0 1
k : ℕ
hk : k.succ ≠ 0
⊢ hurwitzZetaOdd (↑x) (1 - 2 * ↑k.succ) = 0

Proof state:
x : ℝ
hx : x ∈ Icc 0 1
k : ℕ
hk : k.succ ≠ 0
⊢ 1 - 2 * (↑k + 1) = -2 * ↑k - 1

Tactic:
ring

Result:
no goals

Proof state:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : hurwitzZetaOdd (↑x) (1 - 2 * ↑k) = 0
⊢ hurwitzZeta (↑x) (1 - 2 * ↑k) =
    -1 / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))

Tactic:
rw [hurwitzZeta, this, add_zero, hurwitzZetaEven_one_sub_two_mul_nat hk hx]

Result:
no goals

Proof state:
case intro
x : ℝ
hx : x ∈ Icc 0 1
k : ℕ
hk : k.succ ≠ 0
⊢ hurwitzZetaOdd (↑x) (1 - 2 * ↑k.succ) = 0

Tactic:
rw [Nat.cast_succ, show (1 : ℂ) - 2 * (k + 1) = -2 * k - 1 by ring,
  hurwitzZetaOdd_neg_two_mul_nat_sub_one]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem exists_pow_eq_self_of_coprime (h : n.Coprime (orderOf x)) : ∃ m : ℕ, (x ^ n) ^ m = x

Proof state:
case neg
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
⊢ ∃ m, (x ^ n) ^ m = x

Tactic:
by_cases h1 : orderOf x = 1

Result:
case pos
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : orderOf x = 1
⊢ ∃ m, (x ^ n) ^ m = x

case neg
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
⊢ ∃ m, (x ^ n) ^ m = x

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h✝ : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
m : ℕ
h : n * m % orderOf x = 1
⊢ (x ^ n) ^ m = x

Tactic:
rw [← pow_mul, ← pow_mod_orderOf, h, pow_one]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n = 1
h0 : orderOf x = 0
⊢ (x ^ n) ^ 1 = x

Tactic:
rw [h, pow_one, pow_one]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
⊢ ∃ m, (x ^ n) ^ m = x

Tactic:
by_cases h0 : orderOf x = 0

Result:
case pos
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : orderOf x = 0
⊢ ∃ m, (x ^ n) ^ m = x

case neg
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
⊢ ∃ m, (x ^ n) ^ m = x

Proof state:
case neg.intro
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h✝ : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
m : ℕ
h : n * m % orderOf x = 1
⊢ ∃ m, (x ^ n) ^ m = x

Tactic:
exact ⟨m, by rw [← pow_mul, ← pow_mod_orderOf, h, pow_one]⟩

Result:
no goals

Proof state:
case neg
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
⊢ ∃ m, (x ^ n) ^ m = x

Tactic:
obtain ⟨m, h⟩ := exists_mul_emod_eq_one_of_coprime h (one_lt_iff_ne_zero_and_ne_one.mpr ⟨h0, h1⟩)

Result:
case neg.intro
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h✝ : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : ¬orderOf x = 1
m : ℕ
h : n * m % orderOf x = 1
⊢ ∃ m, (x ^ n) ^ m = x

Proof state:
case pos
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : orderOf x = 1
⊢ ∃ m, (x ^ n) ^ m = x

Tactic:
exact ⟨0, by rw [orderOf_eq_one_iff.mp h1, one_pow, one_pow]⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : ¬orderOf x = 0
h1 : orderOf x = 1
⊢ (x ^ n) ^ 0 = x

Tactic:
rw [orderOf_eq_one_iff.mp h1, one_pow, one_pow]

Result:
no goals

Proof state:
case pos
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n = 1
h0 : orderOf x = 0
⊢ ∃ m, (x ^ n) ^ m = x

Tactic:
exact ⟨1, by rw [h, pow_one, pow_one]⟩

Result:
no goals

Proof state:
case pos
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n.Coprime (orderOf x)
h0 : orderOf x = 0
⊢ ∃ m, (x ^ n) ^ m = x

Tactic:
rw [h0, coprime_zero_right] at h

Result:
case pos
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : n = 1
h0 : orderOf x = 0
⊢ ∃ m, (x ^ n) ^ m = x
-- Mathlib/Control/LawfulFix.lean
theorem fix_eq_ωSup_of_ωScottContinuous (hc : ωScottContinuous g) : Part.fix g =
    ωSup (approxChain (⟨g,hc.monotone⟩ : ((a : _) → Part <| β a) →o (a : _) → Part <| β a))

Proof state:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ Part.fix g = ωSup (approxChain { toFun := g, monotone' := ⋯ })

Tactic:
rw [← fix_eq_ωSup]

Result:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ Part.fix g = Part.fix ⇑{ toFun := g, monotone' := ⋯ }

Proof state:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ Part.fix g = Part.fix ⇑{ toFun := g, monotone' := ⋯ }

Tactic:
rfl

Result:
no goals