harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem logMap_eq_of_normAtPlace_eq (h : ∀ w, normAtPlace w x = normAtPlace w y) :
    logMap x = logMap y

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
h : ∀ (w : InfinitePlace K), (normAtPlace w) x = (normAtPlace w) y
⊢ logMap x = logMap y

Tactic:
ext

Result:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
h : ∀ (w : InfinitePlace K), (normAtPlace w) x = (normAtPlace w) y
x✝ : { w // w ≠ w₀ }
⊢ logMap x x✝ = logMap y x✝

Proof state:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
h : ∀ (w : InfinitePlace K), (normAtPlace w) x = (normAtPlace w) y
x✝ : { w // w ≠ w₀ }
⊢ logMap x x✝ = logMap y x✝

Tactic:
simp_rw [logMap_apply, h, norm_eq_of_normAtPlace_eq h]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Pseudoelements.lean
theorem comp_apply {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R) (a : P) : (f ≫ g) a = g (f a) :=
  Quotient.inductionOn a fun x =>
    Quotient.sound <| by
      simp only [app]
      rw [← Category.assoc, Over.coe_hom]

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
a : Pseudoelement P
x : Over P
⊢ (fun g_1 => app (f ≫ g) g_1) x ≈ (fun g_1 => app g g_1) ((fun g => app f g) x)

Tactic:
simp only [app]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
a : Pseudoelement P
x : Over P
⊢ Over.mk (x.hom ≫ f ≫ g) ≈ Over.mk ((Over.mk (x.hom ≫ f)).hom ≫ g)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
a : Pseudoelement P
x : Over P
⊢ Over.mk (x.hom ≫ f ≫ g) ≈ Over.mk ((Over.mk (x.hom ≫ f)).hom ≫ g)

Tactic:
rw [← Category.assoc, Over.coe_hom]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem edgeSet_sSup (s : Set G.Subgraph) : (sSup s).edgeSet = ⋃ G' ∈ s, edgeSet G'

Proof state:
case h
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
e : Sym2 V
⊢ e ∈ (sSup s).edgeSet ↔ e ∈ ⋃ G' ∈ s, G'.edgeSet

Tactic:
induction e

Result:
case h.h
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
x✝ y✝ : V
⊢ s(x✝, y✝) ∈ (sSup s).edgeSet ↔ s(x✝, y✝) ∈ ⋃ G' ∈ s, G'.edgeSet

Proof state:
case h.h
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
x✝ y✝ : V
⊢ s(x✝, y✝) ∈ (sSup s).edgeSet ↔ s(x✝, y✝) ∈ ⋃ G' ∈ s, G'.edgeSet

Tactic:
simp

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
⊢ (sSup s).edgeSet = ⋃ G' ∈ s, G'.edgeSet

Tactic:
ext e

Result:
case h
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
e : Sym2 V
⊢ e ∈ (sSup s).edgeSet ↔ e ∈ ⋃ G' ∈ s, G'.edgeSet
-- Mathlib/RingTheory/Polynomial/HilbertPoly.lean
lemma hilbertPoly_mul_one_sub_succ (p : F[X]) (d : ℕ) :
    hilbertPoly (p * (1 - X)) (d + 1) = hilbertPoly p d

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
⊢ (p * (1 - X)).hilbertPoly (d + 1) = p.hilbertPoly d

Tactic:
apply eq_hilbertPoly_of_forall_coeff_eq_eval (p * (1 - X)).natDegree

Result:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
⊢ ∀ n > (p * (1 - X)).natDegree,
    (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) ((p * (1 - X)).hilbertPoly (d + 1))

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d n : ℕ
hn : n > (p * (1 - X)).natDegree
⊢ (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) ((p * (1 - X)).hilbertPoly (d + 1))

Tactic:
have heq : 1 - PowerSeries.X = ((1 - X : F[X]) : F⟦X⟧) := by simp only [coe_sub, coe_one, coe_X]

Result:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d n : ℕ
hn : n > (p * (1 - X)).natDegree
heq : 1 - PowerSeries.X = ↑(1 - X)
⊢ (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) ((p * (1 - X)).hilbertPoly (d + 1))

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d n : ℕ
hn : n > (p * (1 - X)).natDegree
heq : 1 - PowerSeries.X = ↑(1 - X)
⊢ (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) ((p * (1 - X)).hilbertPoly (d + 1))

Tactic:
rw [← one_sub_pow_mul_invOneSubPow_val_add_eq_invOneSubPow_val F d 1, pow_one, ← mul_assoc, heq,
  ← coe_mul, coeff_mul_invOneSubPow_eq_hilbertPoly_eval (d + 1) hn]

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d n : ℕ
hn : n > (p * (1 - X)).natDegree
⊢ 1 - PowerSeries.X = ↑(1 - X)

Tactic:
simp only [coe_sub, coe_one, coe_X]

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
⊢ ∀ n > (p * (1 - X)).natDegree,
    (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) ((p * (1 - X)).hilbertPoly (d + 1))

Tactic:
intro n hn

Result:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d n : ℕ
hn : n > (p * (1 - X)).natDegree
⊢ (PowerSeries.coeff F n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) ((p * (1 - X)).hilbertPoly (d + 1))
-- Mathlib/MeasureTheory/Measure/Prod.lean
/-- If `Prod.snd ⁻¹' t` is a null measurable set and `μ ≠ 0`, then `t` is a null measurable set. -/
lemma _root_.MeasureTheory.NullMeasurableSet.of_preimage_snd [NeZero μ] {t : Set β}
    (h : NullMeasurableSet (Prod.snd ⁻¹' t) (μ.prod ν)) : NullMeasurableSet t ν :=
  .right_of_prod (by rwa [univ_prod]) (NeZero.ne (μ univ))

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : NeZero μ
t : Set β
h : NullMeasurableSet (Prod.snd ⁻¹' t) (μ.prod ν)
⊢ NullMeasurableSet (univ ×ˢ t) (μ.prod ν)

Tactic:
rwa [univ_prod]

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Alternating/Centralizer.lean
/-- The number of cycles of given length -/
lemma card_of_cycleType_singleton {n : ℕ} (hn : 2 ≤ n) (hα : n ≤ card α) :
    #({g | g.val.cycleType = {n}} : Finset (alternatingGroup α)) =
      if Odd n then (n - 1)! * (choose (card α) n) else 0

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
hn : 2 ≤ n
hα : n ≤ Fintype.card α
⊢ (if Even (n + 1) then #(filter (fun g => g.cycleType = {n}) univ) else 0) =
    if Odd n then (n - 1)! * (Fintype.card α).choose n else 0

Tactic:
simp_rw [← Nat.not_odd_iff_even, Nat.odd_add_one, not_not,
  Perm.card_of_cycleType_singleton hn hα]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
hn : 2 ≤ n
hα : n ≤ Fintype.card α
⊢ #(filter (fun g => (↑g).cycleType = {n}) univ) = if Odd n then (n - 1)! * (Fintype.card α).choose n else 0

Tactic:
rw [← card_map, map_subtype_of_cycleType, apply_ite Finset.card]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
hn : 2 ≤ n
hα : n ≤ Fintype.card α
⊢ (if Even ({n}.sum + {n}.card) then #(filter (fun g => g.cycleType = {n}) univ) else #∅) =
    if Odd n then (n - 1)! * (Fintype.card α).choose n else 0

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
hn : 2 ≤ n
hα : n ≤ Fintype.card α
⊢ (if Even ({n}.sum + {n}.card) then #(filter (fun g => g.cycleType = {n}) univ) else #∅) =
    if Odd n then (n - 1)! * (Fintype.card α).choose n else 0

Tactic:
simp only [Multiset.sum_singleton, Multiset.card_singleton, Finset.card_empty]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
hn : 2 ≤ n
hα : n ≤ Fintype.card α
⊢ (if Even (n + 1) then #(filter (fun g => g.cycleType = {n}) univ) else 0) =
    if Odd n then (n - 1)! * (Fintype.card α).choose n else 0
-- Mathlib/Data/Part.lean
theorem inv_mem_inv [Inv α] (a : Part α) (ma : α) (ha : ma ∈ a) : ma⁻¹ ∈ a⁻¹

Proof state:
α : Type u_1
inst✝ : Inv α
a : Part α
ma : α
ha : ma ∈ a
⊢ ma⁻¹ ∈ a⁻¹

Tactic:
simp [inv_def]

Result:
α : Type u_1
inst✝ : Inv α
a : Part α
ma : α
ha : ma ∈ a
⊢ ∃ a_1 ∈ a, a_1⁻¹ = ma⁻¹

Proof state:
α : Type u_1
inst✝ : Inv α
a : Part α
ma : α
ha : ma ∈ a
⊢ ∃ a_1 ∈ a, a_1⁻¹ = ma⁻¹

Tactic:
aesop

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
@[nontriviality]
lemma coeffs_eq_empty_of_subsingleton [Subsingleton R] (p : MvPolynomial σ R) : p.coeffs = ∅

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Subsingleton R
p : MvPolynomial σ R
⊢ p.coeffs = ∅

Tactic:
simpa [coeffs] using Subsingleton.eq_zero p

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem reverse_zipWith :
    (zipWith f l l').reverse = zipWith f l.reverse l'.reverse

Proof state:
case mk.mk
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
l : Array α✝²
l' : Array α✝¹
h : l'.size = l.size
⊢ (zipWith f { toArray := l, size_toArray := ⋯ } { toArray := l', size_toArray := h }).reverse =
    zipWith f { toArray := l, size_toArray := ⋯ }.reverse { toArray := l', size_toArray := h }.reverse

Tactic:
simp [Array.reverse_zipWith, h]

Result:
no goals

Proof state:
case mk
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
l : Array α✝²
l' : Vector α✝¹ l.size
⊢ (zipWith f { toArray := l, size_toArray := ⋯ } l').reverse =
    zipWith f { toArray := l, size_toArray := ⋯ }.reverse l'.reverse

Tactic:
rcases l' with ⟨l', h⟩

Result:
case mk.mk
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
l : Array α✝²
l' : Array α✝¹
h : l'.size = l.size
⊢ (zipWith f { toArray := l, size_toArray := ⋯ } { toArray := l', size_toArray := h }).reverse =
    zipWith f { toArray := l, size_toArray := ⋯ }.reverse { toArray := l', size_toArray := h }.reverse

Proof state:
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
n✝ : Nat
l : Vector α✝² n✝
l' : Vector α✝¹ n✝
⊢ (zipWith f l l').reverse = zipWith f l.reverse l'.reverse

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
l : Array α✝²
l' : Vector α✝¹ l.size
⊢ (zipWith f { toArray := l, size_toArray := ⋯ } l').reverse =
    zipWith f { toArray := l, size_toArray := ⋯ }.reverse l'.reverse
-- Mathlib/Algebra/MvPolynomial/Variables.lean
theorem vars_C_mul (a : A) (ha : a ≠ 0) (φ : MvPolynomial σ A) :
    (C a * φ : MvPolynomial σ A).vars = φ.vars

Proof state:
σ : Type u_1
A : Type u_3
inst✝¹ : CommRing A
inst✝ : NoZeroDivisors A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
d : σ →₀ ℕ
⊢ coeff d (C a * φ) ≠ 0 ↔ coeff d φ ≠ 0

Tactic:
rw [coeff_C_mul, mul_ne_zero_iff, eq_true ha, true_and]

Result:
no goals

Proof state:
σ : Type u_1
A : Type u_3
inst✝¹ : CommRing A
inst✝ : NoZeroDivisors A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
⊢ (C a * φ).vars = φ.vars

Tactic:
ext1 i

Result:
case h
σ : Type u_1
A : Type u_3
inst✝¹ : CommRing A
inst✝ : NoZeroDivisors A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
⊢ i ∈ (C a * φ).vars ↔ i ∈ φ.vars

Proof state:
case h
σ : Type u_1
A : Type u_3
inst✝¹ : CommRing A
inst✝ : NoZeroDivisors A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
⊢ (∃ d, coeff d (C a * φ) ≠ 0 ∧ i ∈ d.support) ↔ ∃ d, coeff d φ ≠ 0 ∧ i ∈ d.support

Tactic:
apply exists_congr

Result:
case h.h
σ : Type u_1
A : Type u_3
inst✝¹ : CommRing A
inst✝ : NoZeroDivisors A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
⊢ ∀ (a_1 : σ →₀ ℕ), coeff a_1 (C a * φ) ≠ 0 ∧ i ∈ a_1.support ↔ coeff a_1 φ ≠ 0 ∧ i ∈ a_1.support

Proof state:
case h.h
σ : Type u_1
A : Type u_3
inst✝¹ : CommRing A
inst✝ : NoZeroDivisors A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
d : σ →₀ ℕ
⊢ coeff d (C a * φ) ≠ 0 ∧ i ∈ d.support ↔ coeff d φ ≠ 0 ∧ i ∈ d.support

Tactic:
apply and_congr _ Iff.rfl

Result:
σ : Type u_1
A : Type u_3
inst✝¹ : CommRing A
inst✝ : NoZeroDivisors A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
d : σ →₀ ℕ
⊢ coeff d (C a * φ) ≠ 0 ↔ coeff d φ ≠ 0

Proof state:
case h
σ : Type u_1
A : Type u_3
inst✝¹ : CommRing A
inst✝ : NoZeroDivisors A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
⊢ i ∈ (C a * φ).vars ↔ i ∈ φ.vars

Tactic:
simp only [mem_vars, exists_prop, mem_support_iff]

Result:
case h
σ : Type u_1
A : Type u_3
inst✝¹ : CommRing A
inst✝ : NoZeroDivisors A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
⊢ (∃ d, coeff d (C a * φ) ≠ 0 ∧ i ∈ d.support) ↔ ∃ d, coeff d φ ≠ 0 ∧ i ∈ d.support

Proof state:
case h.h
σ : Type u_1
A : Type u_3
inst✝¹ : CommRing A
inst✝ : NoZeroDivisors A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
⊢ ∀ (a_1 : σ →₀ ℕ), coeff a_1 (C a * φ) ≠ 0 ∧ i ∈ a_1.support ↔ coeff a_1 φ ≠ 0 ∧ i ∈ a_1.support

Tactic:
intro d

Result:
case h.h
σ : Type u_1
A : Type u_3
inst✝¹ : CommRing A
inst✝ : NoZeroDivisors A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
d : σ →₀ ℕ
⊢ coeff d (C a * φ) ≠ 0 ∧ i ∈ d.support ↔ coeff d φ ≠ 0 ∧ i ∈ d.support
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem and_assoc (x y z : BitVec w) :
    x &&& y &&& z = x &&& (y &&& z)

Proof state:
case pred
w : Nat
x y z : BitVec w
i : Nat
a✝ : i < w
⊢ (x &&& y &&& z).getLsbD i = (x &&& (y &&& z)).getLsbD i

Tactic:
simp [Bool.and_assoc]

Result:
no goals

Proof state:
w : Nat
x y z : BitVec w
⊢ x &&& y &&& z = x &&& (y &&& z)

Tactic:
ext i

Result:
case pred
w : Nat
x y z : BitVec w
i : Nat
a✝ : i < w
⊢ (x &&& y &&& z).getLsbD i = (x &&& (y &&& z)).getLsbD i
-- Mathlib/Topology/Algebra/ConstMulAction.lean
theorem Dense.smul (c : G) {s : Set α} (hs : Dense s) : Dense (c • s)

Proof state:
α : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : ContinuousConstSMul G α
c : G
s : Set α
hs : Dense s
⊢ Dense (c • s)

Tactic:
rw [dense_iff_closure_eq] at hs ⊢

Result:
α : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : ContinuousConstSMul G α
c : G
s : Set α
hs : closure s = univ
⊢ closure (c • s) = univ

Proof state:
α : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : ContinuousConstSMul G α
c : G
s : Set α
hs : closure s = univ
⊢ closure (c • s) = univ

Tactic:
rw [closure_smul, hs, smul_set_univ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKeyD_modify [LawfulBEq α] {k k' fallback : α} {f : β k → β k} (h : m.WF) :
    (m.modify k f).getKeyD k' fallback =
      if k == k' then
        if k ∈ m then k else fallback
      else
        m.getKeyD k' fallback

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k k' fallback : α
f : β k → β k
h : m.WF
⊢ (m.modify k f).getKeyD k' fallback =
    if (k == k') = true then if m.contains k = true then k else fallback else m.getKeyD k' fallback

Tactic:
simp_to_raw using Raw₀.getKeyD_modify

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k k' fallback : α
f : β k → β k
h : m.WF
⊢ (m.modify k f).getKeyD k' fallback = if (k == k') = true then if k ∈ m then k else fallback else m.getKeyD k' fallback

Tactic:
simp only [mem_iff_contains]

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k k' fallback : α
f : β k → β k
h : m.WF
⊢ (m.modify k f).getKeyD k' fallback =
    if (k == k') = true then if m.contains k = true then k else fallback else m.getKeyD k' fallback
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_add {f g : α → G} (hf : Integrable f μ) (hg : Integrable g μ) :
    ∫ a, f a + g a ∂μ = ∫ a, f a ∂μ + ∫ a, g a ∂μ

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
hG : CompleteSpace G
⊢ (if h : True then
      if hf : Integrable (fun a => f a + g a) μ then L1.integralCLM (Integrable.toL1 (fun a => f a + g a) hf) else 0
    else 0) =
    (if h : True then if hf : Integrable (fun a => f a) μ then L1.integralCLM (Integrable.toL1 (fun a => f a) hf) else 0
      else 0) +
      if h : True then
        if hf : Integrable (fun a => g a) μ then L1.integralCLM (Integrable.toL1 (fun a => g a) hf) else 0
      else 0

Tactic:
exact setToFun_add (dominatedFinMeasAdditive_weightedSMul μ) hf hg

Result:
no goals

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
hG : CompleteSpace G
⊢ ∫ (a : α), f a + g a ∂μ = ∫ (a : α), f a ∂μ + ∫ (a : α), g a ∂μ

Tactic:
simp only [integral, hG, L1.integral]

Result:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
hG : CompleteSpace G
⊢ (if h : True then
      if hf : Integrable (fun a => f a + g a) μ then L1.integralCLM (Integrable.toL1 (fun a => f a + g a) hf) else 0
    else 0) =
    (if h : True then if hf : Integrable (fun a => f a) μ then L1.integralCLM (Integrable.toL1 (fun a => f a) hf) else 0
      else 0) +
      if h : True then
        if hf : Integrable (fun a => g a) μ then L1.integralCLM (Integrable.toL1 (fun a => g a) hf) else 0
      else 0

Proof state:
case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
hG : ¬CompleteSpace G
⊢ ∫ (a : α), f a + g a ∂μ = ∫ (a : α), f a ∂μ + ∫ (a : α), g a ∂μ

Tactic:
simp [integral, hG]

Result:
no goals

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
⊢ ∫ (a : α), f a + g a ∂μ = ∫ (a : α), f a ∂μ + ∫ (a : α), g a ∂μ

Tactic:
by_cases hG : CompleteSpace G

Result:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
hG : CompleteSpace G
⊢ ∫ (a : α), f a + g a ∂μ = ∫ (a : α), f a ∂μ + ∫ (a : α), g a ∂μ

case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
hG : ¬CompleteSpace G
⊢ ∫ (a : α), f a + g a ∂μ = ∫ (a : α), f a ∂μ + ∫ (a : α), g a ∂μ
-- Mathlib/Analysis/Analytic/Composition.lean
theorem blocksFun_sigmaCompositionAux (a : Composition n) (b : Composition a.length)
    (i : Fin b.length) (j : Fin (blocksFun b i)) :
    blocksFun (sigmaCompositionAux a b ⟨i, (length_gather a b).symm ▸ i.2⟩)
        ⟨j, (length_sigmaCompositionAux a b i).symm ▸ j.2⟩ =
      blocksFun a (embedding b i j)

Proof state:
n : ℕ
a : Composition n
b : Composition a.length
i : Fin b.length
j : Fin (b.blocksFun i)
⊢ a.blocks[b.sizeUpTo ↑⟨↑i, ⋯⟩ + ↑⟨↑j, ⋯⟩] = a.blocksFun ((b.embedding i) j)

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
a : Composition n
b : Composition a.length
i : Fin b.length
j : Fin (b.blocksFun i)
⊢ { blocks := (a.blocks.splitWrtComposition b)[↑⟨↑i, ⋯⟩], blocks_pos := ⋯, blocks_sum := ⋯ }.blocksFun ⟨↑j, ⋯⟩ =
    a.blocksFun ((b.embedding i) j)

Tactic:
rw [blocksFun, get_eq_getElem, getElem_of_eq (getElem_splitWrtComposition _ _ _ _),
  getElem_drop, getElem_take]

Result:
n : ℕ
a : Composition n
b : Composition a.length
i : Fin b.length
j : Fin (b.blocksFun i)
⊢ a.blocks[b.sizeUpTo ↑⟨↑i, ⋯⟩ + ↑⟨↑j, ⋯⟩] = a.blocksFun ((b.embedding i) j)

Proof state:
n : ℕ
a : Composition n
b : Composition a.length
i : Fin b.length
j : Fin (b.blocksFun i)
⊢ (a.sigmaCompositionAux b ⟨↑i, ⋯⟩).blocksFun ⟨↑j, ⋯⟩ = a.blocksFun ((b.embedding i) j)

Tactic:
unfold sigmaCompositionAux

Result:
n : ℕ
a : Composition n
b : Composition a.length
i : Fin b.length
j : Fin (b.blocksFun i)
⊢ { blocks := (a.blocks.splitWrtComposition b)[↑⟨↑i, ⋯⟩], blocks_pos := ⋯, blocks_sum := ⋯ }.blocksFun ⟨↑j, ⋯⟩ =
    a.blocksFun ((b.embedding i) j)
-- Mathlib/Analysis/InnerProductSpace/Orientation.lean
theorem abs_volumeForm_apply_le (v : Fin n → E) : |o.volumeForm v| ≤ ∏ i : Fin n, ‖v i‖

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
v : Fin n → E
⊢ |o.volumeForm v| ≤ ∏ i : Fin n, ‖v i‖

Tactic:
rcases n with - | n

Result:
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
v : Fin 0 → E
⊢ |o.volumeForm v| ≤ ∏ i : Fin 0, ‖v i‖

case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
⊢ |o.volumeForm v| ≤ ∏ i : Fin (n + 1), ‖v i‖

Proof state:
case succ.h1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
hb : b.toBasis.det v = ∏ i : Fin n.succ, inner (b i) (v i)
i : Fin n.succ
a✝ : i ∈ Finset.univ
⊢ |inner (b i) (v i)| ≤ ‖v i‖

Tactic:
convert abs_real_inner_le_norm (b i) (v i)

Result:
case h.e'_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
hb : b.toBasis.det v = ∏ i : Fin n.succ, inner (b i) (v i)
i : Fin n.succ
a✝ : i ∈ Finset.univ
⊢ ‖v i‖ = ‖b i‖ * ‖v i‖

Proof state:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin n.succ)
⊢ |o.volumeForm v| ≤ ∏ i : Fin (n + 1), ‖v i‖

Tactic:
let b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v

Result:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
⊢ |o.volumeForm v| ≤ ∏ i : Fin (n + 1), ‖v i‖

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this : FiniteDimensional ℝ E
⊢ finrank ℝ E = Fintype.card (Fin n.succ)

Tactic:
simpa using _i.out

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem HasStrictDerivAt.finset_prod (hf : ∀ i ∈ u, HasStrictDerivAt (f i) (f' i) x) :
    HasStrictDerivAt (∏ i ∈ u, f i ·) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) x

Proof state:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_2
inst✝² : DecidableEq ι
𝔸' : Type u_3
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
f' : ι → 𝔸'
hf : ∀ i ∈ u, HasStrictDerivAt (f i) (f' i) x
⊢ HasStrictDerivAt (fun x => ∏ i ∈ u, f i x) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) x

Tactic:
simpa [ContinuousLinearMap.sum_apply, ContinuousLinearMap.smul_apply] using
  (HasStrictFDerivAt.finset_prod (fun i hi ↦ (hf i hi).hasStrictFDerivAt)).hasStrictDerivAt

Result:
no goals
-- Mathlib/GroupTheory/Commutator/Basic.lean
theorem map_commutatorElement : (f ⁅g₁, g₂⁆ : G') = ⁅f g₁, f g₂⁆

Proof state:
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : FunLike F G G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ : G
⊢ f ⁅g₁, g₂⁆ = ⁅f g₁, f g₂⁆

Tactic:
simp_rw [commutatorElement_def, map_mul f, map_inv f]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_tail? (f : α → β) (l : List α) : (tail? l).map (map f) = tail? (map f l)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : List α
⊢ Option.map (map f) l.tail? = (map f l).tail?

Tactic:
cases l <;> rfl

Result:
no goals