harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/WittVector/DiscreteValuationRing.lean
theorem exists_eq_pow_p_mul (a : 𝕎 k) (ha : a ≠ 0) :
    ∃ (m : ℕ) (b : 𝕎 k), b.coeff 0 ≠ 0 ∧ a = (p : 𝕎 k) ^ m * b

Proof state:
case intro.intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : ((⇑frobenius)^[m] b).coeff 0 ≠ 0
hcm : a = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)
⊢ ∃ m b, b.coeff 0 ≠ 0 ∧ a = ↑p ^ m * b

Tactic:
rw [WittVector.iterate_frobenius_coeff] at hc

Result:
case intro.intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)
⊢ ∃ m b, b.coeff 0 ≠ 0 ∧ a = ↑p ^ m * b

Proof state:
case intro.intro.intro.intro.refine_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hcm : a = (⇑verschiebung ∘ ⇑frobenius)^[m] b
this : (⇑verschiebung ∘ ⇑frobenius)^[m] b = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)
hc : b.coeff 0 = 0
⊢ b.coeff 0 ^ p ^ m = 0

Tactic:
simp [hc, zero_pow <| pow_ne_zero _ hp.out.ne_zero]

Result:
no goals

Proof state:
case intro.intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)
⊢ ∃ m b, b.coeff 0 ≠ 0 ∧ a = ↑p ^ m * b

Tactic:
have := congr_fun (WittVector.verschiebung_frobenius_comm.comp_iterate m) b

Result:
case intro.intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)
this : (⇑verschiebung ∘ ⇑frobenius)^[m] b = ((⇑verschiebung)^[m] ∘ (⇑frobenius)^[m]) b
⊢ ∃ m b, b.coeff 0 ≠ 0 ∧ a = ↑p ^ m * b

Proof state:
case h.e'_3.h.e'_2.h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (⇑verschiebung ∘ ⇑frobenius)^[m] b
this : (⇑verschiebung ∘ ⇑frobenius)^[m] b = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)
x : 𝕎 k
⊢ ↑p * x = (⇑verschiebung ∘ ⇑frobenius) x

Tactic:
rw [mul_comm, ← WittVector.verschiebung_frobenius x]

Result:
case h.e'_3.h.e'_2.h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (⇑verschiebung ∘ ⇑frobenius)^[m] b
this : (⇑verschiebung ∘ ⇑frobenius)^[m] b = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)
x : 𝕎 k
⊢ verschiebung (frobenius x) = (⇑verschiebung ∘ ⇑frobenius) x
-- Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
theorem norm_eq_one_of_linearly_ordered {K : Type*} [LinearOrderedField K] [Algebra K L]
    (hodd : Odd (n : ℕ)) : norm K ζ = 1

Proof state:
n : ℕ+
L : Type v
inst✝² : CommRing L
ζ : L
hζ : IsPrimitiveRoot ζ ↑n
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : Algebra K L
hodd : Odd ↑n
⊢ (Algebra.norm K) ζ = 1

Tactic:
have hz := congr_arg (norm K) ((IsPrimitiveRoot.iff_def _ n).1 hζ).1

Result:
n : ℕ+
L : Type v
inst✝² : CommRing L
ζ : L
hζ : IsPrimitiveRoot ζ ↑n
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : Algebra K L
hodd : Odd ↑n
hz : (Algebra.norm K) (ζ ^ ↑n) = (Algebra.norm K) 1
⊢ (Algebra.norm K) ζ = 1

Proof state:
n : ℕ+
L : Type v
inst✝² : CommRing L
ζ : L
hζ : IsPrimitiveRoot ζ ↑n
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : Algebra K L
hodd : Odd ↑n
hz : (Algebra.norm K) (ζ ^ ↑n) = (Algebra.norm K) 1
⊢ (Algebra.norm K) ζ = 1

Tactic:
rw [← (algebraMap K L).map_one, Algebra.norm_algebraMap, one_pow, map_pow, ← one_pow ↑n] at hz

Result:
n : ℕ+
L : Type v
inst✝² : CommRing L
ζ : L
hζ : IsPrimitiveRoot ζ ↑n
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : Algebra K L
hodd : Odd ↑n
hz : (Algebra.norm K) ζ ^ ↑n = 1 ^ ↑n
⊢ (Algebra.norm K) ζ = 1

Proof state:
n : ℕ+
L : Type v
inst✝² : CommRing L
ζ : L
hζ : IsPrimitiveRoot ζ ↑n
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : Algebra K L
hodd : Odd ↑n
hz : (Algebra.norm K) ζ ^ ↑n = 1 ^ ↑n
⊢ (Algebra.norm K) ζ = 1

Tactic:
exact StrictMono.injective hodd.strictMono_pow hz

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem lift_type_lt {α : Type u} {β : Type v} {r s} [IsWellOrder α r] [IsWellOrder β s] :
    lift.{max v w} (type r) < lift.{max u w} (type s) ↔ Nonempty (r ≺i s)

Proof state:
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ lift.{max v w, u} (type r) < lift.{max u w, v} (type s) ↔ Nonempty (r ≺i s)

Tactic:
constructor <;> refine fun ⟨f⟩ ↦ ⟨?_⟩

Result:
case mp
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ : lift.{max v w, u} (type r) < lift.{max u w, v} (type s)
f : ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≺i ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r
⊢ r ≺i s

case mpr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ : Nonempty (r ≺i s)
f : r ≺i s
⊢ ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≺i ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r

Proof state:
case mp
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ : lift.{max v w, u} (type r) < lift.{max u w, v} (type s)
f : ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≺i ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r
⊢ r ≺i s

Tactic:
exact (f.relIsoTrans (RelIso.preimage Equiv.ulift r).symm).transInitial
  (RelIso.preimage Equiv.ulift s).toInitialSeg

Result:
no goals

Proof state:
case mpr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝ : Nonempty (r ≺i s)
f : r ≺i s
⊢ ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r ≺i ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r

Tactic:
exact (f.relIsoTrans (RelIso.preimage Equiv.ulift r)).transInitial
  (RelIso.preimage Equiv.ulift s).symm.toInitialSeg

Result:
no goals
-- Mathlib/Topology/Algebra/Module/FiniteDimension.lean
theorem toLinearEquiv_toContinuousLinearEquiv (e : E ≃ₗ[𝕜] F) :
    e.toContinuousLinearEquiv.toLinearEquiv = e

Proof state:
case h
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : AddCommGroup E
inst✝¹² : Module 𝕜 E
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : IsTopologicalAddGroup E
inst✝⁹ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : IsTopologicalAddGroup F
inst✝⁴ : ContinuousSMul 𝕜 F
inst✝³ : CompleteSpace 𝕜
inst✝² : T2Space E
inst✝¹ : T2Space F
inst✝ : FiniteDimensional 𝕜 E
e : E ≃ₗ[𝕜] F
x : E
⊢ e.toContinuousLinearEquiv.toLinearEquiv x = e x

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : AddCommGroup E
inst✝¹² : Module 𝕜 E
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : IsTopologicalAddGroup E
inst✝⁹ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : IsTopologicalAddGroup F
inst✝⁴ : ContinuousSMul 𝕜 F
inst✝³ : CompleteSpace 𝕜
inst✝² : T2Space E
inst✝¹ : T2Space F
inst✝ : FiniteDimensional 𝕜 E
e : E ≃ₗ[𝕜] F
⊢ e.toContinuousLinearEquiv.toLinearEquiv = e

Tactic:
ext x

Result:
case h
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : AddCommGroup E
inst✝¹² : Module 𝕜 E
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : IsTopologicalAddGroup E
inst✝⁹ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : IsTopologicalAddGroup F
inst✝⁴ : ContinuousSMul 𝕜 F
inst✝³ : CompleteSpace 𝕜
inst✝² : T2Space E
inst✝¹ : T2Space F
inst✝ : FiniteDimensional 𝕜 E
e : E ≃ₗ[𝕜] F
x : E
⊢ e.toContinuousLinearEquiv.toLinearEquiv x = e x
-- Mathlib/Computability/TMConfig.lean
theorem stepNormal_then (c) (k k' : Cont) (v) :
    stepNormal c (k.then k') v = (stepNormal c k v).then k'

Proof state:
c : Code
k k' : Cont
v : List ℕ
⊢ stepNormal c (k.then k') v = (stepNormal c k v).then k'

Tactic:
induction c generalizing k v with simp only [Cont.then, stepNormal, *]
| cons c c' ih _ => rw [← ih, Cont.then]
| comp c c' _ ih' => rw [← ih', Cont.then]
| case => cases v.headI <;> simp only [Nat.rec_zero]
| fix c ih => rw [← ih, Cont.then]
| _ => simp only [Cfg.then]

Result:
no goals

Proof state:
case case
k' : Cont
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (k : Cont) (v : List ℕ), stepNormal a✝¹ (k.then k') v = (stepNormal a✝¹ k v).then k'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), stepNormal a✝ (k.then k') v = (stepNormal a✝ k v).then k'
k : Cont
v : List ℕ
⊢ Nat.rec ((stepNormal a✝¹ k v.tail).then k') (fun y x => (stepNormal a✝ k (y :: v.tail)).then k') v.headI =
    (Nat.rec (stepNormal a✝¹ k v.tail) (fun y x => stepNormal a✝ k (y :: v.tail)) v.headI).then k'

Tactic:
cases v.headI <;> simp only [Nat.rec_zero]

Result:
no goals

Proof state:
case comp
k' : Cont
c c' : Code
a_ih✝ : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
ih' : ∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k'
k : Cont
v : List ℕ
⊢ stepNormal c' (Cont.comp c (k.then k')) v = (stepNormal c' (Cont.comp c k) v).then k'

Tactic:
rw [← ih', Cont.then]

Result:
no goals

Proof state:
case cons
k' : Cont
c c' : Code
ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
a_ih✝ : ∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k'
k : Cont
v : List ℕ
⊢ stepNormal c (Cont.cons₁ c' v (k.then k')) v = (stepNormal c (Cont.cons₁ c' v k) v).then k'

Tactic:
rw [← ih, Cont.then]

Result:
no goals

Proof state:
case fix
k' : Cont
c : Code
ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'
k : Cont
v : List ℕ
⊢ stepNormal c (Cont.fix c (k.then k')) v = (stepNormal c (Cont.fix c k) v).then k'

Tactic:
rw [← ih, Cont.then]

Result:
no goals

Proof state:
case tail
k' k : Cont
v : List ℕ
⊢ Cfg.ret (k.then k') v.tail = (Cfg.ret k v.tail).then k'

Tactic:
simp only [Cfg.then]

Result:
no goals
-- Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean
lemma tsum_riemannZetaSummand (hs : 1 < s.re) :
    ∑' (n : ℕ), riemannZetaSummandHom (ne_zero_of_one_lt_re hs) n = riemannZeta s

Proof state:
s : ℂ
hs : 1 < s.re
hsum : Summable fun n => ‖(riemannZetaSummandHom ⋯) n‖
⊢ ∑' (b : ℕ), (riemannZetaSummandHom ⋯) (b + 1) = ∑' (n : ℕ), 1 / (↑n + 1) ^ s

Tactic:
simp only [riemannZetaSummandHom, cpow_neg, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk,
  Nat.cast_add, Nat.cast_one, one_div]

Result:
no goals

Proof state:
s : ℂ
hs : 1 < s.re
⊢ ∑' (n : ℕ), (riemannZetaSummandHom ⋯) n = riemannZeta s

Tactic:
have hsum := summable_riemannZetaSummand hs

Result:
s : ℂ
hs : 1 < s.re
hsum : Summable fun n => ‖(riemannZetaSummandHom ⋯) n‖
⊢ ∑' (n : ℕ), (riemannZetaSummandHom ⋯) n = riemannZeta s

Proof state:
s : ℂ
hs : 1 < s.re
hsum : Summable fun n => ‖(riemannZetaSummandHom ⋯) n‖
⊢ ∑' (n : ℕ), (riemannZetaSummandHom ⋯) n = riemannZeta s

Tactic:
rw [zeta_eq_tsum_one_div_nat_add_one_cpow hs, tsum_eq_zero_add hsum.of_norm, map_zero, zero_add]

Result:
s : ℂ
hs : 1 < s.re
hsum : Summable fun n => ‖(riemannZetaSummandHom ⋯) n‖
⊢ ∑' (b : ℕ), (riemannZetaSummandHom ⋯) (b + 1) = ∑' (n : ℕ), 1 / (↑n + 1) ^ s
-- Mathlib/Topology/Constructions.lean
theorem prod_eq_generateFrom :
    instTopologicalSpaceProd =
      generateFrom { g | ∃ (s : Set X) (t : Set Y), IsOpen s ∧ IsOpen t ∧ g = s ×ˢ t } :=
  le_antisymm (le_generateFrom fun _ ⟨_, _, hs, ht, g_eq⟩ => g_eq.symm ▸ hs.prod ht)
    (le_inf
      (forall_mem_image.2 fun t ht =>
        GenerateOpen.basic _ ⟨t, univ, by simpa [Set.prod_eq] using ht⟩)
      (forall_mem_image.2 fun t ht =>
        GenerateOpen.basic _ ⟨univ, t, by simpa [Set.prod_eq] using ht⟩))

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
t : Set Y
ht : t ∈ inst✝.1
⊢ IsOpen univ ∧ IsOpen t ∧ Prod.snd ⁻¹' t = univ ×ˢ t

Tactic:
simpa [Set.prod_eq] using ht

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
t : Set X
ht : t ∈ inst✝¹.1
⊢ IsOpen t ∧ IsOpen univ ∧ Prod.fst ⁻¹' t = t ×ˢ univ

Tactic:
simpa [Set.prod_eq] using ht

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Constructions.lean
theorem filter_apply_eq_zero_iff (a : α) : (p.filter s h) a = 0 ↔ a ∉ s ∨ a ∉ p.support

Proof state:
α : Type u_1
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
a : α
⊢ (p.filter s h) a = 0 ↔ a ∉ s ∨ a ∉ p.support

Tactic:
rw [apply_eq_zero_iff, support_filter, Set.mem_inter_iff, not_and_or]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_erase_self [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {k : α} :
    get! (m.erase k) k = default

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.WF
k : α
⊢ get! (m.erase k) k = default

Tactic:
simp_to_raw using Raw₀.Const.get!_erase_self

Result:
no goals
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean
@[simp]
lemma symm_add : φ.symm.add = φ.add

Proof state:
case e_f
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
W : MorphismProperty C
X Y : C
φ : W.LeftFraction₂ X Y
⊢ φ.f' + φ.f = φ.f + φ.f'

Tactic:
apply add_comm

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
W : MorphismProperty C
X Y : C
φ : W.LeftFraction₂ X Y
⊢ φ.symm.add = φ.add

Tactic:
dsimp [add, symm]

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
W : MorphismProperty C
X Y : C
φ : W.LeftFraction₂ X Y
⊢ LeftFraction.mk (φ.f' + φ.f) φ.s ⋯ = LeftFraction.mk (φ.f + φ.f') φ.s ⋯

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
W : MorphismProperty C
X Y : C
φ : W.LeftFraction₂ X Y
⊢ LeftFraction.mk (φ.f' + φ.f) φ.s ⋯ = LeftFraction.mk (φ.f + φ.f') φ.s ⋯

Tactic:
congr 1

Result:
case e_f
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
W : MorphismProperty C
X Y : C
φ : W.LeftFraction₂ X Y
⊢ φ.f' + φ.f = φ.f + φ.f'
-- Mathlib/.lake/packages/batteries/Batteries/Data/BinomialHeap/Basic.lean
theorem HeapNode.rankTR_eq : @rankTR = @rank

Proof state:
case h.h
α : Type u_1
s : HeapNode α
⊢ Batteries.BinomialHeap.Imp.HeapNode.rankTR s = s.rank

Tactic:
exact go s 0

Result:
no goals

Proof state:
α : Type ?u.2427
a✝ : α
child✝ sibling✝ : HeapNode α
x✝ : Nat
⊢ Batteries.BinomialHeap.Imp.HeapNode.rankTR.go (node a✝ child✝ sibling✝) x✝ = (node a✝ child✝ sibling✝).rank + x✝

Tactic:
simp_arith only [rankTR.go, go, rank]

Result:
no goals

Proof state:
⊢ @Batteries.BinomialHeap.Imp.HeapNode.rankTR = @rank

Tactic:
funext α s

Result:
case h.h
α : Type u_1
s : HeapNode α
⊢ Batteries.BinomialHeap.Imp.HeapNode.rankTR s = s.rank
-- Mathlib/Order/Filter/NAry.lean
theorem map_prod_eq_map₂ (m : α → β → γ) (f : Filter α) (g : Filter β) :
    Filter.map (fun p : α × β => m p.1 p.2) (f ×ˢ g) = map₂ m f g

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
⊢ map (fun p => m p.1 p.2) (f ×ˢ g) = map₂ m f g

Tactic:
rw [map₂, copy_eq, uncurry_def]

Result:
no goals
-- Mathlib/RingTheory/WittVector/StructurePolynomial.lean
theorem eq_wittStructureInt (Φ : MvPolynomial idx ℤ) (φ : ℕ → MvPolynomial (idx × ℕ) ℤ)
    (h : ∀ n, bind₁ φ (wittPolynomial p ℤ n) = bind₁ (fun i => rename (Prod.mk i) (W_ ℤ n)) Φ) :
    φ = wittStructureInt p Φ

Proof state:
case h.a
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), (bind₁ φ) (W_ ℤ n) = (bind₁ fun i => (rename (Prod.mk i)) (W_ ℤ n)) Φ
k : ℕ
⊢ (map (Int.castRingHom ℚ)) (φ k) = (map (Int.castRingHom ℚ)) (wittStructureInt p Φ k)

Tactic:
rw [map_wittStructureInt]

Result:
case h.a
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), (bind₁ φ) (W_ ℤ n) = (bind₁ fun i => (rename (Prod.mk i)) (W_ ℤ n)) Φ
k : ℕ
⊢ (map (Int.castRingHom ℚ)) (φ k) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) k
-- Mathlib/NumberTheory/LSeries/PrimesInAP.lean
/-- The L-series of the von Mangoldt function restricted to the residue class `a` mod `q`
with `a` invertible in `ZMod q` is a linear combination of logarithmic derivatives of
L-functions of the Dirichlet characters mod `q` (on `re s > 1`). -/
lemma LSeries_residueClass_eq (ha : IsUnit a) {s : ℂ} (hs : 1 < s.re) :
    LSeries ↗(residueClass a) s =
      -(q.totient : ℂ)⁻¹ * ∑ χ : DirichletCharacter ℂ q, χ a⁻¹ *
        (deriv (LFunction χ) s / LFunction χ s)

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
n : ℕ
x✝ : n ≠ 0
⊢ (↑q.totient • fun n => ↑(residueClass a n)) n =
    (∑ i : DirichletCharacter ℂ q, i a⁻¹ • ((fun n => i ↑n) * fun n => ↑(Λ n))) n

Tactic:
simp only [Pi.smul_apply, residueClass_apply ha, smul_eq_mul, ← mul_assoc,
  mul_inv_cancel_of_invertible, one_mul, Finset.sum_apply, Pi.mul_apply]

Result:
no goals

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
⊢ L (fun n => ↑(residueClass a n)) s =
    (↑q.totient)⁻¹ * ∑ x : DirichletCharacter ℂ q, x a⁻¹ * L ((fun x_1 => x ↑x_1) * fun n => ↑(Λ n)) s

Tactic:
rw [eq_inv_mul_iff_mul_eq₀ <| mod_cast (Nat.totient_pos.mpr q.pos_of_neZero).ne']

Result:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
⊢ ↑q.totient * L (fun n => ↑(residueClass a n)) s =
    ∑ x : DirichletCharacter ℂ q, x a⁻¹ * L ((fun x_1 => x ↑x_1) * fun n => ↑(Λ n)) s

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
⊢ L (fun n => ↑(residueClass a n)) s =
    -(↑q.totient)⁻¹ * ∑ χ : DirichletCharacter ℂ q, χ a⁻¹ * (deriv (LFunction χ) s / LFunction χ s)

Tactic:
simp only [deriv_LFunction_eq_deriv_LSeries _ hs, LFunction_eq_LSeries _ hs, neg_mul, ← mul_neg,
  ← Finset.sum_neg_distrib, ← neg_div, ← LSeries_twist_vonMangoldt_eq _ hs]

Result:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
⊢ L (fun n => ↑(residueClass a n)) s =
    (↑q.totient)⁻¹ * ∑ x : DirichletCharacter ℂ q, x a⁻¹ * L ((fun x_1 => x ↑x_1) * fun n => ↑(Λ n)) s

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
⊢ ↑q.totient * L (fun n => ↑(residueClass a n)) s =
    ∑ x : DirichletCharacter ℂ q, x a⁻¹ * L ((fun x_1 => x ↑x_1) * fun n => ↑(Λ n)) s

Tactic:
simp_rw [← LSeries_smul,
  ← LSeries_sum <| fun χ _ ↦ (LSeriesSummable_twist_vonMangoldt χ hs).smul _]

Result:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
⊢ L (↑q.totient • fun n => ↑(residueClass a n)) s =
    L (∑ i : DirichletCharacter ℂ q, i a⁻¹ • ((fun n => i ↑n) * fun n => ↑(Λ n))) s

Proof state:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
⊢ L (↑q.totient • fun n => ↑(residueClass a n)) s =
    L (∑ i : DirichletCharacter ℂ q, i a⁻¹ • ((fun n => i ↑n) * fun n => ↑(Λ n))) s

Tactic:
refine LSeries_congr s fun {n} _ ↦ ?_

Result:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
n : ℕ
x✝ : n ≠ 0
⊢ (↑q.totient • fun n => ↑(residueClass a n)) n =
    (∑ i : DirichletCharacter ℂ q, i a⁻¹ • ((fun n => i ↑n) * fun n => ↑(Λ n))) n
-- Mathlib/AlgebraicGeometry/Scheme.lean
@[reassoc (attr := simp)]
lemma map_appLE (e : V ≤ f ⁻¹ᵁ U) (i : op U' ⟶ op U) :
    Y.presheaf.map i ≫ f.appLE U V e =
      f.appLE U' V (e.trans ((Opens.map f.base).map i.unop).le)

Proof state:
X Y : Scheme
f : X.Hom Y
U U' : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : op U' ⟶ op U
⊢ Y.presheaf.map i ≫ f.appLE U V e = f.appLE U' V ⋯

Tactic:
rw [Hom.appLE, f.naturality_assoc, ← Functor.map_comp]

Result:
X Y : Scheme
f : X.Hom Y
U U' : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : op U' ⟶ op U
⊢ f.app U' ≫ X.presheaf.map (((Opens.map f.base).map i.unop).op ≫ (homOfLE e).op) = f.appLE U' V ⋯

Proof state:
X Y : Scheme
f : X.Hom Y
U U' : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : op U' ⟶ op U
⊢ f.app U' ≫ X.presheaf.map (((Opens.map f.base).map i.unop).op ≫ (homOfLE e).op) = f.appLE U' V ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma Indep.closure_inter_eq_inter_closure (h : M.Indep (I ∪ J)) :
    M.closure (I ∩ J) = M.closure I ∩ M.closure J

Proof state:
α : Type u_2
M : Matroid α
I J : Set α
h : M.Indep (I ∪ J)
⊢ ⋂ i, M.closure (bif i then I else J) = ⋂ b, bif b then M.closure I else M.closure J

Tactic:
exact iInter_congr (by simp)

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
I J : Set α
h : M.Indep (I ∪ J)
⊢ ∀ (i : Bool), M.closure (bif i then I else J) = bif i then M.closure I else M.closure J

Tactic:
simp

Result:
no goals

Proof state:
case h
α : Type u_2
M : Matroid α
I J : Set α
h : M.Indep (I ∪ J)
⊢ M.Indep (⋃ i, bif i then I else J)

Tactic:
rwa [← union_eq_iUnion]

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
I J : Set α
h : M.Indep (I ∪ J)
⊢ M.closure (I ∩ J) = M.closure I ∩ M.closure J

Tactic:
rw [inter_eq_iInter, closure_iInter_eq_iInter_closure_of_iUnion_indep, inter_eq_iInter]

Result:
α : Type u_2
M : Matroid α
I J : Set α
h : M.Indep (I ∪ J)
⊢ ⋂ i, M.closure (bif i then I else J) = ⋂ b, bif b then M.closure I else M.closure J

case h
α : Type u_2
M : Matroid α
I J : Set α
h : M.Indep (I ∪ J)
⊢ M.Indep (⋃ i, bif i then I else J)
-- Mathlib/Data/Rat/Cast/Defs.lean
theorem ext_rat' (h : ∀ m : ℤ, f m = g m) : f = g :=
  (DFunLike.ext f g) fun r => by
    rw [← r.num_div_den, div_eq_mul_inv, map_mul, map_mul, h, ← Int.cast_natCast,
      eq_on_inv₀ f g]
    apply h

Proof state:
F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ M₀
inst✝ : MonoidWithZeroHomClass F ℚ M₀
f g : F
h : ∀ (m : ℤ), f ↑m = g ↑m
r : ℚ
⊢ f r = g r

Tactic:
rw [← r.num_div_den, div_eq_mul_inv, map_mul, map_mul, h, ← Int.cast_natCast,
  eq_on_inv₀ f g]

Result:
F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ M₀
inst✝ : MonoidWithZeroHomClass F ℚ M₀
f g : F
h : ∀ (m : ℤ), f ↑m = g ↑m
r : ℚ
⊢ f ↑↑r.den = g ↑↑r.den

Proof state:
F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ M₀
inst✝ : MonoidWithZeroHomClass F ℚ M₀
f g : F
h : ∀ (m : ℤ), f ↑m = g ↑m
r : ℚ
⊢ f ↑↑r.den = g ↑↑r.den

Tactic:
apply h

Result:
no goals