mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
K : Type u_3
inst✝⁴ : Semifield K
inst✝³ : CharZero K
inst✝² : Fintype ι
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
f : ι → K
i : ι
⊢ 𝔼 j, (if j = i then ↑(Fintype.card ι) else 0) * f j = f i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
⊢ a ≤ (F.intervalGapsWithin h a b ↑j).1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → Semiring (G i)
inst✝¹ : (i : ι) → Algebra R (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)
r : R
i : ι
x✝ : G i
⊢ ((map₀RingHom f).comp (algebraMap R ((i : ι) → G i))) r * ⟦⟨i, x✝⟩⟧ =
    ⟦⟨i, x✝⟩⟧ * ((map₀RingHom f).comp (algebraMap R ((i : ι) → G i))) r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
K : Type u_3
inst✝¹ : Semifield K
inst✝ : CharZero K
s : Finset ι
f : ι → K
⊢ 𝔼 i ∈ s, f i = (∑ i ∈ s, f i) / ↑(#s)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
K : Type u_3
inst✝¹ : Semifield K
inst✝ : CharZero K
s : Finset ι
f : ι → K
a : K
⊢ (𝔼 i ∈ s, f i) / a = 𝔼 i ∈ s, f i / a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
α : Type u_6
π : α → Type u_7
inst✝¹ : (a : α) → CommSemiring (π a)
inst✝ : (a : α) → Module ℚ≥0 (π a)
s : Finset ι
f : ι → (a : α) → π a
a : α
⊢ (𝔼 i ∈ s, f i) a = 𝔼 i ∈ s, f i a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → Semiring (G i)
inst✝¹ : (i : ι) → Algebra R (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)
r : R
i : ι
x✝ : G i
⊢ r • ⟦⟨i, x✝⟩⟧ = ((map₀RingHom f).comp (algebraMap R ((i : ι) → G i))) r * ⟦⟨i, x✝⟩⟧

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
e : ι → κ
he : Bijective e
f : ι → M
g : κ → M
h : ∀ (i : ι), f i = g (e i)
⊢ Set.SurjOn e ↑univ ↑univ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ (i j : ι), p i → p j → i = j
a : M
⊢ ∀ i ∈ univ, ∀ j ∈ univ, p i → p j → i = j

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj✝ : j < k + 1
hj : ¬j = k
⊢ j ∈ Iio k

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ (i j : ι), p i → p j → i = j
a : M
⊢ (𝔼 i, if p i then a else 0) = if ∃ i, p i then (↑(card ι))⁻¹ • a else 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
inst✝ : DecidableEq ι
s : Finset ι
f : ι → M
⊢ (𝔼 i, if i ∈ s then f i else 0) = s.dens • 𝔼 i ∈ s, f i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
inst✝ : DecidableEq ι
i : ι
f : (j : ι) → i = j → M
⊢ (𝔼 j, if h : i = j then f j h else 0) = (↑(card ι))⁻¹ • f i ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
inst✝ : DecidableEq ι
i : ι
f : (j : ι) → j = i → M
⊢ (𝔼 j, if h : j = i then f j h else 0) = (↑(card ι))⁻¹ • f i ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
inst✝ : DecidableEq ι
i : ι
f : ι → M
⊢ (𝔼 j, if i = j then f j else 0) = (↑(card ι))⁻¹ • f i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
inst✝ : DecidableEq ι
i : ι
f : ι → M
⊢ (𝔼 j, if j = i then f j else 0) = (↑(card ι))⁻¹ • f i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
⊢ (F.intervalGapsWithin h a b ↑j).2 ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹⁰ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁹ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁸ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁷ : IsDirectedOrder ι
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (G i)
inst✝⁴ : (i : ι) → Module R (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), LinearMapClass (T h) R (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
g₁ g₂ : DirectLimit G f →ₗ[R] P
h : ∀ (i : ι), g₁ ∘ₗ of R ι G f i = g₂ ∘ₗ of R ι G f i
⊢ g₁ = g₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := F.intervalGapsWithin h a b
i : ℕ
x✝ : i ∈ range k
⊢ i ∈ Set.Iio k

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁵ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁴ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝³ : IsDirectedOrder ι
inst✝² : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)
inst✝ : Nonempty ι
i j : ι
hij : i ≤ j
x : G i
⊢ (of G f j) ((f i j hij) x) = (of G f i) x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
this : ∀ j < k + 1, (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2
hj : ¬j < k + 1
⊢ ↑↑j < k + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
p : Fin (k + 1) → α × α := F.intervalGapsWithin h a b
z : α × α
hz : z ∈ F
i : ℕ
hi₁ : i ∈ Set.Iio k
hi₂ : (fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) i = z
⊢ i ∈ range k

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁶ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁵ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁴ : IsDirectedOrder ι
inst✝³ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝² : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)
inst✝¹ : Nonempty ι
P : Type u_7
inst✝ : NonUnitalNonAssocSemiring P
g₁ g₂ : DirectLimit G f →ₙ+* P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
⊢ g₁ = g₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
f : α → α → β
⊢ ∏ z ∈ F, f z.1 z.2 = ∏ i ∈ range k, f (F.intervalGapsWithin h a b ↑i).2 (F.intervalGapsWithin h a b ↑i.succ).1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁶ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁵ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁴ : IsDirectedOrder ι
inst✝³ : (i : ι) → NonAssocSemiring (G i)
inst✝² : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)
inst✝¹ : Nonempty ι
P : Type u_7
inst✝ : NonAssocSemiring P
g₁ g₂ : DirectLimit G f →+* P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
⊢ g₁ = g₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : Type u_2
inst✝¹⁰ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁹ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁸ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁷ : IsDirectedOrder ι
inst✝⁶ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝⁵ : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)
inst✝⁴ : (i : ι) → StarRing (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring P
inst✝ : StarRing P
g₁ g₂ : DirectLimit G f →⋆ₙ+* P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
⊢ g₁ = g₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → Semiring (G i)
inst✝² : (i : ι) → Algebra R (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)
inst✝ : Nonempty ι
i : ι
r : R
⊢ ⟦⟨i, (algebraMap R (G i)) r⟩⟧ = (algebraMap R (DirectLimit G f)) r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
g : α → β
⊢ (∏ i ∈ range (k + 1), g (F.intervalGapsWithin h a b ↑i).2 / g (F.intervalGapsWithin h a b ↑i).1) *
      ∏ z ∈ F, g z.2 / g z.1 =
    g b / g a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹¹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝¹⁰ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁹ : (i : ι) → FunLike (H i) (G i) C
inst✝⁸ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁷ : IsDirectedOrder ι
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → Semiring (G i)
inst✝⁴ : (i : ι) → Algebra R (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : Semiring P
inst✝ : Algebra R P
g : (i : ι) → G i →ₐ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
r : R
⊢ DirectLimit.lift f (fun x1 x2 ↦ (g x1) x2) ⋯ ((algebraMap R (DirectLimit G f)) r) = (algebraMap R P) r

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : j = 0
hk : ¬0 = k
⊢ 0 ∈ Iio k

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Neg α
γ : Type u_3
inst✝ : Neg β
f : β → γ
hf : Function.Even f
g : α → β
hg : Function.Odd g
⊢ Function.Even (f ∘ g)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Neg α
γ : Type u_3
inst✝¹ : Neg β
inst✝ : Neg γ
f : β → γ
hf : Function.Odd f
g : α → β
hg : Function.Odd g
⊢ Function.Odd (f ∘ g)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Neg α
inst✝ : Add β
f g : α → β
hf : Function.Even f
hg : Function.Even g
⊢ Function.Even (f + g)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Neg α
inst✝ : SubtractionCommMonoid β
f g : α → β
hf : Function.Odd f
hg : Function.Odd g
a : α
⊢ (f + g) (-a) = -(f + g) a

Tactic:
simp only [hf a, hg a, Pi.add_apply, neg_add]

Goal state after:
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Neg α
inst✝ : SubtractionCommMonoid β
f g : α → β
hf : Function.Odd f
hg : Function.Odd g
⊢ Function.Odd (f + g)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst✝ : SMul β γ
hf : Function.Even f
hg : Function.Even g
⊢ Function.Even (f • g)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst✝² : Monoid β
inst✝¹ : AddGroup γ
inst✝ : DistribMulAction β γ
hf : Function.Even f
hg : Function.Odd g
⊢ Function.Odd (f • g)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst✝² : Ring β
inst✝¹ : AddCommGroup γ
inst✝ : Module β γ
hf : Function.Odd f
hg : Function.Even g
⊢ Function.Odd (f • g)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Neg α
γ : Type u_3
f : α → β
g : α → γ
inst✝² : Ring β
inst✝¹ : AddCommGroup γ
inst✝ : Module β γ
hf : Function.Odd f
hg : Function.Odd g
⊢ Function.Even (f • g)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Neg α
γ : Type u_3
g : α → γ
inst✝ : SMul β γ
hg : Function.Even g
r : β
⊢ Function.Even (r • g)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
⊢ k - 1 + 1 = k

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹⁰ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁹ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁸ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁷ : IsDirectedOrder ι
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → Semiring (G i)
inst✝⁴ : (i : ι) → Algebra R (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : Semiring P
inst✝ : Algebra R P
g₁ g₂ : DirectLimit G f →ₐ[R] P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
⊢ g₁ = g₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Neg α
γ : Type u_3
g : α → γ
inst✝² : Monoid β
inst✝¹ : AddGroup γ
inst✝ : DistribMulAction β γ
hg : Function.Odd g
r : β
⊢ Function.Odd (r • g)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
inst✝¹ : Neg α
R : Type u_3
inst✝ : Mul R
f g : α → R
hf : Function.Even f
hg : Function.Even g
⊢ Function.Even (f * g)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝² : (i : ι) → DistribMulAction R (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)
inst✝ : Nonempty ι
i : ι
m : R
x : G i
⊢ ⟦⟨i, m • x⟩⟧ = (MonoidHom.id R) m • ⟦⟨i, x⟩⟧

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
inst✝² : Neg α
R : Type u_3
inst✝¹ : Mul R
f g : α → R
inst✝ : HasDistribNeg R
hf : Function.Even f
hg : Function.Odd g
⊢ Function.Odd (f * g)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹¹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝¹⁰ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁹ : (i : ι) → FunLike (H i) (G i) C
inst✝⁸ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁷ : IsDirectedOrder ι
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝⁴ : (i : ι) → DistribMulAction R (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring P
inst✝ : DistribMulAction R P
g : (i : ι) → G i →ₙₐ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
m : R
⊢ ∀ (x : DirectLimit G f),
    DirectLimit.lift f (fun x1 x2 ↦ (g x1) x2) ⋯ (m • x) =
      (MonoidHom.id R) m • DirectLimit.lift f (fun x1 x2 ↦ (g x1) x2) ⋯ x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : j = k
⊢ j - 1 ∈ Iio k

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
inst✝² : Neg α
R : Type u_3
inst✝¹ : Mul R
f g : α → R
inst✝ : HasDistribNeg R
hf : Function.Odd f
hg : Function.Even g
⊢ Function.Odd (f * g)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
inst✝² : Neg α
R : Type u_3
inst✝¹ : Mul R
f g : α → R
inst✝ : HasDistribNeg R
hf : Function.Odd f
hg : Function.Odd g
⊢ Function.Even (f * g)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : AddCommGroup β
inst✝¹ : IsAddTorsionFree β
f : α → β
inst✝ : Neg α
he : Function.Even f
ho : Function.Odd f
⊢ f = 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
F✝ : Finset (α × α)
h✝ : #F✝ = k
a✝ b✝ : α
⊢ 0 < j

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : AddCommGroup β
inst✝¹ : IsAddTorsionFree β
inst✝ : InvolutiveNeg α
f : α → β
hf : Function.Odd f
s : Finset α
hs : Finset.map (Equiv.toEmbedding (Equiv.neg α)) s = s
⊢ s.sum f = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : AddCommGroup β
inst✝¹ : IsAddTorsionFree β
f : α → β
inst✝ : NegZeroClass α
hf : Function.Odd f
⊢ f 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹⁰ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁹ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁸ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁷ : IsDirectedOrder ι
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝⁴ : (i : ι) → DistribMulAction R (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring P
inst✝ : DistribMulAction R P
g₁ g₂ : DirectLimit G f →ₙₐ[R] P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
⊢ g₁ = g₂

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
F✝ : Finset (α × α)
h✝ : #F✝ = k
a✝ b✝ : α
⊢ j - 1 < k

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b x : ℤ
⊢ x ∈ map (Nat.castEmbedding.trans (addLeftEmbedding a)) (range (b + 1 - a).toNat) ↔ a ≤ x ∧ x ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b x : ℤ
⊢ x ∈ map (Nat.castEmbedding.trans (addLeftEmbedding a)) (range (b - a).toNat) ↔ a ≤ x ∧ x < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
hk : k - 1 + 1 = k
hj₂ : ¬j = k
F✝ : Finset (α × α)
h✝ : #F✝ = k
a✝ b✝ : α
⊢ j < k

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
⊢ IsTensorProduct (mk R M N)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
x₁ : M₁
x₂ : M₂
⊢ h.equiv.symm ((f x₁) x₂) = x₁ ⊗ₜ[R] x₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b x : ℤ
⊢ x ∈ map (Nat.castEmbedding.trans (addLeftEmbedding (a + 1))) (range (b - a).toNat) ↔ a < x ∧ x ≤ b

Tactic:
by

Goal state after: