awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Notation.Pi.Basic
Goal:
ι : Type u_1
M : ι → Type u_6
N : ι → Type u_7
O : ι → Type u_8
inst : (i : ι) → One (M i)
inst_1 : (i : ι) → One (N i)
inst_2 : (i : ι) → One (O i)
inst_3 : DecidableEq ι
f' : (i : ι) → M i → N i → O i
hf' : ∀ (i : ι), f' i 1 1 = 1
i : ι
x : M i
y : N i
j : ι
pos : ∀ (h : j = i), f' j (mulSingle (M := M) i x j) (mulSingle (M := N) i y j) = mulSingle (M := O) i (f' i x y) j
neg : ∀ (h : ¬j = i), f' j (mulSingle (M := M) i x j) (mulSingle (M := N) i y j) = mulSingle (M := O) i (f' i x y) j
⊢ f' j (mulSingle (M := M) i x j) (mulSingle (M := N) i y j) = mulSingle (M := O) i (f' i x y) j

Tactic:
by_cases h : j = i
-- Module: Mathlib.Algebra.Notation.Pi.Basic
Goal:
ι : Type u_1
M : ι → Type u_6
N : ι → Type u_7
O : ι → Type u_8
inst : (i : ι) → One (M i)
inst_1 : (i : ι) → One (N i)
inst_2 : (i : ι) → One (O i)
inst_3 : DecidableEq ι
f' : (i : ι) → M i → N i → O i
hf' : ∀ (i : ι), f' i 1 1 = 1
i : ι
x : M i
y : N i
j : ι
h : j = i
pos :
  ∀ (x : M j) (y : N j), f' j (mulSingle (M := M) j x j) (mulSingle (M := N) j y j) = mulSingle (M := O) j (f' j x y) j
⊢ f' j (mulSingle (M := M) i x j) (mulSingle (M := N) i y j) = mulSingle (M := O) i (f' i x y) j

Tactic:
subst h
-- Module: Mathlib.Algebra.Notation.Pi.Basic
Goal:
ι : Type u_1
M : ι → Type u_6
N : ι → Type u_7
O : ι → Type u_8
inst : (i : ι) → One (M i)
inst_1 : (i : ι) → One (N i)
inst_2 : (i : ι) → One (O i)
inst_3 : DecidableEq ι
f' : (i : ι) → M i → N i → O i
hf' : ∀ (i : ι), f' i 1 1 = 1
j : ι
x : M j
y : N j
⊢ f' j (mulSingle (M := M) j x j) (mulSingle (M := N) j y j) = mulSingle (M := O) j (f' j x y) j

Tactic:
simp only [mulSingle_eq_same]

Premises used: Pi.mulSingle_eq_same
-- Module: Mathlib.Algebra.Notation.Pi.Basic
Goal:
ι : Type u_1
M : ι → Type u_6
N : ι → Type u_7
O : ι → Type u_8
inst : (i : ι) → One (M i)
inst_1 : (i : ι) → One (N i)
inst_2 : (i : ι) → One (O i)
inst_3 : DecidableEq ι
f' : (i : ι) → M i → N i → O i
hf' : ∀ (i : ι), f' i 1 1 = 1
i : ι
x : M i
y : N i
j : ι
h : ¬j = i
⊢ f' j (mulSingle (M := M) i x j) (mulSingle (M := N) i y j) = mulSingle (M := O) i (f' i x y) j

Tactic:
simp only [mulSingle_eq_of_ne h, hf']

Premises used: Pi.mulSingle_eq_of_ne
-- Module: Mathlib.Algebra.Notation.Pi.Basic
Goal:
ι : Type u_1
M : ι → Type u_6
N : ι → Type u_7
inst : (i : ι) → One (M i)
inst_1 : (i : ι) → One (N i)
inst_2 : DecidableEq ι
op : (i : ι) → M i → N i
h : ∀ (i : ι), op i 1 = 1
i : ι
x : M i
⊢ mulSingle (M := N) i (op i x) = fun (j : ι) ↦ op j (mulSingle (M := M) i x j)

Tactic:
.symm <| funext <| apply_mulSingle op h i x

Premises used: funext, Eq.symm, Pi.apply_mulSingle
-- Module: Mathlib.Algebra.Notation.Pi.Basic
Goal:
ι : Type u_1
M : ι → Type u_6
N : ι → Type u_7
O : ι → Type u_8
inst : (i : ι) → One (M i)
inst_1 : (i : ι) → One (N i)
inst_2 : (i : ι) → One (O i)
inst_3 : DecidableEq ι
op : (i : ι) → M i → N i → O i
h : ∀ (i : ι), op i 1 1 = 1
i : ι
x : M i
y : N i
⊢ mulSingle (M := O) i (op i x y) = fun (j : ι) ↦ op j (mulSingle (M := M) i x j) (mulSingle (M := N) i y j)

Tactic:
.symm <| funext <| apply_mulSingle₂ op h i x y

Premises used: Pi.apply_mulSingle₂, funext, Eq.symm
-- Module: Mathlib.Algebra.Notation.Pi.Basic
Goal:
ι : Type u_1
M : ι → Type u_6
inst : (i : ι) → One (M i)
inst_1 : DecidableEq ι
i : ι
⊢ Injective (α := M i) (mulSingle (M := M) i)

Tactic:
Function.update_injective _ i

Premises used: Function.update_injective, Pi.mulSingle
-- Module: Mathlib.Algebra.Notation.Pi.Basic
Goal:
ι : Type u_1
M : ι → Type u_6
inst : (i : ι) → One (M i)
inst_1 : DecidableEq ι
i : ι
x y : M i
⊢ mulSingle (M := M) i x = mulSingle (M := M) i y ↔ x = y

Tactic:
(mulSingle_injective _).eq_iff

Premises used: Function.Injective.eq_iff, Pi.mulSingle_injective
-- Module: Mathlib.Algebra.Notation.Pi.Basic
Goal:
ι : Type u_1
inst : DecidableEq ι
M : Type u_9
inst_1 : One M
i : ι
x : M
i' : ι
⊢ mulSingle (M := fun (a : ι) ↦ M) i x i' = if i' = i then x else 1

Tactic:
Function.update_apply (1 : ι → M) i x i'

Premises used: Function.update_apply, OfNat.ofNat, Pi.mulSingle
-- Module: Mathlib.Algebra.Notation.Pi.Basic
Goal:
ι : Type u_1
inst : DecidableEq ι
M : Type u_9
inst_1 : One M
i : ι
x : M
j : ι
⊢ Eq.{u_9 + 1} (α := M) (mulSingle (M := fun (a : ι) ↦ M) i x j : M) (mulSingle (M := fun (a : ι) ↦ M) j x i : M)

Tactic:
simp [mulSingle_apply, eq_comm]

Premises used: eq_comm, Pi.mulSingle_apply
-- Module: Mathlib.Algebra.Notation.Pi.Basic
Goal:
ι : Type u_1
ι' : Type u_2
inst : DecidableEq ι
M : Type u_9
inst_1 : One M
inst_2 : DecidableEq ι'
i : ι × ι'
b : M
⊢ Eq (α := ι → ι' → M) (curry (mulSingle (M := fun (a : ι × ι') ↦ M) i b))
    (mulSingle (M := fun (j : ι) ↦ ι' → M) i.fst (mulSingle (M := fun (j : ι') ↦ M) i.snd b))

Tactic:
curry_update _ _ _

Premises used: Function.curry_update, Pi.mulSingle
-- Module: Mathlib.Algebra.Notation.Pi.Basic
Goal:
ι : Type u_1
ι' : Type u_2
inst : DecidableEq ι
M : Type u_9
inst_1 : One M
inst_2 : DecidableEq ι'
i : ι
i' : ι'
b : M
⊢ Eq (α := ι × ι' → M) (uncurry (mulSingle (M := fun (a : ι) ↦ ι' → M) i (mulSingle (M := fun (a : ι') ↦ M) i' b)))
    (mulSingle (M := fun (j : ι × ι') ↦ M) (i, i') b)

Tactic:
uncurry_update_update _ _ _ _

Premises used: Function.uncurry_update_update, Pi.mulSingle
-- Module: Mathlib.Algebra.Notation.Pi.Defs
Goal:
ι : Type u_1
M : ι → Type u_5
inst : (i : ι) → One (M i)
i : ι
⊢ Eq.{u_5 + 1} (α := M i) (1 i) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Pi.Defs
Goal:
ι : Type u_1
M : ι → Type u_5
inst : (i : ι) → One (M i)
⊢ Eq (α := (i : ι) → M i) 1 fun (x : ι) ↦ 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Pi.Defs
Goal:
α : Type u_2
M : Type u_7
inst : One M
⊢ Eq (α := α → M) (const α 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Pi.Defs
Goal:
α : Type u_2
β : Type u_3
M : Type u_7
inst : One M
f : α → β
⊢ Eq (α := α → M) (1 ∘ f) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Pi.Defs
Goal:
α : Type u_2
β : Type u_3
M : Type u_7
inst : One M
f : M → β
⊢ f ∘ 1 = const α (f 1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Pi.Defs
Goal:
ι : Type u_1
M : ι → Type u_5
inst : (i : ι) → Mul (M i)
f g : (i : ι) → M i
i : ι
⊢ (f * g) i = f i * g i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Pi.Defs
Goal:
ι : Type u_1
M : ι → Type u_5
inst : (i : ι) → Mul (M i)
f g : (i : ι) → M i
⊢ f * g = fun (i : ι) ↦ f i * g i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Pi.Defs
Goal:
ι : Type u_1
M : Type u_7
inst : Mul M
a b : M
⊢ const ι a * const ι b = const ι (a * b)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Pi.Defs
Goal:
α : Type u_2
β : Type u_3
M : Type u_7
inst : Mul M
f g : β → M
z : α → β
⊢ (f * g) ∘ z = f ∘ z * g ∘ z

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Pi.Defs
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Inv (G i)
f : (i : ι) → G i
i : ι
⊢ f⁻¹ i = (f i)⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Pi.Defs
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Inv (G i)
f : (i : ι) → G i
⊢ f⁻¹ = fun (i : ι) ↦ (f i)⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Pi.Defs
Goal:
ι : Type u_1
G : Type u_7
inst : Inv G
a : G
⊢ (const ι a)⁻¹ = const ι a⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Pi.Defs
Goal:
α : Type u_2
β : Type u_3
G : Type u_7
inst : Inv G
f : β → G
g : α → β
⊢ f⁻¹ ∘ g = (f ∘ g)⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Pi.Defs
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Div (G i)
f g : (i : ι) → G i
i : ι
⊢ (f / g) i = f i / g i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Pi.Defs
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Div (G i)
f g : (i : ι) → G i
⊢ f / g = fun (i : ι) ↦ f i / g i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Pi.Defs
Goal:
α : Type u_2
β : Type u_3
G : Type u_7
inst : Div G
f g : β → G
z : α → β
⊢ (f / g) ∘ z = f ∘ z / g ∘ z

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Pi.Defs
Goal:
ι : Type u_1
G : Type u_7
inst : Div G
a b : G
⊢ const ι a / const ι b = const ι (a / b)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Pi.Defs
Goal:
ι : Type u_1
α : Type u_2
M : ι → Type u_5
inst : (i : ι) → Pow.{u_5, u_2} (M i) α
f : (i : ι) → M i
a : α
i : ι
⊢ (f ^ a) i = f i ^ a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Pi.Defs
Goal:
ι : Type u_1
α : Type u_2
M : ι → Type u_5
inst : (i : ι) → Pow.{u_5, u_2} (M i) α
f : (i : ι) → M i
a : α
⊢ f ^ a = fun (i : ι) ↦ f i ^ a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Pi.Defs
Goal:
ι : Type u_1
α : Type u_2
M : Type u_7
inst : Pow M α
a : M
b : α
⊢ const ι a ^ b = const ι (a ^ b)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Pi.Defs
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
M : Type u_7
inst : Pow M α
f : β → M
a : α
g : ι → β
⊢ (f ^ a) ∘ g = f ∘ g ^ a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Pi.Defs
Goal:
ι : Type u_1
R : ι → Type u_6
inst : (i : ι) → Star (R i)
x : (i : ι) → R i
i : ι
⊢ star x i = star (x i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Pi.Defs
Goal:
ι : Type u_1
R : ι → Type u_6
inst : (i : ι) → Star (R i)
x : (i : ι) → R i
⊢ star x = fun (i : ι) ↦ star (x i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Prod
Goal:
M : Type u_3
N : Type u_4
inst : One M
inst_1 : One N
⊢ Eq.{u_3 + 1} (α := M) 1.1 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Prod
Goal:
M : Type u_3
N : Type u_4
inst : One M
inst_1 : One N
⊢ Eq.{u_4 + 1} (α := N) 1.2 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Prod
Goal:
M : Type u_3
N : Type u_4
inst : One M
inst_1 : One N
⊢ Eq (α := M × N) 1 (1, 1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Prod
Goal:
M : Type u_3
N : Type u_4
inst : One M
inst_1 : One N
⊢ Eq (α := M × N) (1, 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Prod
Goal:
M : Type u_3
N : Type u_4
inst : One M
inst_1 : One N
x : M
y : N
⊢ (x, y) = 1 ↔ x = 1 ∧ y = 1

Tactic:
mk_inj

Premises used: Prod.mk_inj
-- Module: Mathlib.Algebra.Notation.Prod
Goal:
M : Type u_3
N : Type u_4
inst : One M
inst_1 : One N
⊢ Eq (α := N × M) (swap 1) 1

Tactic:
rfl

Premises used: Prod.swap, rfl
-- Module: Mathlib.Algebra.Notation.Prod
Goal:
M : Type u_8
N : Type u_9
inst : Mul M
inst_1 : Mul N
p q : M × N
⊢ (p * q).1 = p.1 * q.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Prod
Goal:
M : Type u_8
N : Type u_9
inst : Mul M
inst_1 : Mul N
p q : M × N
⊢ (p * q).2 = p.2 * q.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Prod
Goal:
M : Type u_8
N : Type u_9
inst : Mul M
inst_1 : Mul N
a₁ a₂ : M
b₁ b₂ : N
⊢ (a₁, b₁) * (a₂, b₂) = (a₁ * a₂, b₁ * b₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Prod
Goal:
M : Type u_8
N : Type u_9
inst : Mul M
inst_1 : Mul N
p q : M × N
⊢ (p * q).swap = p.swap * q.swap

Tactic:
rfl

Premises used: Prod.swap, rfl
-- Module: Mathlib.Algebra.Notation.Prod
Goal:
M : Type u_8
N : Type u_9
inst : Mul M
inst_1 : Mul N
p q : M × N
⊢ p * q = (p.1 * q.1, p.2 * q.2)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Prod
Goal:
G : Type u_8
H : Type u_9
inst : Inv G
inst_1 : Inv H
p : G × H
⊢ p⁻¹.1 = p.1⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Prod
Goal:
G : Type u_8
H : Type u_9
inst : Inv G
inst_1 : Inv H
p : G × H
⊢ p⁻¹.2 = p.2⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Prod
Goal:
G : Type u_8
H : Type u_9
inst : Inv G
inst_1 : Inv H
a : G
b : H
⊢ (a, b)⁻¹ = (a⁻¹, b⁻¹)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Prod
Goal:
G : Type u_8
H : Type u_9
inst : Inv G
inst_1 : Inv H
p : G × H
⊢ p⁻¹.swap = p.swap⁻¹

Tactic:
rfl

Premises used: Prod.swap, rfl
-- Module: Mathlib.Algebra.Notation.Prod
Goal:
G : Type u_8
H : Type u_9
inst : Div G
inst_1 : Div H
a b : G × H
⊢ (a / b).1 = a.1 / b.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Prod
Goal:
G : Type u_8
H : Type u_9
inst : Div G
inst_1 : Div H
a b : G × H
⊢ (a / b).2 = a.2 / b.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Prod
Goal:
G : Type u_8
H : Type u_9
inst : Div G
inst_1 : Div H
x₁ x₂ : G
y₁ y₂ : H
⊢ (x₁, y₁) / (x₂, y₂) = (x₁ / x₂, y₁ / y₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Prod
Goal:
G : Type u_8
H : Type u_9
inst : Div G
inst_1 : Div H
a b : G × H
⊢ (a / b).swap = a.swap / b.swap

Tactic:
rfl

Premises used: Prod.swap, rfl
-- Module: Mathlib.Algebra.Notation.Prod
Goal:
G : Type u_8
H : Type u_9
inst : Div G
inst_1 : Div H
a b : G × H
⊢ a / b = (a.1 / b.1, a.2 / b.2)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Prod
Goal:
E : Type u_8
α : Type u_9
β : Type u_10
inst : Pow α E
inst_1 : Pow β E
p : α × β
c : E
⊢ (p ^ c).1 = p.1 ^ c

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Prod
Goal:
E : Type u_8
α : Type u_9
β : Type u_10
inst : Pow α E
inst_1 : Pow β E
p : α × β
c : E
⊢ (p ^ c).2 = p.2 ^ c

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Prod
Goal:
E : Type u_8
α : Type u_9
β : Type u_10
inst : Pow α E
inst_1 : Pow β E
a : α
b : β
c : E
⊢ (a, b) ^ c = (a ^ c, b ^ c)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Prod
Goal:
E : Type u_8
α : Type u_9
β : Type u_10
inst : Pow α E
inst_1 : Pow β E
p : α × β
c : E
⊢ p ^ c = (p.1 ^ c, p.2 ^ c)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Prod
Goal:
E : Type u_8
α : Type u_9
β : Type u_10
inst : Pow α E
inst_1 : Pow β E
p : α × β
c : E
⊢ (p ^ c).swap = p.swap ^ c

Tactic:
rfl

Premises used: Prod.swap, rfl
-- Module: Mathlib.Algebra.Notation.Prod
Goal:
R : Type u_6
S : Type u_7
inst : Star R
inst_1 : Star S
x : R × S
⊢ (star x).1 = star x.1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Prod
Goal:
R : Type u_6
S : Type u_7
inst : Star R
inst_1 : Star S
x : R × S
⊢ (star x).2 = star x.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Prod
Goal:
R : Type u_6
S : Type u_7
inst : Star R
inst_1 : Star S
x : R × S
⊢ star x = (star x.1, star x.2)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f : ι → M
⊢ mulSupport f = f ⁻¹' {1}ᶜ

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton, Function.mulSupport, Not, rfl
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f : ι → M
x : ι
⊢ ¬x ∈ mulSupport f ↔ f x = 1

Tactic:
not_not

Premises used: Classical.not_not, Set.Mem, setOf, Function.mulSupport, Not
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f : ι → M
⊢ (mulSupport f)ᶜ = {x : ι | f x = 1}

Tactic:
ext fun _ ↦ notMem_mulSupport

Premises used: Set.ext, Function.notMem_mulSupport
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f : ι → M
x : ι
⊢ x ∈ mulSupport f ↔ f x ≠ 1

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Function.mulSupport, Not
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f : ι → M
s : Set ι
⊢ mulSupport f ⊆ s ↔ ∀ (x : ι), f x ≠ 1 → x ∈ s

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.Subset, Function.mulSupport, Not
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f : ι → M
s : Set ι
⊢ mulSupport f ⊆ s ↔ ∀ (x : ι), ¬x ∈ s → f x = 1

Tactic:
forall_congr' fun _ ↦ not_imp_comm

Premises used: not_imp_comm, Set.Subset, forall_congr'
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f : ι → M
s : Set ι
⊢ mulSupport f = s ↔ (∀ (x : ι), x ∈ s → f x ≠ 1) ∧ ∀ (x : ι), ¬x ∈ s → f x = 1

Tactic:
simp +contextual only [Set.ext_iff, mem_mulSupport, ne_eq, iff_def,
    not_imp_comm, and_comm, forall_and]

Premises used: not_imp_comm, Function.mem_mulSupport, iff_def, and_comm, ne_eq, Set.ext_iff, forall_and
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f g : ι → M
h : mulSupport f = mulSupport g ∧ ∀ (x : ι), x ∈ mulSupport f → f x = g x
h₁ : mulSupport f = mulSupport g
h₂ : ∀ (x : ι), x ∈ mulSupport f → f x = g x
x : ι
hx : x ∈ mulSupport f
⊢ f x = g x

Tactic:
h₂ x hx
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f g : ι → M
h : mulSupport f = mulSupport g ∧ ∀ (x : ι), x ∈ mulSupport f → f x = g x
h₁ : mulSupport f = mulSupport g
h₂ : ∀ (x : ι), x ∈ mulSupport f → f x = g x
x : ι
hx : x ∈ mulSupport f
⊢ f x = g x

Tactic:
exact h₂ x hx
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f g : ι → M
h : mulSupport f = mulSupport g ∧ ∀ (x : ι), x ∈ mulSupport f → f x = g x
h₁ : mulSupport f = mulSupport g
h₂ : ∀ (x : ι), x ∈ mulSupport f → f x = g x
x : ι
hx : ¬x ∈ mulSupport f
rw : 1 = g x
rw₁ rw₂ : Eq.{u_3 + 1} (α := M) 1 1
⊢ f x = g x

Tactic:
rw [notMem_mulSupport.1 hx, notMem_mulSupport.1 (mt (Set.ext_iff.1 h₁ x).2 hx)]

Premises used: Iff.mpr, mt, Iff.mp, Set.ext_iff, Function.notMem_mulSupport
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f g : ι → M
h : mulSupport f = mulSupport g ∧ ∀ (x : ι), x ∈ mulSupport f → f x = g x
h₁ : mulSupport f = mulSupport g
h₂ : ∀ (x : ι), x ∈ mulSupport f → f x = g x
x : ι
if : ∀ (hx : x ∈ mulSupport f), f x = g x
if₁ : ∀ (hx : ¬x ∈ mulSupport f), f x = g x
if₂ : ∀ (hx : x ∈ mulSupport f), f x = g x
if₃ if₄ : ∀ (hx : ¬x ∈ mulSupport f), f x = g x
⊢ f x = g x

Tactic:
if hx : x ∈ f.mulSupport then exact h₂ x hx
    else rw [notMem_mulSupport.1 hx, notMem_mulSupport.1 (mt (Set.ext_iff.1 h₁ x).2 hx)]

Premises used: Function.mulSupport
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
inst_1 : DecidableEq ι
f : ι → M
x : ι
y : M
hy : y ≠ 1
h : ∀ (a : ι), a ∈ mulSupport (update (β := fun (a : ι) ↦ M) f x y) ↔ a ∈ insert x (mulSupport f)
⊢ mulSupport (update (β := fun (a : ι) ↦ M) f x y) = insert x (mulSupport f)

Tactic:
ext a
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
inst_1 : DecidableEq ι
f : ι → M
x : ι
y : M
hy : y ≠ 1
a : ι
h : a ∈ mulSupport (update (β := fun (a : ι) ↦ M) f a y) ↔ a ∈ insert a (mulSupport f)
h₁ : ∀ (hne : a ≠ x), a ∈ mulSupport (update (β := fun (a : ι) ↦ M) f x y) ↔ a ∈ insert x (mulSupport f)
⊢ a ∈ mulSupport (update (β := fun (a : ι) ↦ M) f x y) ↔ a ∈ insert x (mulSupport f)

Tactic:
obtain rfl | hne := eq_or_ne a x

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
inst_1 : DecidableEq ι
f : ι → M
y : M
hy : y ≠ 1
a : ι
⊢ a ∈ mulSupport (update (β := fun (a : ι) ↦ M) f a y) ↔ a ∈ insert a (mulSupport f)

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
inst_1 : DecidableEq ι
f : ι → M
x : ι
y : M
hy : y ≠ 1
a : ι
hne : a ≠ x
⊢ a ∈ mulSupport (update (β := fun (a : ι) ↦ M) f x y) ↔ a ∈ insert x (mulSupport f)

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
inst_1 : DecidableEq ι
f : ι → M
x : ι
h : ∀ (a : ι), a ∈ mulSupport (update (β := fun (a : ι) ↦ M) f x 1) ↔ a ∈ mulSupport f \ {x}
⊢ mulSupport (update (β := fun (a : ι) ↦ M) f x 1) = mulSupport f \ {x}

Tactic:
ext a
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
inst_1 : DecidableEq ι
f : ι → M
x a : ι
h : a ∈ mulSupport (update (β := fun (a : ι) ↦ M) f a 1) ↔ a ∈ mulSupport f \ {a}
h₁ : ∀ (hne : a ≠ x), a ∈ mulSupport (update (β := fun (a : ι) ↦ M) f x 1) ↔ a ∈ mulSupport f \ {x}
⊢ a ∈ mulSupport (update (β := fun (a : ι) ↦ M) f x 1) ↔ a ∈ mulSupport f \ {x}

Tactic:
obtain rfl | hne := eq_or_ne a x

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
inst_1 : DecidableEq ι
f : ι → M
a : ι
⊢ a ∈ mulSupport (update (β := fun (a : ι) ↦ M) f a 1) ↔ a ∈ mulSupport f \ {a}

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
inst_1 : DecidableEq ι
f : ι → M
x a : ι
hne : a ≠ x
⊢ a ∈ mulSupport (update (β := fun (a : ι) ↦ M) f x 1) ↔ a ∈ mulSupport f \ {x}

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
inst_1 : DecidableEq ι
inst_2 : DecidableEq M
f : ι → M
x : ι
y : M
inl :
  mulSupport (update (β := fun (a : ι) ↦ M) f x 1) =
    if Eq.{u_3 + 1} (α := M) 1 1 then mulSupport f \ {x} else insert x (mulSupport f)
inr :
  ∀ (hy : y ≠ 1),
    mulSupport (update (β := fun (a : ι) ↦ M) f x y) = if y = 1 then mulSupport f \ {x} else insert x (mulSupport f)
⊢ mulSupport (update (β := fun (a : ι) ↦ M) f x y) = if y = 1 then mulSupport f \ {x} else insert x (mulSupport f)

Tactic:
rcases eq_or_ne y 1 with rfl | hy

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
inst_1 : DecidableEq ι
inst_2 : DecidableEq M
f : ι → M
x : ι
⊢ mulSupport (update (β := fun (a : ι) ↦ M) f x 1) =
    if Eq.{u_3 + 1} (α := M) 1 1 then mulSupport f \ {x} else insert x (mulSupport f)

Tactic:
simp [mulSupport_update_one, mulSupport_update_of_ne_one, *]

Premises used: Function.mulSupport_update_one, Function.mulSupport_update_of_ne_one
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
inst_1 : DecidableEq ι
inst_2 : DecidableEq M
f : ι → M
x : ι
y : M
hy : y ≠ 1
⊢ mulSupport (update (β := fun (a : ι) ↦ M) f x y) = if y = 1 then mulSupport f \ {x} else insert x (mulSupport f)

Tactic:
simp [mulSupport_update_one, mulSupport_update_of_ne_one, *]

Premises used: Function.mulSupport_update_one, Function.mulSupport_update_of_ne_one
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
κ : Type u_2
N : Type u_4
inst : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
pos : ∀ (hf : ∃ (a : ι), f a = x), extend f g 1 x = 1
neg : ∀ (hf : ¬∃ (a : ι), f a = x), extend f g 1 x = 1
⊢ extend f g 1 x = 1

Tactic:
by_cases hf : ∃ a, f a = x
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
κ : Type u_2
N : Type u_4
inst : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
hf : ∃ (a : ι), f a = x
pos : ¬Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) hf ∈ mulSupport g
⊢ extend f g 1 x = 1

Tactic:
rw [extend, dif_pos hf, ← notMem_mulSupport]

Premises used: dif_pos, Function.extend, Function.notMem_mulSupport
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
κ : Type u_2
N : Type u_4
inst : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
hf : ∃ (a : ι), f a = x
⊢ ¬f (Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) hf) ∈ f '' mulSupport g

Tactic:
rw [← Classical.choose_spec hf] at hfg

Premises used: Classical.choose_spec
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
κ : Type u_2
N : Type u_4
inst : One N
f : ι → κ
g : ι → N
x : κ
hf : ∃ (a : ι), f a = x
hfg : ¬f (Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) hf) ∈ f '' mulSupport g
⊢ ¬Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) hf ∈ mulSupport g

Tactic:
fun hg ↦ hfg ⟨_, hg, rfl⟩

Premises used: And.intro, Exists.intro, Classical.choose, Not, rfl
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
κ : Type u_2
N : Type u_4
inst : One N
f : ι → κ
g : ι → N
x : κ
hf : ∃ (a : ι), f a = x
hfg : ¬f (Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) hf) ∈ f '' mulSupport g
⊢ ¬Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) hf ∈ mulSupport g

Tactic:
exact fun hg ↦ hfg ⟨_, hg, rfl⟩

Premises used: And.intro, Exists.intro, Classical.choose, rfl
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
κ : Type u_2
N : Type u_4
inst : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
hf : ¬∃ (a : ι), f a = x
neg : Eq.{u_4 + 1} (α := N) (1 x) 1
⊢ extend f g 1 x = 1

Tactic:
rw [extend_apply' _ _ _ hf]

Premises used: Function.extend_apply'