awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
M : Type u_5
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst_9 : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
hg : g.ker = ⊥
rw : Submodule.comap f g.ker = f.ker
rw₁ : Submodule.comap f ⊥ = f.ker
rw₂ rw₃ : f.ker = f.ker
⊢ (g ∘ₛₗ f).ker = f.ker

Tactic:
rw [ker_comp, hg, Submodule.comap_bot]

Premises used: LinearMap.ker_comp, Submodule.comap_bot
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_11
S : Type u_12
M : Type u_13
N : Type u_14
inst : Semiring R
inst_1 : Semiring S
inst_2 : SMul R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : Module S N
inst_10 : IsScalarTower R S N
f : M →ₗ[S] N
⊢ Eq (α := Submodule R M)
    (ker
      ((↑R :
          {S : Type u_12} →
            {M : Type u_13} →
              {M₂ : Type u_14} →
                [inst : Semiring R] →
                  [inst_11 : Semiring S] →
                    [inst_12 : AddCommMonoid M] →
                      [inst_13 : AddCommMonoid M₂] →
                        [inst_14 : Module R M] →
                          [inst_15 : Module R M₂] →
                            [inst_16 : Module S M] →
                              [inst_17 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        f))
    (Submodule.restrictScalars R f.ker)

Tactic:
rfl

Premises used: Set.Mem, Submodule.restrictScalars, LinearMap.ker, setOf, Submodule.comap, Set.preimage, Set.singleton, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
e : M ≃ₛₗ[σ₁₂] M₂
⊢ (↑e : M →ₛₗ[σ₁₂] M₂).ker = ⊥

Tactic:
LinearMap.ker_eq_bot_of_injective e.toEquiv.injective

Premises used: LinearEquiv.toEquiv, LinearMap.ker_eq_bot_of_injective, Equiv.injective
-- Module: Mathlib.Algebra.Module.Submodule.Ker
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
M : Type u_5
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M : Module R M
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
σ₃₂ : R₃ →+* R₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
e'' : M₂ ≃ₛₗ[σ₂₃] M₃
l : M →ₛₗ[σ₁₂] M₂
⊢ ((↑e'' : M₂ →ₛₗ[σ₂₃] M₃) ∘ₛₗ l).ker = l.ker

Tactic:
LinearMap.ker_comp_of_ker_eq_bot _ e''.ker

Premises used: LinearMap.ker_comp_of_ker_eq_bot, LinearEquiv.ker
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f : α → M
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
⊢ s.piecewise (β := fun (i : α) ↦ M) f 1 = s.mulIndicator f

Tactic:
funext fun _ => @if_congr _ _ _ _ (id _) _ _ _ _ Iff.rfl rfl rfl

Premises used: Iff.rfl, if_congr, funext, rfl
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f : α → M
a : α
inst_1 : Decidable (a ∈ s)
⊢ (if a ∈ s then f a else 1) = if a ∈ s then f a else 1

Tactic:
congr
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
a : α
h : a ∈ s
f : α → M
⊢ s.mulIndicator f a = f a

Tactic:
if_pos h

Premises used: Set.mulIndicator, if_pos
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
a : α
h : ¬a ∈ s
f : α → M
⊢ s.mulIndicator f a = 1

Tactic:
if_neg h

Premises used: Set.mulIndicator, if_neg
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f : α → M
a : α
pos : ∀ (h : a ∈ s), s.mulIndicator f a = 1 ∨ s.mulIndicator f a = f a
neg : ∀ (h : ¬a ∈ s), s.mulIndicator f a = 1 ∨ s.mulIndicator f a = f a
⊢ s.mulIndicator f a = 1 ∨ s.mulIndicator f a = f a

Tactic:
by_cases h : a ∈ s
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f : α → M
a : α
h : a ∈ s
⊢ s.mulIndicator f a = 1 ∨ s.mulIndicator f a = f a

Tactic:
Or.inr (mulIndicator_of_mem h f)

Premises used: Set.mulIndicator_of_mem, Or.inr
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f : α → M
a : α
h : a ∈ s
⊢ s.mulIndicator f a = 1 ∨ s.mulIndicator f a = f a

Tactic:
exact Or.inr (mulIndicator_of_mem h f)

Premises used: Set.mulIndicator_of_mem, Or.inr
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f : α → M
a : α
h : ¬a ∈ s
⊢ s.mulIndicator f a = 1 ∨ s.mulIndicator f a = f a

Tactic:
Or.inl (mulIndicator_of_notMem h f)

Premises used: Set.mulIndicator_of_notMem, Or.inl
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f : α → M
a : α
h : ¬a ∈ s
⊢ s.mulIndicator f a = 1 ∨ s.mulIndicator f a = f a

Tactic:
exact Or.inl (mulIndicator_of_notMem h f)

Premises used: Set.mulIndicator_of_notMem, Or.inl
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f : α → M
a : α
this : Decidable (a ∈ s) := Classical.dec (a ∈ s)
rw rw₁ : ¬a ∈ s → 1 = f a ↔ ¬a ∈ s → 1 = f a
⊢ ¬a ∈ s → 1 = f a ↔ ¬a ∈ s → f a = 1

Tactic:
rw [@eq_comm _ (f a)]

Premises used: eq_comm
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f : α → M
⊢ s.mulIndicator f = f ↔ mulSupport f ⊆ s

Tactic:
simp only [funext_iff, subset_def, mem_mulSupport, mulIndicator_apply_eq_self, not_imp_comm]

Premises used: Set.subset_def, not_imp_comm, funext_iff, Function.mem_mulSupport, Set.mulIndicator_apply_eq_self
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s t : Set α
f : α → M
h1 : s.mulIndicator f = f
h2 : s ⊆ t
rw : ∀ (h1 : mulSupport f ⊆ s) (h2 : s ⊆ t), mulSupport f ⊆ t
⊢ t.mulIndicator f = f

Tactic:
rw [mulIndicator_eq_self] at h1 ⊢

Premises used: Set.mulIndicator_eq_self
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s t : Set α
f : α → M
h1 : mulSupport f ⊆ s
h2 : s ⊆ t
⊢ mulSupport f ⊆ t

Tactic:
Subset.trans h1 h2

Premises used: Set.Subset.trans
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s t : Set α
f : α → M
h1 : mulSupport f ⊆ s
h2 : s ⊆ t
⊢ mulSupport f ⊆ t

Tactic:
exact Subset.trans h1 h2

Premises used: Set.Subset.trans
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f : α → M
a : α
⊢ s.mulIndicator f a = 1 ↔ a ∈ s → f a = 1

Tactic:
letI := Classical.dec (a ∈ s)
  ite_eq_right_iff

Premises used: Set.mulIndicator, ite_eq_right_iff
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f : α → M
⊢ (s.mulIndicator f = fun (x : α) ↦ 1) ↔ Disjoint (mulSupport f) s

Tactic:
simp only [funext_iff, mulIndicator_apply_eq_one, Set.disjoint_left, mem_mulSupport,
    not_imp_not]

Premises used: Set.mulIndicator_apply_eq_one, Set.disjoint_left, funext_iff, Function.mem_mulSupport, not_imp_not
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f : α → M
⊢ s.mulIndicator f = 1 ↔ Disjoint (mulSupport f) s

Tactic:
mulIndicator_eq_one

Premises used: Set.mulIndicator_eq_one
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f : α → M
a : α
⊢ s.mulIndicator f a ≠ 1 ↔ a ∈ s ∩ mulSupport f

Tactic:
simp only [Ne, mulIndicator_apply_eq_one, Classical.not_imp, mem_inter_iff, mem_mulSupport]

Premises used: Set.mulIndicator_apply_eq_one, Set.mem_inter_iff, Function.mem_mulSupport, Ne, Classical.not_imp
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f : α → M
x : α
⊢ x ∈ mulSupport (s.mulIndicator f) ↔ x ∈ s ∩ mulSupport f

Tactic:
simp [Function.mem_mulSupport, mulIndicator_apply_eq_one]

Premises used: Set.mulIndicator_apply_eq_one, Function.mem_mulSupport
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f : α → M
a : α
h : s.mulIndicator f a ≠ 1
⊢ a ∈ s

Tactic:
not_imp_comm.1 (fun hn => mulIndicator_of_notMem hn f) h

Premises used: not_imp_comm, Set.mulIndicator_of_notMem, Iff.mp
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f : α → M
⊢ EqOn (s.mulIndicator f) f s

Tactic:
fun _ hx => mulIndicator_of_mem hx f

Premises used: Set.EqOn, Set.mulIndicator_of_mem
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f : α → M
⊢ EqOn (s.mulIndicator f) 1 sᶜ

Tactic:
fun _ hx => mulIndicator_of_notMem hx f

Premises used: Set.mulIndicator_of_notMem, Set.EqOn
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f : α → M
⊢ mulSupport (s.mulIndicator f) ⊆ s

Tactic:
fun _ hx =>
  hx.imp_symm fun h => mulIndicator_of_notMem h f

Premises used: Set.mulIndicator_of_notMem, Not.imp_symm, Set.Subset
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
f : α → M
⊢ (mulSupport f).mulIndicator f = f

Tactic:
mulIndicator_eq_self.2 Subset.rfl

Premises used: Iff.mpr, Set.Subset.rfl, Set.mulIndicator_eq_self
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
ι : Sort u_5
f : ι → α
g : α → M
⊢ (range f).mulIndicator g ∘ f = g ∘ f

Tactic:
letI := Classical.decPred (· ∈ range f)
  piecewise_range_comp _ _ _

Premises used: Set.piecewise_range_comp, Set.mulIndicator, OfNat.ofNat
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f g : α → M
h : EqOn f g s
x : α
pos : ∀ (h_1 : x ∈ s), f x = g x
neg : ∀ (h_1 : ¬x ∈ s), Eq.{u_3 + 1} (α := M) 1 1
⊢ (if x ∈ s then f x else 1) = if x ∈ s then g x else 1

Tactic:
split_ifs with h_1
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f g : α → M
h : EqOn f g s
x : α
h_1 : x ∈ s
⊢ f x = g x

Tactic:
h h_1
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f g : α → M
h : EqOn f g s
x : α
h_1 : x ∈ s
⊢ f x = g x

Tactic:
exact h h_1
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f g : α → M
h : EqOn f g s
x : α
h_1 : ¬x ∈ s
⊢ Eq.{u_3 + 1} (α := M) 1 1

Tactic:
rfl
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : One M
s : Set α
f : α → M
a : α
t : Set β
g : β → M
b : β
h1 : a ∈ s ↔ b ∈ t
h2 : f a = g b
pos : a ∈ s → s.mulIndicator f a = t.mulIndicator g b
neg : ¬a ∈ s → s.mulIndicator f a = t.mulIndicator g b
⊢ s.mulIndicator f a = t.mulIndicator g b

Tactic:
by_cases a ∈ s
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : One M
s : Set α
f : α → M
a : α
t : Set β
g : β → M
b : β
h1 : a ∈ s ↔ b ∈ t
h2 : f a = g b
h : a ∈ s
⊢ s.mulIndicator f a = t.mulIndicator g b

Tactic:
simp_all
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : One M
s : Set α
f : α → M
a : α
t : Set β
g : β → M
b : β
h1 : a ∈ s ↔ b ∈ t
h2 : f a = g b
h : ¬a ∈ s
⊢ s.mulIndicator f a = t.mulIndicator g b

Tactic:
simp_all
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : One M
s : Set α
a : α
t : Set β
b : β
c : M
h : a ∈ s ↔ b ∈ t
⊢ Eq.{u_3 + 1} (α := M) (s.mulIndicator (fun (x : α) ↦ c) a) (t.mulIndicator (fun (x : β) ↦ c) b)

Tactic:
mulIndicator_eq_mulIndicator h rfl

Premises used: Set.mulIndicator_eq_mulIndicator, rfl
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
f : α → M
⊢ mulIndicator univ f = f

Tactic:
mulIndicator_eq_self.2 <| subset_univ _

Premises used: Iff.mpr, Set.subset_univ, Set.mulIndicator_eq_self
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
f : α → M
⊢ mulIndicator ∅ f = fun (x : α) ↦ 1

Tactic:
mulIndicator_eq_one.2 <| disjoint_empty _

Premises used: Iff.mpr, Set.disjoint_empty, Set.mulIndicator_eq_one
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
f : α → M
⊢ mulIndicator ∅ f = 1

Tactic:
mulIndicator_empty f

Premises used: Set.mulIndicator_empty
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
⊢ Disjoint (mulSupport.{u_1, u_3} (M := M) fun (x : α) ↦ 1) s

Tactic:
simp only [mulSupport_fun_one, empty_disjoint]

Premises used: Function.mulSupport_fun_one, Set.empty_disjoint
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
⊢ Eq (α := (x : α) → M) (s.mulIndicator 1) 1

Tactic:
mulIndicator_one M s

Premises used: Set.mulIndicator_one
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s t : Set α
f : α → M
x : α
pos : x ∈ s → x ∈ t → x ∈ s ∩ t → f x = f x
neg : x ∈ s → x ∈ t → ¬x ∈ s ∩ t → f x = 1
pos₁ : x ∈ s → ¬x ∈ t → x ∈ s ∩ t → 1 = f x
neg₁ : x ∈ s → ¬x ∈ t → ¬x ∈ s ∩ t → Eq.{u_3 + 1} (α := M) 1 1
pos₂ : ¬x ∈ s → x ∈ s ∩ t → 1 = f x
neg₂ : ¬x ∈ s → ¬x ∈ s ∩ t → Eq.{u_3 + 1} (α := M) 1 1
⊢ (if x ∈ s then if x ∈ t then f x else 1 else 1) = if x ∈ s ∩ t then f x else 1

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s t : Set α
f : α → M
x : α
h : x ∈ s
h_1 : x ∈ t
h_2 : x ∈ s ∩ t
⊢ f x = f x

Tactic:
simp_all +contextual
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s t : Set α
f : α → M
x : α
h : x ∈ s
h_1 : x ∈ t
h_2 : ¬x ∈ s ∩ t
⊢ f x = 1

Tactic:
simp_all +contextual
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s t : Set α
f : α → M
x : α
h : x ∈ s
h_1 : ¬x ∈ t
h_2 : x ∈ s ∩ t
⊢ 1 = f x

Tactic:
simp_all +contextual
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s t : Set α
f : α → M
x : α
h : x ∈ s
h_1 : ¬x ∈ t
h_2 : ¬x ∈ s ∩ t
⊢ Eq.{u_3 + 1} (α := M) 1 1

Tactic:
simp_all +contextual
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s t : Set α
f : α → M
x : α
h : ¬x ∈ s
h_1 : x ∈ s ∩ t
⊢ 1 = f x

Tactic:
simp_all +contextual
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s t : Set α
f : α → M
x : α
h : ¬x ∈ s
h_1 : ¬x ∈ s ∩ t
⊢ Eq.{u_3 + 1} (α := M) 1 1

Tactic:
simp_all +contextual
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f : α → M
rw : s.mulIndicator ((mulSupport f).mulIndicator f) = s.mulIndicator f
rw₁ rw₂ : s.mulIndicator f = s.mulIndicator f
⊢ (s ∩ mulSupport f).mulIndicator f = s.mulIndicator f

Tactic:
rw [← mulIndicator_mulIndicator, mulIndicator_mulSupport]

Premises used: Set.mulIndicator_mulSupport, Set.mulIndicator_mulIndicator
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : One M
h : M → β
f : α → M
s : Set α
x : α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
this : DecidablePred fun (x : α) ↦ x ∈ s := Classical.decPred fun (x : α) ↦ x ∈ s
⊢ h (s.piecewise (β := fun (i : α) ↦ M) f (const α 1) x) =
    s.piecewise (β := fun (x : α) ↦ β) (fun (x : α) ↦ h (f x)) (fun (x : α) ↦ h (const α 1 x)) x

Tactic:
s.apply_piecewise f (const α 1) (fun _ => h) (x := x)

Premises used: Function.const, OfNat.ofNat, Set.apply_piecewise
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : One M
h : M → β
f : α → M
s : Set α
x : α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
this : DecidablePred fun (x : α) ↦ x ∈ s := Classical.decPred fun (x : α) ↦ x ∈ s
⊢ h (s.mulIndicator f x) = s.piecewise (β := fun (a : α) ↦ β) (h ∘ f) (const α (h 1)) x

Tactic:
convert! s.apply_piecewise f (const α 1) (fun _ => h) (x := x) using 2

Premises used: Function.const, OfNat.ofNat, Set.apply_piecewise
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : One M
s : Set α
f : β → α
g : α → M
x : β
⊢ (f ⁻¹' s).mulIndicator (g ∘ f) x = s.mulIndicator g (f x)

Tactic:
tauto
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : One M
s : Set α
f : β → M
g : α → β
hg : Injective g
x : α
rw : (g ⁻¹' g '' s).mulIndicator (f ∘ g) x = s.mulIndicator (f ∘ g) x
rw₁ rw₂ : s.mulIndicator (f ∘ g) x = s.mulIndicator (f ∘ g) x
⊢ (g '' s).mulIndicator f (g x) = s.mulIndicator (f ∘ g) x

Tactic:
rw [← mulIndicator_comp_right, preimage_image_eq _ hg]

Premises used: Set.preimage_image_eq, Set.mulIndicator_comp_right
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
N : Type u_4
inst : One M
inst_1 : One N
s : Set α
f : α → M
g : M → N
hg : g 1 = 1
h : ∀ (x : α), s.mulIndicator (g ∘ f) x = (g ∘ s.mulIndicator f) x
⊢ s.mulIndicator (g ∘ f) = g ∘ s.mulIndicator f

Tactic:
funext
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
N : Type u_4
inst : One M
inst_1 : One N
s : Set α
f : α → M
g : M → N
hg : g 1 = 1
x : α
pos : x ∈ s → (g ∘ f) x = (g ∘ s.mulIndicator f) x
neg : ¬x ∈ s → 1 = (g ∘ s.mulIndicator f) x
⊢ (if x ∈ s then (g ∘ f) x else 1) = (g ∘ s.mulIndicator f) x

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
N : Type u_4
inst : One M
inst_1 : One N
s : Set α
f : α → M
g : M → N
hg : g 1 = 1
x : α
h : x ∈ s
⊢ (g ∘ f) x = (g ∘ s.mulIndicator f) x

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
N : Type u_4
inst : One M
inst_1 : One N
s : Set α
f : α → M
g : M → N
hg : g 1 = 1
x : α
h : ¬x ∈ s
⊢ 1 = (g ∘ s.mulIndicator f) x

Tactic:
simp [*]
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
N : Type u_4
inst : One M
inst_1 : One N
s : Set α
c : M
f : M → N
hf : f 1 = 1
⊢ Eq (α := (x : α) → N) (fun (x : α) ↦ f (s.mulIndicator (fun (x : α) ↦ c) x)) (s.mulIndicator fun (x : α) ↦ f c)

Tactic:
(mulIndicator_comp_of_one hf).symm

Premises used: Eq.symm, Set.mulIndicator_comp_of_one
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f : α → M
B : Set M
⊢ s.mulIndicator f ⁻¹' B = s.ite (f ⁻¹' B) (1 ⁻¹' B)

Tactic:
letI := Classical.decPred (· ∈ s)
  piecewise_preimage s f 1 B

Premises used: Set.mulIndicator, Set.piecewise_preimage, OfNat.ofNat
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
t : Set α
s : Set M
rw : Membership.mem (γ := Set (Set α)) {univ, ∅} (if 1 ∈ s then univ else ∅)
⊢ Membership.mem (γ := Set (Set α)) {univ, ∅} (t.mulIndicator 1 ⁻¹' s)

Tactic:
rw [mulIndicator_one', Pi.one_def, Set.preimage_const]

Premises used: Set.preimage_const, Pi.one_def, Set.mulIndicator_one'
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
t : Set α
s : Set M
pos : 1 ∈ s → Membership.mem (γ := Set (Set α)) {univ, ∅} univ
neg : ¬1 ∈ s → Membership.mem (γ := Set (Set α)) {univ, ∅} ∅
⊢ Membership.mem (γ := Set (Set α)) {univ, ∅} (if 1 ∈ s then univ else ∅)

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
t : Set α
s : Set M
h : 1 ∈ s
⊢ Membership.mem (γ := Set (Set α)) {univ, ∅} univ

Tactic:
simp
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
t : Set α
s : Set M
h : ¬1 ∈ s
⊢ Membership.mem (γ := Set (Set α)) {univ, ∅} ∅

Tactic:
simp
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
t : Set α
s : Set M
rw : Membership.mem (γ := Set (Set α)) {univ, ∅} (1 ⁻¹' s)
rw₁ : Membership.mem (γ := Set (Set α)) {univ, ∅} ((fun (x : α) ↦ 1) ⁻¹' s)
rw₂ rw₃ rw₄ : Membership.mem (γ := Set (Set α)) {univ, ∅} (if 1 ∈ s then univ else ∅)
⊢ Membership.mem (γ := Set (Set α)) {univ, ∅} (t.mulIndicator 1 ⁻¹' s)

Tactic:
classical
  rw [mulIndicator_one', Pi.one_def, Set.preimage_const]
  split_ifs <;> simp

Premises used: Set.preimage_const, Pi.one_def, Set.mulIndicator_one'
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
U : Set α
s : Set M
a : M
inst_1 : Decidable (a ∈ s)
inst_2 : Decidable (1 ∈ s)
rw : U.ite (if a ∈ s then univ else ∅) (if 1 ∈ s then univ else ∅) = (if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅
⊢ (U.mulIndicator fun (x : α) ↦ a) ⁻¹' s = (if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅

Tactic:
rw [mulIndicator_preimage, Pi.one_def, Set.preimage_const, preimage_const]

Premises used: Set.mulIndicator_preimage, Set.preimage_const, Pi.one_def
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
U : Set α
s : Set M
a : M
inst_1 : Decidable (a ∈ s)
inst_2 : Decidable (1 ∈ s)
pos : a ∈ s → 1 ∈ s → U.ite univ univ = U ∪ Uᶜ
neg : a ∈ s → ¬1 ∈ s → U.ite univ ∅ = U ∪ ∅
pos₁ : ¬a ∈ s → 1 ∈ s → U.ite ∅ univ = ∅ ∪ Uᶜ
neg₁ : ¬a ∈ s → ¬1 ∈ s → U.ite ∅ ∅ = ∅ ∪ ∅
⊢ U.ite (if a ∈ s then univ else ∅) (if 1 ∈ s then univ else ∅) = (if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
U : Set α
s : Set M
a : M
inst_1 : Decidable (a ∈ s)
inst_2 : Decidable (1 ∈ s)
h : a ∈ s
h_1 : 1 ∈ s
⊢ U.ite univ univ = U ∪ Uᶜ

Tactic:
simp [← compl_eq_univ_diff]

Premises used: Set.compl_eq_univ_diff
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
U : Set α
s : Set M
a : M
inst_1 : Decidable (a ∈ s)
inst_2 : Decidable (1 ∈ s)
h : a ∈ s
h_1 : ¬1 ∈ s
⊢ U.ite univ ∅ = U ∪ ∅

Tactic:
simp [← compl_eq_univ_diff]

Premises used: Set.compl_eq_univ_diff
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
U : Set α
s : Set M
a : M
inst_1 : Decidable (a ∈ s)
inst_2 : Decidable (1 ∈ s)
h : ¬a ∈ s
h_1 : 1 ∈ s
⊢ U.ite ∅ univ = ∅ ∪ Uᶜ

Tactic:
simp [← compl_eq_univ_diff]

Premises used: Set.compl_eq_univ_diff
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
U : Set α
s : Set M
a : M
inst_1 : Decidable (a ∈ s)
inst_2 : Decidable (1 ∈ s)
h : ¬a ∈ s
h_1 : ¬1 ∈ s
⊢ U.ite ∅ ∅ = ∅ ∪ ∅

Tactic:
simp [← compl_eq_univ_diff]

Premises used: Set.compl_eq_univ_diff
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
U : Set α
s : Set M
a : M
rw : Membership.mem (γ := Set (Set α)) {univ, U, Uᶜ, ∅} ((if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅)
⊢ Membership.mem (γ := Set (Set α)) {univ, U, Uᶜ, ∅} ((U.mulIndicator fun (x : α) ↦ a) ⁻¹' s)

Tactic:
rw [mulIndicator_const_preimage_eq_union]

Premises used: Set.mulIndicator_const_preimage_eq_union
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
U : Set α
s : Set M
a : M
pos : a ∈ s → 1 ∈ s → Membership.mem (γ := Set (Set α)) {univ, U, Uᶜ, ∅} (U ∪ Uᶜ)
neg : a ∈ s → ¬1 ∈ s → Membership.mem (γ := Set (Set α)) {univ, U, Uᶜ, ∅} (U ∪ ∅)
pos₁ : ¬a ∈ s → 1 ∈ s → Membership.mem (γ := Set (Set α)) {univ, U, Uᶜ, ∅} (∅ ∪ Uᶜ)
neg₁ : ¬a ∈ s → ¬1 ∈ s → Membership.mem (γ := Set (Set α)) {univ, U, Uᶜ, ∅} (∅ ∪ ∅)
⊢ Membership.mem (γ := Set (Set α)) {univ, U, Uᶜ, ∅} ((if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅)

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
U : Set α
s : Set M
a : M
h : a ∈ s
h_1 : 1 ∈ s
⊢ Membership.mem (γ := Set (Set α)) {univ, U, Uᶜ, ∅} (U ∪ Uᶜ)

Tactic:
simp
-- Module: Mathlib.Algebra.Notation.Indicator
Goal:
α : Type u_1
M : Type u_3
inst : One M
U : Set α
s : Set M
a : M
h : a ∈ s
h_1 : ¬1 ∈ s
⊢ Membership.mem (γ := Set (Set α)) {univ, U, Uᶜ, ∅} (U ∪ ∅)

Tactic:
simp