harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Functor/Currying.lean
lemma uncurry_obj_curry_obj_flip_flip' (F₁ : B ⥤ C) (F₂ : D ⥤ E) (G : C × E ⥤ H) :
    uncurry.obj (F₁ ⋙ (F₂ ⋙ (curry.obj G).flip).flip) = (F₁.prod F₂) ⋙ G :=
  Functor.ext (by simp) (fun ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ ⟨f₁, f₂⟩ => by
    dsimp
    simp only [Category.id_comp, Category.comp_id, ← G.map_comp, prod_comp])

Proof state:
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F₁ : B ⥤ C
F₂ : D ⥤ E
G : C × E ⥤ H
x✝² x✝¹ : B × D
x₁ : B
x₂ : D
y₁ : B
y₂ : D
x✝ : (x₁, x₂) ⟶ (y₁, y₂)
f₁ : (x₁, x₂).1 ⟶ (y₁, y₂).1
f₂ : (x₁, x₂).2 ⟶ (y₁, y₂).2
⊢ (uncurry.obj (F₁ ⋙ (F₂ ⋙ (curry.obj G).flip).flip)).map (f₁, f₂) =
    eqToHom ⋯ ≫ (F₁.prod F₂ ⋙ G).map (f₁, f₂) ≫ eqToHom ⋯

Tactic:
dsimp

Result:
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F₁ : B ⥤ C
F₂ : D ⥤ E
G : C × E ⥤ H
x✝² x✝¹ : B × D
x₁ : B
x₂ : D
y₁ : B
y₂ : D
x✝ : (x₁, x₂) ⟶ (y₁, y₂)
f₁ : (x₁, x₂).1 ⟶ (y₁, y₂).1
f₂ : (x₁, x₂).2 ⟶ (y₁, y₂).2
⊢ G.map (F₁.map f₁, 𝟙 (F₂.obj x₂)) ≫ G.map (𝟙 (F₁.obj y₁), F₂.map f₂) =
    𝟙 (G.obj (F₁.obj x₁, F₂.obj x₂)) ≫ G.map (F₁.map f₁, F₂.map f₂) ≫ 𝟙 (G.obj (F₁.obj y₁, F₂.obj y₂))

Proof state:
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F₁ : B ⥤ C
F₂ : D ⥤ E
G : C × E ⥤ H
x✝² x✝¹ : B × D
x₁ : B
x₂ : D
y₁ : B
y₂ : D
x✝ : (x₁, x₂) ⟶ (y₁, y₂)
f₁ : (x₁, x₂).1 ⟶ (y₁, y₂).1
f₂ : (x₁, x₂).2 ⟶ (y₁, y₂).2
⊢ G.map (F₁.map f₁, 𝟙 (F₂.obj x₂)) ≫ G.map (𝟙 (F₁.obj y₁), F₂.map f₂) =
    𝟙 (G.obj (F₁.obj x₁, F₂.obj x₂)) ≫ G.map (F₁.map f₁, F₂.map f₂) ≫ 𝟙 (G.obj (F₁.obj y₁, F₂.obj y₂))

Tactic:
simp only [Category.id_comp, Category.comp_id, ← G.map_comp, prod_comp]

Result:
no goals

Proof state:
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F₁ : B ⥤ C
F₂ : D ⥤ E
G : C × E ⥤ H
⊢ ∀ (X : B × D), (uncurry.obj (F₁ ⋙ (F₂ ⋙ (curry.obj G).flip).flip)).obj X = (F₁.prod F₂ ⋙ G).obj X

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sinh_three_mul : sinh (3 * x) = 4 * sinh x ^ 3 + 3 * sinh x

Proof state:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ sinh (3 * x) = 4 * sinh x ^ 3 + 3 * sinh x

Tactic:
rw [← h1, sinh_add x (2 * x)]

Result:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ sinh x * cosh (2 * x) + cosh x * sinh (2 * x) = 4 * sinh x ^ 3 + 3 * sinh x

Proof state:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ sinh x * (cosh x ^ 2 + sinh x ^ 2) + cosh x * (2 * sinh x * cosh x) = 4 * sinh x ^ 3 + 3 * sinh x

Tactic:
have h2 : cosh x * (2 * sinh x * cosh x) = 2 * sinh x * cosh x ^ 2 := by ring

Result:
x : ℂ
h1 : x + 2 * x = 3 * x
h2 : cosh x * (2 * sinh x * cosh x) = 2 * sinh x * cosh x ^ 2
⊢ sinh x * (cosh x ^ 2 + sinh x ^ 2) + cosh x * (2 * sinh x * cosh x) = 4 * sinh x ^ 3 + 3 * sinh x

Proof state:
x : ℂ
⊢ sinh (3 * x) = 4 * sinh x ^ 3 + 3 * sinh x

Tactic:
have h1 : x + 2 * x = 3 * x := by ring

Result:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ sinh (3 * x) = 4 * sinh x ^ 3 + 3 * sinh x

Proof state:
x : ℂ
h1 : x + 2 * x = 3 * x
h2 : cosh x * (2 * sinh x * cosh x) = 2 * sinh x * cosh x ^ 2
⊢ sinh x * (cosh x ^ 2 + sinh x ^ 2) + cosh x * (2 * sinh x * cosh x) = 4 * sinh x ^ 3 + 3 * sinh x

Tactic:
rw [h2, cosh_sq]

Result:
x : ℂ
h1 : x + 2 * x = 3 * x
h2 : cosh x * (2 * sinh x * cosh x) = 2 * sinh x * cosh x ^ 2
⊢ sinh x * (sinh x ^ 2 + 1 + sinh x ^ 2) + 2 * sinh x * (sinh x ^ 2 + 1) = 4 * sinh x ^ 3 + 3 * sinh x

Proof state:
x : ℂ
h1 : x + 2 * x = 3 * x
h2 : cosh x * (2 * sinh x * cosh x) = 2 * sinh x * cosh x ^ 2
⊢ sinh x * (sinh x ^ 2 + 1 + sinh x ^ 2) + 2 * sinh x * (sinh x ^ 2 + 1) = 4 * sinh x ^ 3 + 3 * sinh x

Tactic:
ring

Result:
no goals

Proof state:
x : ℂ
⊢ x + 2 * x = 3 * x

Tactic:
ring

Result:
no goals

Proof state:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ sinh x * cosh (2 * x) + cosh x * sinh (2 * x) = 4 * sinh x ^ 3 + 3 * sinh x

Tactic:
simp only [cosh_two_mul, sinh_two_mul]

Result:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ sinh x * (cosh x ^ 2 + sinh x ^ 2) + cosh x * (2 * sinh x * cosh x) = 4 * sinh x ^ 3 + 3 * sinh x

Proof state:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ cosh x * (2 * sinh x * cosh x) = 2 * sinh x * cosh x ^ 2

Tactic:
ring

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Checker.lean
theorem check_sound (lratProof : Array IntAction) (cnf : CNF Nat) :
    check lratProof cnf → cnf.Unsat

Proof state:
case intro.intro.h_2
lratProof : Array IntAction
cnf : CNF Nat
h1 :
  lratChecker (CNF.convertLRAT cnf)
      (List.filterMap
        (fun actOpt =>
          match actOpt with
          | none => none
          | some (Action.addEmpty id rupHints) => some (Action.addEmpty id rupHints)
          | some (Action.addRup id c rupHints) => some (Action.addRup id c rupHints)
          | some (Action.del ids) => some (Action.del ids)
          | some (Action.addRat id c pivot rupHints ratHints) =>
            if pivot ∈ Clause.toList c then some (Action.addRat id c pivot rupHints ratHints) else none)
        (List.map (intActionToDefaultClauseAction (cnf.numLiterals + 1)) lratProof.toList)) =
    Result.success
action : Action (DefaultClause (cnf.numLiterals + 1)) (PosFin (cnf.numLiterals + 1))
WellFormedActions : IntAction
left✝ : WellFormedActions ∈ lratProof.toList
actOpt✝ : Option (DefaultClauseAction (cnf.numLiterals + 1))
id✝ : Nat
rupHints✝ : Array Nat
heq✝ : intActionToDefaultClauseAction (cnf.numLiterals + 1) WellFormedActions = some (Action.addEmpty id✝ rupHints✝)
h2 : some (Action.addEmpty id✝ rupHints✝) = some action
⊢ WellFormedAction action

Tactic:
simp only [Option.some.injEq] at h2

Result:
case intro.intro.h_2
lratProof : Array IntAction
cnf : CNF Nat
h1 :
  lratChecker (CNF.convertLRAT cnf)
      (List.filterMap
        (fun actOpt =>
          match actOpt with
          | none => none
          | some (Action.addEmpty id rupHints) => some (Action.addEmpty id rupHints)
          | some (Action.addRup id c rupHints) => some (Action.addRup id c rupHints)
          | some (Action.del ids) => some (Action.del ids)
          | some (Action.addRat id c pivot rupHints ratHints) =>
            if pivot ∈ Clause.toList c then some (Action.addRat id c pivot rupHints ratHints) else none)
        (List.map (intActionToDefaultClauseAction (cnf.numLiterals + 1)) lratProof.toList)) =
    Result.success
action : Action (DefaultClause (cnf.numLiterals + 1)) (PosFin (cnf.numLiterals + 1))
WellFormedActions : IntAction
left✝ : WellFormedActions ∈ lratProof.toList
actOpt✝ : Option (DefaultClauseAction (cnf.numLiterals + 1))
id✝ : Nat
rupHints✝ : Array Nat
heq✝ : intActionToDefaultClauseAction (cnf.numLiterals + 1) WellFormedActions = some (Action.addEmpty id✝ rupHints✝)
h2 : Action.addEmpty id✝ rupHints✝ = action
⊢ WellFormedAction action
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Checker.lean
theorem check_sound (lratProof : Array IntAction) (cnf : CNF Nat) :
    check lratProof cnf → cnf.Unsat

Proof state:
case intro.intro.h_5
lratProof : Array IntAction
cnf : CNF Nat
h1 :
  lratChecker (CNF.convertLRAT cnf)
      (List.filterMap
        (fun actOpt =>
          match actOpt with
          | none => none
          | some (Action.addEmpty id rupHints) => some (Action.addEmpty id rupHints)
          | some (Action.addRup id c rupHints) => some (Action.addRup id c rupHints)
          | some (Action.del ids) => some (Action.del ids)
          | some (Action.addRat id c pivot rupHints ratHints) =>
            if pivot ∈ Clause.toList c then some (Action.addRat id c pivot rupHints ratHints) else none)
        (List.map (intActionToDefaultClauseAction (cnf.numLiterals + 1)) lratProof.toList)) =
    Result.success
action : Action (DefaultClause (cnf.numLiterals + 1)) (PosFin (cnf.numLiterals + 1))
WellFormedActions : IntAction
left✝ : WellFormedActions ∈ lratProof.toList
actOpt✝ : Option (DefaultClauseAction (cnf.numLiterals + 1))
id✝ : Nat
c✝ : DefaultClause (cnf.numLiterals + 1)
pivot✝ : Literal (PosFin (cnf.numLiterals + 1))
rupHints✝ : Array Nat
ratHints✝ : Array (Nat × Array Nat)
heq✝ :
  intActionToDefaultClauseAction (cnf.numLiterals + 1) WellFormedActions =
    some (Action.addRat id✝ c✝ pivot✝ rupHints✝ ratHints✝)
h2 : (if pivot✝ ∈ Clause.toList c✝ then some (Action.addRat id✝ c✝ pivot✝ rupHints✝ ratHints✝) else none) = some action
⊢ WellFormedAction action

Tactic:
. simp only [Option.ite_none_right_eq_some, Option.some.injEq] at h2
  rcases h2 with ⟨hleft, hright⟩
  simp [WellFormedAction, hleft, ← hright, Clause.limplies_iff_mem]

Result:
no goals
-- Mathlib/Data/Multiset/Count.lean
theorem coe_count (a : α) (l : List α) : count a (ofList l) = l.count a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ List.countP (fun b => decide (b = a)) l = List.countP (fun x => x == a) l

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Addition.lean
@[simp]
protected lemma map_sub [AddGroup S] (f : R →+ S) {x y : HahnSeries Γ R} :
    ((x - y).map f : HahnSeries Γ S) = x.map f - y.map f

Proof state:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : AddGroup S
f : R →+ S
x y : HahnSeries Γ R
⊢ (x - y).map f = x.map f - y.map f

Tactic:
ext

Result:
case coeff.h
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : AddGroup S
f : R →+ S
x y : HahnSeries Γ R
x✝ : Γ
⊢ ((x - y).map f).coeff x✝ = (x.map f - y.map f).coeff x✝

Proof state:
case coeff.h
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : AddGroup R
inst✝ : AddGroup S
f : R →+ S
x y : HahnSeries Γ R
x✝ : Γ
⊢ ((x - y).map f).coeff x✝ = (x.map f - y.map f).coeff x✝

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/ZGroup.lean
theorem exponent_eq_card [Finite G] [IsZGroup G] : Monoid.exponent G = Nat.card G

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
p : ℕ
hp : Nat.Prime p
⊢ (Nat.card G).factorization p ≤ (Monoid.exponent G).factorization p

Tactic:
have := Fact.mk hp

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
⊢ (Nat.card G).factorization p ≤ (Monoid.exponent G).factorization p

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
⊢ Nat.card G ∣ Monoid.exponent G

Tactic:
rw [← Nat.factorization_prime_le_iff_dvd Nat.card_pos.ne' Monoid.exponent_ne_zero_of_finite]

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
⊢ ∀ (p : ℕ), Nat.Prime p → (Nat.card G).factorization p ≤ (Monoid.exponent G).factorization p

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
⊢ ∀ (p : ℕ), Nat.Prime p → (Nat.card G).factorization p ≤ (Monoid.exponent G).factorization p

Tactic:
intro p hp

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
p : ℕ
hp : Nat.Prime p
⊢ (Nat.card G).factorization p ≤ (Monoid.exponent G).factorization p

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
⊢ Monoid.exponent G = Nat.card G

Tactic:
refine dvd_antisymm Group.exponent_dvd_nat_card ?_

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
⊢ Nat.card G ∣ Monoid.exponent G

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
⊢ (Nat.card G).factorization p ≤ (Monoid.exponent G).factorization p

Tactic:
let P : Sylow p G := default

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
P : Sylow p G := default
⊢ (Nat.card G).factorization p ≤ (Monoid.exponent G).factorization p

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
P : Sylow p G := default
⊢ Monoid.exponent ↥↑P ∣ Monoid.exponent G

Tactic:
exact Monoid.exponent_dvd_of_monoidHom P.1.subtype P.1.subtype_injective

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
P : Sylow p G := default
⊢ (Nat.card G).factorization p ≤ (Monoid.exponent G).factorization p

Tactic:
rw [← hp.pow_dvd_iff_le_factorization Monoid.exponent_ne_zero_of_finite,
    ← P.card_eq_multiplicity, ← (isZGroup p hp P).exponent_eq_card]

Result:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
P : Sylow p G := default
⊢ Monoid.exponent ↥↑P ∣ Monoid.exponent G
-- Mathlib/Tactic/Ring/Basic.lean
theorem add_pf_add_overlap
    (_ : a₁ + b₁ = c₁) (_ : a₂ + b₂ = c₂) : (a₁ + a₂ : R) + (b₁ + b₂) = c₁ + c₂

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a₁ a₂ b₁ b₂ : R
⊢ a₁ + a₂ + (b₁ + b₂) = a₁ + b₁ + (a₂ + b₂)

Tactic:
simp [add_assoc, add_left_comm]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a₁ a₂ b₁ b₂ c₁ c₂ : R
x✝¹ : a₁ + b₁ = c₁
x✝ : a₂ + b₂ = c₂
⊢ a₁ + a₂ + (b₁ + b₂) = c₁ + c₂

Tactic:
subst_vars

Result:
R : Type u_1
inst✝ : CommSemiring R
a₁ a₂ b₁ b₂ : R
⊢ a₁ + a₂ + (b₁ + b₂) = a₁ + b₁ + (a₂ + b₂)
-- Mathlib/RingTheory/Polynomial/Opposites.lean
theorem opRingEquiv_op_monomial (n : ℕ) (r : R) :
    opRingEquiv R (op (monomial n r : R[X])) = monomial n (op r)

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
r : R
⊢ (opRingEquiv R) (op ((monomial n) r)) = (monomial n) (op r)

Tactic:
simp only [opRingEquiv, RingEquiv.coe_trans, Function.comp_apply,
  AddMonoidAlgebra.opRingEquiv_apply, RingEquiv.op_apply_apply, toFinsuppIso_apply, unop_op,
  toFinsupp_monomial, Finsupp.mapRange_single, toFinsuppIso_symm_apply, ofFinsupp_single]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm_smul_measure_of_ne_zero_of_ne_top {p : ℝ≥0∞} (hp_ne_zero : p ≠ 0)
    (hp_ne_top : p ≠ ∞) {f : α → ε} (c : ℝ≥0∞) :
    eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α → ε
c : ℝ≥0∞
⊢ c ^ (1 / p.toReal) * eLpNorm' f p.toReal μ = c ^ (1 / p).toReal • eLpNorm' f p.toReal μ

Tactic:
congr

Result:
case e_a.e_a
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α → ε
c : ℝ≥0∞
⊢ 1 / p.toReal = (1 / p).toReal

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α → ε
c : ℝ≥0∞
⊢ eLpNorm' f p.toReal (c • μ) = c ^ (1 / p).toReal • eLpNorm' f p.toReal μ

Tactic:
rw [eLpNorm'_smul_measure ENNReal.toReal_nonneg]

Result:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α → ε
c : ℝ≥0∞
⊢ c ^ (1 / p.toReal) * eLpNorm' f p.toReal μ = c ^ (1 / p).toReal • eLpNorm' f p.toReal μ

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α → ε
c : ℝ≥0∞
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

Tactic:
simp_rw [eLpNorm_eq_eLpNorm' hp_ne_zero hp_ne_top]

Result:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α → ε
c : ℝ≥0∞
⊢ eLpNorm' f p.toReal (c • μ) = c ^ (1 / p).toReal • eLpNorm' f p.toReal μ

Proof state:
case e_a.e_a
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α → ε
c : ℝ≥0∞
⊢ 1 / p.toReal = (1 / p).toReal

Tactic:
simp_rw [one_div]

Result:
case e_a.e_a
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α → ε
c : ℝ≥0∞
⊢ p.toReal⁻¹ = p⁻¹.toReal

Proof state:
case e_a.e_a
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α → ε
c : ℝ≥0∞
⊢ p.toReal⁻¹ = p⁻¹.toReal

Tactic:
rw [ENNReal.toReal_inv]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean
lemma accumulate_rec {i n m : ℕ} (hin : i < n) (him : i + 1 < m) (t : Fin n → ℕ) :
    accumulate n m t ⟨i, Nat.lt_of_succ_lt him⟩ = t ⟨i, hin⟩ + accumulate n m t ⟨i + 1, him⟩

Proof state:
case convert_7
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
⊢ ⟨i, hin⟩ ∈ filter (fun i_1 => i ≤ ↑i_1) univ

Tactic:
exact mem_filter.2 ⟨mem_univ _, le_rfl⟩

Result:
no goals

Proof state:
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
⊢ (accumulate n m) t ⟨i, ⋯⟩ = t ⟨i, hin⟩ + (accumulate n m) t ⟨i + 1, him⟩

Tactic:
simp_rw [accumulate_apply]

Result:
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
⊢ ∑ i ∈ filter (fun i_1 => i ≤ ↑i_1) univ, t i = t ⟨i, hin⟩ + ∑ i ∈ filter (fun i_1 => i + 1 ≤ ↑i_1) univ, t i

Proof state:
case h.e'_3.h.e'_6.h.h
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
a✝ : Fin n
⊢ i ≤ ↑a✝ ∧ i ≠ ↑a✝ ↔ a✝ ≠ ⟨i, hin⟩ ∧ i ≤ ↑a✝

Tactic:
rw [and_comm, ne_comm, ← Fin.val_ne_iff]

Result:
no goals

Proof state:
case h.e'_3.h.e'_6.h
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
⊢ filter (fun i_1 => i + 1 ≤ ↑i_1) univ = (filter (fun i_1 => i ≤ ↑i_1) univ).erase ⟨i, hin⟩

Tactic:
ext

Result:
case h.e'_3.h.e'_6.h.h
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
a✝ : Fin n
⊢ a✝ ∈ filter (fun i_1 => i + 1 ≤ ↑i_1) univ ↔ a✝ ∈ (filter (fun i_1 => i ≤ ↑i_1) univ).erase ⟨i, hin⟩

Proof state:
case h.e'_3.h.e'_6.h.h
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
a✝ : Fin n
⊢ a✝ ∈ filter (fun i_1 => i + 1 ≤ ↑i_1) univ ↔ a✝ ∈ (filter (fun i_1 => i ≤ ↑i_1) univ).erase ⟨i, hin⟩

Tactic:
rw [mem_erase]

Result:
case h.e'_3.h.e'_6.h.h
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
a✝ : Fin n
⊢ a✝ ∈ filter (fun i_1 => i + 1 ≤ ↑i_1) univ ↔ a✝ ≠ ⟨i, hin⟩ ∧ a✝ ∈ filter (fun i_1 => i ≤ ↑i_1) univ

Proof state:
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
⊢ ∑ i ∈ filter (fun i_1 => i ≤ ↑i_1) univ, t i = t ⟨i, hin⟩ + ∑ i ∈ filter (fun i_1 => i + 1 ≤ ↑i_1) univ, t i

Tactic:
convert (add_sum_erase _ _ _).symm

Result:
case h.e'_3.h.e'_6.h
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
⊢ filter (fun i_1 => i + 1 ≤ ↑i_1) univ = (filter (fun i_1 => i ≤ ↑i_1) univ).erase ⟨i, hin⟩

case convert_3
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
⊢ DecidableEq (Fin n)

case convert_7
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
⊢ ⟨i, hin⟩ ∈ filter (fun i_1 => i ≤ ↑i_1) univ

Proof state:
case h.e'_3.h.e'_6.h.h
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
a✝ : Fin n
⊢ a✝ ∈ filter (fun i_1 => i + 1 ≤ ↑i_1) univ ↔ a✝ ≠ ⟨i, hin⟩ ∧ a✝ ∈ filter (fun i_1 => i ≤ ↑i_1) univ

Tactic:
simp_rw [mem_filter, mem_univ, true_and, i.succ_le_iff, lt_iff_le_and_ne]

Result:
case h.e'_3.h.e'_6.h.h
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
a✝ : Fin n
⊢ i ≤ ↑a✝ ∧ i ≠ ↑a✝ ↔ a✝ ≠ ⟨i, hin⟩ ∧ i ≤ ↑a✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem bmod_mul_bmod : Int.bmod (Int.bmod x n * y) n = Int.bmod (x * y) n

Proof state:
x : Int
n : Nat
y : Int
p : ¬x % ↑n < (↑n + 1) / 2
⊢ ((x % ↑n - ↑n) * y).bmod n = (x * y).bmod n

Tactic:
rw [Int.sub_mul, Int.sub_eq_add_neg, ← Int.mul_neg, bmod_add_mul_cancel, emod_mul_bmod_congr]

Result:
no goals

Proof state:
x : Int
n : Nat
y : Int
⊢ ((if x % ↑n < (↑n + 1) / 2 then x % ↑n else x % ↑n - ↑n) * y).bmod n = (x * y).bmod n

Tactic:
split

Result:
case isTrue
x : Int
n : Nat
y : Int
h✝ : x % ↑n < (↑n + 1) / 2
⊢ (x % ↑n * y).bmod n = (x * y).bmod n

case isFalse
x : Int
n : Nat
y : Int
h✝ : ¬x % ↑n < (↑n + 1) / 2
⊢ ((x % ↑n - ↑n) * y).bmod n = (x * y).bmod n

Proof state:
x : Int
n : Nat
y : Int
p : x % ↑n < (↑n + 1) / 2
⊢ (x % ↑n * y).bmod n = (x * y).bmod n

Tactic:
simp

Result:
no goals

Proof state:
x : Int
n : Nat
y : Int
⊢ (x.bmod n * y).bmod n = (x * y).bmod n

Tactic:
rw [bmod_def x n]

Result:
x : Int
n : Nat
y : Int
⊢ ((if x % ↑n < (↑n + 1) / 2 then x % ↑n else x % ↑n - ↑n) * y).bmod n = (x * y).bmod n

Proof state:
case isTrue
x : Int
n : Nat
y : Int
h✝ : x % ↑n < (↑n + 1) / 2
⊢ (x % ↑n * y).bmod n = (x * y).bmod n

case isFalse
x : Int
n : Nat
y : Int
h✝ : ¬x % ↑n < (↑n + 1) / 2
⊢ ((x % ↑n - ↑n) * y).bmod n = (x * y).bmod n

Tactic:
next p =>
  simp

Result:
case isFalse
x : Int
n : Nat
y : Int
h✝ : ¬x % ↑n < (↑n + 1) / 2
⊢ ((x % ↑n - ↑n) * y).bmod n = (x * y).bmod n

Proof state:
case isFalse
x : Int
n : Nat
y : Int
h✝ : ¬x % ↑n < (↑n + 1) / 2
⊢ ((x % ↑n - ↑n) * y).bmod n = (x * y).bmod n

Tactic:
next p =>
  rw [Int.sub_mul, Int.sub_eq_add_neg, ← Int.mul_neg, bmod_add_mul_cancel, emod_mul_bmod_congr]

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extend_target_mem_nhdsWithin {y : M} (hy : y ∈ f.source) :
    (f.extend I).target ∈ 𝓝[range I] f.extend I y

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
y : M
hy : y ∈ f.source
⊢ (f.extend I).target ∈ 𝓝[range ↑I] ↑(f.extend I) y

Tactic:
rw [← PartialEquiv.image_source_eq_target, ← map_extend_nhds f hy]

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
y : M
hy : y ∈ f.source
⊢ ↑(f.extend I) '' (f.extend I).source ∈ map (↑(f.extend I)) (𝓝 y)

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
y : M
hy : y ∈ f.source
⊢ ↑(f.extend I) '' (f.extend I).source ∈ map (↑(f.extend I)) (𝓝 y)

Tactic:
exact image_mem_map (extend_source_mem_nhds _ hy)

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem zmodEquivZPowers_apply_coe_int (i : ℤ) :
    h.zmodEquivZPowers i = Additive.ofMul (⟨ζ ^ i, i, rfl⟩ : Subgroup.zpowers ζ)

Proof state:
R : Type u_4
k : ℕ
inst✝ : CommRing R
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℤ
⊢ h.zmodEquivZPowers ↑i = Additive.ofMul ⟨ζ ^ i, ⋯⟩

Tactic:
rw [zmodEquivZPowers, AddEquiv.ofBijective_apply]

Result:
R : Type u_4
k : ℕ
inst✝ : CommRing R
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℤ
⊢ (((Int.castAddHom (ZMod k)).liftOfRightInverse ZMod.cast ⋯)
        ⟨{ toFun := fun i => Additive.ofMul ⟨(fun x => ζ ^ x) i, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩)
      ↑i =
    Additive.ofMul ⟨ζ ^ i, ⋯⟩

Proof state:
R : Type u_4
k : ℕ
inst✝ : CommRing R
ζ : Rˣ
h : IsPrimitiveRoot ζ k
i : ℤ
⊢ (((Int.castAddHom (ZMod k)).liftOfRightInverse ZMod.cast ⋯)
        ⟨{ toFun := fun i => Additive.ofMul ⟨(fun x => ζ ^ x) i, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }, ⋯⟩)
      ↑i =
    Additive.ofMul ⟨ζ ^ i, ⋯⟩

Tactic:
exact AddMonoidHom.liftOfRightInverse_comp_apply _ _ ZMod.intCast_rightInverse _ _

Result:
no goals