awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
f g : α → M
x : α
pos : x ∈ s → f x * g x = f x * g x
neg : ¬x ∈ s → 1 = HMul.hMul (α := M) 1 1
⊢ (if x ∈ s then f x * g x else 1) = (if x ∈ s then f x else 1) * if x ∈ s then g x else 1

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
f g : α → M
x : α
h : x ∈ s
⊢ f x * g x = f x * g x

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
f g : α → M
x : α
h : ¬x ∈ s
neg neg₁ : Eq.{u_4 + 1} (α := M) 1 1
⊢ 1 = HMul.hMul (α := M) 1 1

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
f g : α → M
⊢ s.mulIndicator (f * g) = s.mulIndicator f * s.mulIndicator g

Tactic:
mulIndicator_mul s f g

Premises used: Set.mulIndicator_mul
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
f : α → M
a : α
ha : a ∈ s
⊢ sᶜ.mulIndicator f a * s.mulIndicator f a = f a

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
f : α → M
a : α
ha : ¬a ∈ s
⊢ sᶜ.mulIndicator f a * s.mulIndicator f a = f a

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
f : α → M
⊢ sᶜ.mulIndicator f * s.mulIndicator f = f

Tactic:
funext <| mulIndicator_compl_mul_self_apply s f

Premises used: funext, Set.mulIndicator_compl_mul_self_apply
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
f : α → M
a : α
ha : a ∈ s
⊢ s.mulIndicator f a * sᶜ.mulIndicator f a = f a

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
f : α → M
a : α
ha : ¬a ∈ s
⊢ s.mulIndicator f a * sᶜ.mulIndicator f a = f a

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
f : α → M
⊢ s.mulIndicator f * sᶜ.mulIndicator f = f

Tactic:
funext <| mulIndicator_self_mul_compl_apply s f

Premises used: Set.mulIndicator_self_mul_compl_apply, funext
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
⊢ (mulSupport f).mulIndicator (f * g) = f

Tactic:
(mulIndicator_congr fun x hx => ?_).trans mulIndicator_mulSupport

Premises used: Set.mulIndicator_mulSupport, Set.mulIndicator_congr, Eq.trans
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
refine : ∀ (x : α) (hx : x ∈ mulSupport f), (f * g) x = f x
⊢ (mulSupport f).mulIndicator (f * g) = f

Tactic:
refine (mulIndicator_congr fun x hx => ?_).trans mulIndicator_mulSupport

Premises used: Set.mulIndicator_mulSupport, Set.mulIndicator_congr, Eq.trans
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport f
⊢ g x = 1

Tactic:
have : g x = 1 := notMem_mulSupport.1 (disjoint_left.1 h hx)
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport f
this : g x = 1
rw : f x * g x = f x
rw₁ : f x * 1 = f x
rw₂ rw₃ : f x = f x
⊢ (f * g) x = f x

Tactic:
rw [Pi.mul_apply, this, mul_one]

Premises used: Pi.mul_apply, mul_one
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
⊢ (mulSupport g).mulIndicator (f * g) = g

Tactic:
(mulIndicator_congr fun x hx => ?_).trans mulIndicator_mulSupport

Premises used: Set.mulIndicator_mulSupport, Set.mulIndicator_congr, Eq.trans
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
refine : ∀ (x : α) (hx : x ∈ mulSupport g), (f * g) x = g x
⊢ (mulSupport g).mulIndicator (f * g) = g

Tactic:
refine (mulIndicator_congr fun x hx => ?_).trans mulIndicator_mulSupport

Premises used: Set.mulIndicator_mulSupport, Set.mulIndicator_congr, Eq.trans
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport g
⊢ f x = 1

Tactic:
have : f x = 1 := notMem_mulSupport.1 (disjoint_right.1 h hx)
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport g
this : f x = 1
rw : f x * g x = g x
rw₁ : 1 * g x = g x
rw₂ rw₃ : g x = g x
⊢ (f * g) x = g x

Tactic:
rw [Pi.mul_apply, this, one_mul]

Premises used: Pi.mul_apply, one_mul
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
f g : α → M
h : ∀ (x : α), (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise (β := fun (i : α) ↦ M) f g x
⊢ s.mulIndicator f * sᶜ.mulIndicator g = s.piecewise (β := fun (i : α) ↦ M) f g

Tactic:
ext x
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
f g : α → M
x : α
pos : ∀ (h : x ∈ s), (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise (β := fun (i : α) ↦ M) f g x
neg : ∀ (h : ¬x ∈ s), (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise (β := fun (i : α) ↦ M) f g x
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise (β := fun (i : α) ↦ M) f g x

Tactic:
by_cases h : x ∈ s
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
f g : α → M
x : α
h : x ∈ s
pos : (s.mulIndicator f * sᶜ.mulIndicator g) x = f x
pos₁ : s.mulIndicator f x * sᶜ.mulIndicator g x = f x
pos₂ : f x * sᶜ.mulIndicator g x = f x
pos₃ : f x * 1 = f x
pos₄ pos₅ : f x = f x
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise (β := fun (i : α) ↦ M) f g x

Tactic:
rw [piecewise_eq_of_mem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_mem h,
      Set.mulIndicator_of_notMem (Set.notMem_compl_iff.2 h), mul_one]

Premises used: Iff.mpr, Pi.mul_apply, Set.mulIndicator_of_notMem, Set.piecewise_eq_of_mem, Set.notMem_compl_iff, mul_one, Set.mulIndicator_of_mem
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_4
inst : MulOneClass M
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
f g : α → M
x : α
h : ¬x ∈ s
neg : (s.mulIndicator f * sᶜ.mulIndicator g) x = g x
neg₁ : s.mulIndicator f x * sᶜ.mulIndicator g x = g x
neg₂ : 1 * sᶜ.mulIndicator g x = g x
neg₃ : 1 * g x = g x
neg₄ neg₅ : g x = g x
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise (β := fun (i : α) ↦ M) f g x

Tactic:
rw [piecewise_eq_of_notMem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_notMem h,
      Set.mulIndicator_of_mem (Set.mem_compl h), one_mul]

Premises used: Pi.mul_apply, Set.piecewise_eq_of_notMem, Set.mulIndicator_of_notMem, Set.mulIndicator_of_mem, one_mul, Set.mem_compl
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
G : Type u_6
inst : Group G
s : Set α
f : α → G
⊢ s.mulIndicator f⁻¹ = (s.mulIndicator f)⁻¹

Tactic:
(mulIndicatorHom G s).map_inv f

Premises used: Set.mulIndicatorHom, Set.mulIndicator, MonoidHom.map_inv, ite
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
G : Type u_6
inst : Group G
s : Set α
f : α → G
⊢ Eq (α := (x : α) → G) (s.mulIndicator fun (a : α) ↦ (f a)⁻¹) fun (a : α) ↦ (s.mulIndicator f a)⁻¹

Tactic:
mulIndicator_inv' s f

Premises used: Set.mulIndicator_inv'
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
G : Type u_6
inst : Group G
s : Set α
f g : α → G
⊢ Eq (α := (x : α) → G) (s.mulIndicator fun (a : α) ↦ f a / g a) fun (a : α) ↦ s.mulIndicator f a / s.mulIndicator g a

Tactic:
(mulIndicatorHom G s).map_div f g

Premises used: Set.mulIndicatorHom, Set.mulIndicator, MonoidHom.map_div, ite
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
G : Type u_6
inst : Group G
s : Set α
f g : α → G
⊢ s.mulIndicator (f / g) = s.mulIndicator f / s.mulIndicator g

Tactic:
mulIndicator_div s f g

Premises used: Set.mulIndicator_div
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
G : Type u_6
inst : Group G
s : Set α
f : α → G
⊢ sᶜ.mulIndicator f = f * (s.mulIndicator f)⁻¹

Tactic:
eq_mul_inv_of_mul_eq <| s.mulIndicator_compl_mul_self f

Premises used: eq_mul_inv_of_mul_eq, Set.mulIndicator_compl_mul_self
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
G : Type u_6
inst : Group G
s : Set α
f : α → G
rw : sᶜ.mulIndicator f = f * (s.mulIndicator f)⁻¹
rw₁ rw₂ : f * (s.mulIndicator f)⁻¹ = f * (s.mulIndicator f)⁻¹
⊢ sᶜ.mulIndicator f = f / s.mulIndicator f

Tactic:
rw [div_eq_mul_inv, mulIndicator_compl]

Premises used: div_eq_mul_inv, Set.mulIndicator_compl
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
G : Type u_6
inst : Group G
s t : Set α
h : s ⊆ t
f : α → G
h₁ : Disjoint (t \ s) s
⊢ (t \ s).mulIndicator f * s.mulIndicator f = t.mulIndicator f

Tactic:
rw [Pi.mul_def, ← mulIndicator_union_of_disjoint, diff_union_self,
      union_eq_self_of_subset_right h]

Premises used: Set.union_eq_self_of_subset_right, Set.diff_union_self, Set.mulIndicator_union_of_disjoint, Pi.mul_def
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
G : Type u_6
inst : Group G
s t : Set α
h : s ⊆ t
f : α → G
⊢ Disjoint (t \ s) s

Tactic:
disjoint_sdiff_self_left

Premises used: disjoint_sdiff_self_left
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
G : Type u_6
inst : Group G
s t : Set α
h : s ⊆ t
f : α → G
⊢ Disjoint (t \ s) s

Tactic:
exact disjoint_sdiff_self_left

Premises used: disjoint_sdiff_self_left
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
G : Type u_6
inst : Group G
s t : Set α
h : s ⊆ t
f : α → G
rw : t.mulIndicator f * (s.mulIndicator f)⁻¹ = t.mulIndicator f / s.mulIndicator f
rw₁ rw₂ : t.mulIndicator f * (s.mulIndicator f)⁻¹ = t.mulIndicator f * (s.mulIndicator f)⁻¹
⊢ (t \ s).mulIndicator f = t.mulIndicator f / s.mulIndicator f

Tactic:
rw [mulIndicator_diff h, div_eq_mul_inv]

Premises used: div_eq_mul_inv, Set.mulIndicator_diff
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
β : Type u_2
G : Type u_6
inst : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
pos : ∀ (hs : x ∈ s), g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
neg : ∀ (hs : ¬x ∈ s), g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)

Tactic:
by_cases hs : x ∈ s
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
β : Type u_2
G : Type u_6
inst : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
hs : x ∈ s
pos : ∀ (ht : x ∈ t), g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
neg : ∀ (ht : ¬x ∈ t), g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)

Tactic:
by_cases ht : x ∈ t
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
β : Type u_2
G : Type u_6
inst : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
hs : ¬x ∈ s
pos : ∀ (ht : x ∈ t), g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
neg : ∀ (ht : ¬x ∈ t), g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)

Tactic:
by_cases ht : x ∈ t
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
β : Type u_2
G : Type u_6
inst : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
hs : x ∈ s
ht : x ∈ t
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)

Tactic:
simp [mem_symmDiff, *]

Premises used: Set.mem_symmDiff
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
β : Type u_2
G : Type u_6
inst : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
hs : x ∈ s
ht : ¬x ∈ t
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)

Tactic:
simp [mem_symmDiff, *]

Premises used: Set.mem_symmDiff
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
β : Type u_2
G : Type u_6
inst : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
hs : ¬x ∈ s
ht : x ∈ t
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)

Tactic:
simp [mem_symmDiff, *]

Premises used: Set.mem_symmDiff
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
β : Type u_2
G : Type u_6
inst : Group G
g : G → β
hg : ∀ (x : G), g x⁻¹ = g x
s t : Set α
f : α → G
x : α
hs : ¬x ∈ s
ht : ¬x ∈ t
⊢ g ((s ∆ t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)

Tactic:
simp [mem_symmDiff, *]

Premises used: Set.mem_symmDiff
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : One β
s : γ → Set α
f : α → β
hs : Pairwise.{u_3} (α := γ) (onFun.{u_3 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (j : γ) ↦ s j ∩ mulSupport f)
i : α
j : γ
hj : i ∈ s j
this : ∀ (j' : γ), j' ≠ j → {i} ⊆ s j → {i} ⊆ s j' → {i} ⊆ mulSupport f → False
by_contra :
  ∀ (this : ¬Subset (α := Set γ) (mulSupport.{u_3, u_2} (M := β) fun (d : γ) ↦ (s d).mulIndicator f i) {j}), False
⊢ Subset (α := Set γ) (mulSupport.{u_3, u_2} (M := β) fun (d : γ) ↦ (s d).mulIndicator f i) {j}

Tactic:
by_contra
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : One β
s : γ → Set α
f : α → β
hs : Pairwise.{u_3} (α := γ) (onFun.{u_3 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (j : γ) ↦ s j ∩ mulSupport f)
i : α
j : γ
hj : i ∈ s j
this_1 : ∀ (j' : γ), j' ≠ j → {i} ⊆ s j → {i} ⊆ s j' → {i} ⊆ mulSupport f → False
this : ¬Subset (α := Set γ) (mulSupport.{u_3, u_2} (M := β) fun (d : γ) ↦ (s d).mulIndicator f i) {j}
⊢ False

Tactic:
aesop
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : One β
s : γ → Set α
f : α → β
hs : Pairwise.{u_3} (α := γ) (onFun.{u_3 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (j : γ) ↦ s j ∩ mulSupport f)
i : α
j : γ
hj : i ∈ s j
suffices : ∀ (j' : γ), j' ≠ j → {i} ⊆ s j → {i} ⊆ s j' → {i} ⊆ mulSupport f → False
⊢ Subset (α := Set γ) (mulSupport.{u_3, u_2} (M := β) fun (d : γ) ↦ (s d).mulIndicator f i) {j}

Tactic:
suffices ∀ j', j' ≠ j → {i} ⊆ s j → {i} ⊆ s j' → {i} ⊆ mulSupport f → False by by_contra; aesop
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : One β
s : γ → Set α
f : α → β
hs : Pairwise.{u_3} (α := γ) (onFun.{u_3 + 1, u_1 + 1, 1} (β := Set α) Disjoint fun (j : γ) ↦ s j ∩ mulSupport f)
i : α
j : γ
hj_1 : i ∈ s j
j' : γ
h : j' ≠ j
hj : {i} ⊆ s j
hj' : {i} ⊆ s j'
hi : {i} ⊆ mulSupport f
⊢ ∀ ⦃i j : γ⦄, i ≠ j → ∀ ⦃x : Set α⦄, x ⊆ s i ∧ x ⊆ mulSupport f → x ⊆ s j ∧ x ⊆ mulSupport f → x ⊆ ⊥

Tactic:
simp only [Pairwise, Disjoint, Set.le_eq_subset, Set.subset_inter_iff] at hs

Premises used: Set.subset_inter_iff, Set.le_eq_subset, Disjoint, Pairwise
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : One β
s : γ → Set α
f : α → β
i : α
j : γ
hj_1 : i ∈ s j
j' : γ
h : j' ≠ j
hj : {i} ⊆ s j
hj' : {i} ⊆ s j'
hi : {i} ⊆ mulSupport f
hs : ∀ ⦃i j : γ⦄, i ≠ j → ∀ ⦃x : Set α⦄, x ⊆ s i ∧ x ⊆ mulSupport f → x ⊆ s j ∧ x ⊆ mulSupport f → x ⊆ ⊥
⊢ False

Tactic:
simpa using hs h ⟨hj', hi⟩ ⟨hj, hi⟩

Premises used: And.intro
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
ι : Type u_6
inst : DecidableEq ι
M : Type u_7
inst_1 : One M
i : ι
f : ι → M
h : ∀ (j : ι), mulIndicator {i} f j = Pi.mulSingle (M := fun (j : ι) ↦ M) i (f i) j
⊢ mulIndicator {i} f = Pi.mulSingle (M := fun (j : ι) ↦ M) i (f i)

Tactic:
ext j
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
ι : Type u_6
inst : DecidableEq ι
M : Type u_7
inst_1 : One M
i : ι
f : ι → M
j : ι
h : (if j = i then f j else 1) = if j = i then f i else 1
⊢ mulIndicator {i} f j = Pi.mulSingle (M := fun (j : ι) ↦ M) i (f i) j

Tactic:
simp only [Set.mulIndicator_apply, Pi.mulSingle_apply, Set.mem_singleton_iff]

Premises used: Set.mulIndicator_apply, Set.mem_singleton_iff, Pi.mulSingle_apply
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
ι : Type u_6
inst : DecidableEq ι
M : Type u_7
inst_1 : One M
i : ι
f : ι → M
j : ι
pos : ∀ (h : j = i), f j = f i
neg : ∀ (h : ¬j = i), Eq.{u_7 + 1} (α := M) 1 1
⊢ (if j = i then f j else 1) = if j = i then f i else 1

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
ι : Type u_6
inst : DecidableEq ι
M : Type u_7
inst_1 : One M
i : ι
f : ι → M
j : ι
h : j = i
⊢ f j = f i

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
ι : Type u_6
inst : DecidableEq ι
M : Type u_7
inst_1 : One M
i : ι
f : ι → M
j : ι
h : ¬j = i
⊢ Eq.{u_7 + 1} (α := M) 1 1

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Group.Indicator
Goal:
α : Type u_1
M : Type u_6
N : Type u_7
F : Type u_8
inst : One M
inst_1 : One N
inst_2 : FunLike F M N
inst_3 : OneHomClass F M N
f : F
s : Set α
g : α → M
x : α
⊢ Eq.{u_7 + 1} (α := N) ((f : (a : M) → N) (s.mulIndicator g x) : N) (s.mulIndicator ((⇑f : (a : M) → N) ∘ g) x : N)

Tactic:
simp [Set.mulIndicator_comp_of_one]

Premises used: Set.mulIndicator_comp_of_one
-- Module: Mathlib.Algebra.Group.InjSurj
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : Semigroup M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y z : M₁
rw : f (x * y) * f z = f (x * (y * z))
rw₁ : f x * f y * f z = f (x * (y * z))
rw₂ : f x * f y * f z = f x * f (y * z)
rw₃ : f x * f y * f z = f x * (f y * f z)
rw₄ rw₅ : f x * (f y * f z) = f x * (f y * f z)
⊢ f (x * y * z) = f (x * (y * z))

Tactic:
rw [mul, mul, mul, mul, mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Group.InjSurj
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : CommMagma M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y : M₁
rw : f x * f y = f (y * x)
rw₁ : f x * f y = f y * f x
rw₂ rw₃ : f y * f x = f y * f x
⊢ f (x * y) = f (y * x)

Tactic:
rw [mul, mul, mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Group.InjSurj
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : Mul M₂
inst_2 : IsLeftCancelMul M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y z : M₁
H : Eq.{u_1 + 1} (α := M₁) ((fun (x_1 : M₁) ↦ x * x_1) y) ((fun (x_1 : M₁) ↦ x * x_1) z)
⊢ f x * f y = f x * f z

Tactic:
simpa only [mul] using congrArg f H

Premises used: congrArg
-- Module: Mathlib.Algebra.Group.InjSurj
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : Mul M₂
inst_2 : IsRightCancelMul M₂
f : M₁ → M₂
hf : Injective f
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x y z : M₁
H : Eq.{u_1 + 1} (α := M₁) ((fun (x_1 : M₁) ↦ x_1 * x) y) ((fun (x_1 : M₁) ↦ x_1 * x) z)
⊢ f y * f x = f z * f x

Tactic:
simpa only [mul] using congrArg f H

Premises used: congrArg
-- Module: Mathlib.Algebra.Group.InjSurj
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : One M₁
inst_2 : MulOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
rw : f 1 * f x = f x
rw₁ : 1 * f x = f x
rw₂ rw₃ : f x = f x
⊢ f (1 * x) = f x

Tactic:
rw [mul, one, one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.Group.InjSurj
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : One M₁
inst_2 : MulOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
x : M₁
rw : f x * f 1 = f x
rw₁ : f x * 1 = f x
rw₂ rw₃ : f x = f x
⊢ f (x * 1) = f x

Tactic:
rw [mul, one, mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.Group.InjSurj
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : One M₁
inst_2 : Pow M₁ ℕ
inst_3 : Monoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
x : M₁
rw : HPow.hPow (β := ℕ) (f x) 0 = f 1
rw₁ : HPow.hPow (β := ℕ) (f x) 0 = 1
rw₂ rw₃ : Eq.{u_2 + 1} (α := M₂) 1 1
⊢ f (HPow.hPow (β := ℕ) x 0) = f 1

Tactic:
rw [npow, one, pow_zero]

Premises used: pow_zero
-- Module: Mathlib.Algebra.Group.InjSurj
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : One M₁
inst_2 : Pow M₁ ℕ
inst_3 : Monoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
rw : f x ^ (n + 1) = f (x ^ n * x)
rw₁ : f x ^ n * f x = f (x ^ n * x)
rw₂ : f x ^ n * f x = f (x ^ n) * f x
rw₃ rw₄ : f x ^ n * f x = f x ^ n * f x
⊢ f (x ^ (n + 1)) = f (x ^ n * x)

Tactic:
rw [npow, pow_succ, mul, npow]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Group.InjSurj
Goal:
M₁_1 : Type u_1
M₂ : Type u_2
inst : Mul M₁_1
inst_1 : One M₁_1
inst_2 : Pow M₁_1 ℕ
M₁ : Type u_3
inst_3 : Inv M₁
inst_4 : InvolutiveInv M₂
f : M₁ → M₂
hf : Injective f
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
x : M₁
rw : (f x⁻¹)⁻¹ = f x
rw₁ : (f x)⁻¹⁻¹ = f x
rw₂ rw₃ : f x = f x
⊢ f x⁻¹⁻¹ = f x

Tactic:
rw [inv, inv, inv_inv]

Premises used: inv_inv
-- Module: Mathlib.Algebra.Group.InjSurj
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : One M₁
inst_2 : Pow M₁ ℕ
inst_3 : Inv M₁
inst_4 : InvOneClass M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
rw : (f 1)⁻¹ = f 1
rw₁ : Eq.{u_2 + 1} (α := M₂) 1⁻¹ 1
rw₂ rw₃ : Eq.{u_2 + 1} (α := M₂) 1 1
⊢ f 1⁻¹ = f 1

Tactic:
rw [inv, one, inv_one]

Premises used: inv_one
-- Module: Mathlib.Algebra.Group.InjSurj
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : One M₁
inst_2 : Pow M₁ ℕ
inst_3 : Inv M₁
inst_4 : Div M₁
inst_5 : Pow M₁ ℤ
inst_6 : DivInvMonoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x y : M₁
rw : f x / f y = f (x * y⁻¹)
rw₁ : f x / f y = f x * f y⁻¹
rw₂ : f x / f y = f x * (f y)⁻¹
rw₃ rw₄ : f x * (f y)⁻¹ = f x * (f y)⁻¹
⊢ f (x / y) = f (x * y⁻¹)

Tactic:
rw [div, mul, inv, div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Group.InjSurj
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : One M₁
inst_2 : Pow M₁ ℕ
inst_3 : Inv M₁
inst_4 : Div M₁
inst_5 : Pow M₁ ℤ
inst_6 : DivInvMonoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
x : M₁
rw : HPow.hPow (β := ℤ) (f x) 0 = f 1
rw₁ : 1 = f 1
rw₂ rw₃ : Eq.{u_2 + 1} (α := M₂) 1 1
⊢ f (HPow.hPow (β := ℤ) x 0) = f 1

Tactic:
rw [zpow, zpow_zero, one]

Premises used: zpow_zero
-- Module: Mathlib.Algebra.Group.InjSurj
Goal:
M₁ : Type u_1
M₂ : Type u_2
inst : Mul M₁
inst_1 : One M₁
inst_2 : Pow M₁ ℕ
inst_3 : Inv M₁
inst_4 : Div M₁
inst_5 : Pow M₁ ℤ
inst_6 : DivInvMonoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : M₁), f (x / y) = f x / f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n
n : ℕ
x : M₁
rw : HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ) = f (HPow.hPow (β := ℤ) x (↑n : ℤ) * x)
rw₁ : HPow.hPow (β := ℤ) (f x) (↑n.succ : ℤ) = f (HPow.hPow (β := ℤ) x (↑n : ℤ)) * f x
rw₂ : f x ^ n.succ = f (HPow.hPow (β := ℤ) x (↑n : ℤ)) * f x
rw₃ : f x ^ n * f x = f (HPow.hPow (β := ℤ) x (↑n : ℤ)) * f x
rw₄ : f x ^ n * f x = HPow.hPow (β := ℤ) (f x) (↑n : ℤ) * f x
rw₅ rw₆ : f x ^ n * f x = f x ^ n * f x
⊢ f (HPow.hPow (β := ℤ) x (↑n.succ : ℤ)) = f (HPow.hPow (β := ℤ) x (↑n : ℤ) * x)

Tactic:
rw [zpow, mul, zpow_natCast, pow_succ, zpow, zpow_natCast]

Premises used: zpow_natCast, pow_succ