awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
Goal:
R : Type u_1
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
f : M →ₗ[R] M
hf : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
rw : (f.restrict hf).ker = ⊥ ↔ Disjoint p f.ker
rw₁ : comap p.subtype f.ker = ⊥ ↔ Disjoint p f.ker
⊢ Injective (α := ↥p) (β := ↥p) (⇑(f.restrict hf) : (a : ↥p) → ↥p) ↔ Disjoint p f.ker
have rw₂ : (f.domRestrict p).ker = ⊥ ↔ Disjoint p f.ker
Tactic: rw [← ker_eq_bot, ker_restrict hf, ← ker_domRestrict, ker_eq_bot, injective_domRestrict_iff,
    disjoint_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
Goal:
R : Type u_1
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
f : M →ₗ[R] M
hf : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
rw : (f.restrict hf).ker = ⊥ ↔ Disjoint p f.ker
rw₁ : comap p.subtype f.ker = ⊥ ↔ Disjoint p f.ker
rw₂ : (f.domRestrict p).ker = ⊥ ↔ Disjoint p f.ker
⊢ Injective (α := ↥p) (β := ↥p) (⇑(f.restrict hf) : (a : ↥p) → ↥p) ↔ Disjoint p f.ker
have rw₃ : Injective (α := ↥p) (β := M) (⇑(f.domRestrict p) : (a : ↥p) → M) ↔ Disjoint p f.ker
Tactic: rw [← ker_eq_bot, ker_restrict hf, ← ker_domRestrict, ker_eq_bot, injective_domRestrict_iff,
    disjoint_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
Goal:
R : Type u_1
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
f : M →ₗ[R] M
hf : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
rw : (f.restrict hf).ker = ⊥ ↔ Disjoint p f.ker
rw₁ : comap p.subtype f.ker = ⊥ ↔ Disjoint p f.ker
rw₂ : (f.domRestrict p).ker = ⊥ ↔ Disjoint p f.ker
rw₃ : Injective (α := ↥p) (β := M) (⇑(f.domRestrict p) : (a : ↥p) → M) ↔ Disjoint p f.ker
⊢ Injective (α := ↥p) (β := ↥p) (⇑(f.restrict hf) : (a : ↥p) → ↥p) ↔ Disjoint p f.ker
have rw₄ : p ⊓ f.ker = ⊥ ↔ Disjoint p f.ker
Tactic: rw [← ker_eq_bot, ker_restrict hf, ← ker_domRestrict, ker_eq_bot, injective_domRestrict_iff,
    disjoint_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
Goal:
R : Type u_1
M : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
f : M →ₗ[R] M
hf : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
rw : (f.restrict hf).ker = ⊥ ↔ Disjoint p f.ker
rw₁ : comap p.subtype f.ker = ⊥ ↔ Disjoint p f.ker
rw₂ : (f.domRestrict p).ker = ⊥ ↔ Disjoint p f.ker
rw₃ : Injective (α := ↥p) (β := M) (⇑(f.domRestrict p) : (a : ↥p) → M) ↔ Disjoint p f.ker
rw₄ : p ⊓ f.ker = ⊥ ↔ Disjoint p f.ker
⊢ Injective (α := ↥p) (β := ↥p) (⇑(f.restrict hf) : (a : ↥p) → ↥p) ↔ Disjoint p f.ker
have rw₅ : p ⊓ f.ker = ⊥ ↔ p ⊓ f.ker = ⊥
Tactic: rw [← ker_eq_bot, ker_restrict hf, ← ker_domRestrict, ker_eq_bot, injective_domRestrict_iff,
    disjoint_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p p' : Submodule R M
h : p ≤ p'
⊢ (inclusion h).ker = ⊥
have rw : (codRestrict p' p.subtype sorry).ker = ⊥
Tactic: rw [inclusion, ker_codRestrict, ker_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p p' : Submodule R M
h : p ≤ p'
rw : (codRestrict p' p.subtype ⋯).ker = ⊥
⊢ (inclusion h).ker = ⊥
have rw₁ : p.subtype.ker = ⊥
Tactic: rw [inclusion, ker_codRestrict, ker_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p p' : Submodule R M
h : p ≤ p'
rw : (codRestrict p' p.subtype ⋯).ker = ⊥
rw₁ : p.subtype.ker = ⊥
⊢ (inclusion h).ker = ⊥
have rw₂ : Eq.{u_5 + 1} (α := Submodule R ↥p) ⊥ ⊥
Tactic: rw [inclusion, ker_codRestrict, ker_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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 = ⊥
⊢ (g ∘ₛₗ f).ker = f.ker
have rw : Submodule.comap f g.ker = f.ker
Tactic: rw [ker_comp, hg, Submodule.comap_bot]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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
⊢ (g ∘ₛₗ f).ker = f.ker
have rw₁ : Submodule.comap f ⊥ = f.ker
Tactic: rw [ker_comp, hg, Submodule.comap_bot]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Ker (goal)
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
⊢ (g ∘ₛₗ f).ker = f.ker
have rw₂ : f.ker = f.ker
Tactic: rw [ker_comp, hg, Submodule.comap_bot]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f : α → M
a : α
⊢ s.mulIndicator f a = 1 ∨ s.mulIndicator f a = f a
have pos : ∀ (h : a ∈ s), s.mulIndicator f a = 1 ∨ s.mulIndicator f a = f a
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
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
⊢ s.mulIndicator f a = 1 ∨ s.mulIndicator f a = f a
have neg : ∀ (h : ¬a ∈ s), s.mulIndicator f a = 1 ∨ s.mulIndicator f a = f a
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f : α → M
a : α
this : Decidable (a ∈ s) := Classical.dec (a ∈ s)
⊢ ¬a ∈ s → 1 = f a ↔ ¬a ∈ s → f a = 1
have rw : ¬a ∈ s → 1 = f a ↔ ¬a ∈ s → 1 = f a
Tactic: rw [@eq_comm _ (f a)]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
Goal:
α : Type u_1
M : Type u_3
inst : One M
s t : Set α
f : α → M
h1 : s.mulIndicator f = f
h2 : s ⊆ t
⊢ t.mulIndicator f = f
have rw : ∀ (h1 : mulSupport f ⊆ s) (h2 : s ⊆ t), mulSupport f ⊆ t
Tactic: rw [mulIndicator_eq_self] at h1 ⊢
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f g : α → M
h : EqOn f g s
x : α
⊢ (if x ∈ s then f x else 1) = if x ∈ s then g x else 1
have pos : ∀ (h_1 : x ∈ s), f x = g x
Tactic: split_ifs with h_1
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
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
⊢ (if x ∈ s then f x else 1) = if x ∈ s then g x else 1
have neg : ∀ (h_1 : ¬x ∈ s), Eq.{u_3 + 1} (α := M) 1 1
Tactic: split_ifs with h_1
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
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
⊢ s.mulIndicator f a = t.mulIndicator g b
have pos : a ∈ s → s.mulIndicator f a = t.mulIndicator g b
Tactic: by_cases a ∈ s
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
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
⊢ s.mulIndicator f a = t.mulIndicator g b
have neg : ¬a ∈ s → s.mulIndicator f a = t.mulIndicator g b
Tactic: by_cases a ∈ s
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
Goal:
α : Type u_1
M : Type u_3
inst : One M
s t : Set α
f : α → M
x : α
⊢ (if x ∈ s then if x ∈ t then f x else 1 else 1) = if x ∈ s ∩ t then f x else 1
have pos : x ∈ s → x ∈ t → x ∈ s ∩ t → f x = f x
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
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
⊢ (if x ∈ s then if x ∈ t then f x else 1 else 1) = if x ∈ s ∩ t then f x else 1
have neg : x ∈ s → x ∈ t → ¬x ∈ s ∩ t → f x = 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
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
⊢ (if x ∈ s then if x ∈ t then f x else 1 else 1) = if x ∈ s ∩ t then f x else 1
have pos₁ : x ∈ s → ¬x ∈ t → x ∈ s ∩ t → 1 = f x
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
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
⊢ (if x ∈ s then if x ∈ t then f x else 1 else 1) = if x ∈ s ∩ t then f x else 1
have neg₁ : x ∈ s → ¬x ∈ t → ¬x ∈ s ∩ t → Eq.{u_3 + 1} (α := M) 1 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
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
⊢ (if x ∈ s then if x ∈ t then f x else 1 else 1) = if x ∈ s ∩ t then f x else 1
have pos₂ : ¬x ∈ s → x ∈ s ∩ t → 1 = f x
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
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
⊢ (if x ∈ s then if x ∈ t then f x else 1 else 1) = if x ∈ s ∩ t then f x else 1
have neg₂ : ¬x ∈ s → ¬x ∈ s ∩ t → Eq.{u_3 + 1} (α := M) 1 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f : α → M
⊢ (s ∩ mulSupport f).mulIndicator f = s.mulIndicator f
have rw : s.mulIndicator ((mulSupport f).mulIndicator f) = s.mulIndicator f
Tactic: rw [← mulIndicator_mulIndicator, mulIndicator_mulSupport]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
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
⊢ (s ∩ mulSupport f).mulIndicator f = s.mulIndicator f
have rw₁ : s.mulIndicator f = s.mulIndicator f
Tactic: rw [← mulIndicator_mulIndicator, mulIndicator_mulSupport]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_3
inst : One M
s : Set α
f : β → M
g : α → β
hg : Injective g
x : α
⊢ (g '' s).mulIndicator f (g x) = s.mulIndicator (f ∘ g) x
have rw : (g ⁻¹' g '' s).mulIndicator (f ∘ g) x = s.mulIndicator (f ∘ g) x
Tactic: rw [← mulIndicator_comp_right, preimage_image_eq _ hg]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
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
⊢ (g '' s).mulIndicator f (g x) = s.mulIndicator (f ∘ g) x
have rw₁ : s.mulIndicator (f ∘ g) x = s.mulIndicator (f ∘ g) x
Tactic: rw [← mulIndicator_comp_right, preimage_image_eq _ hg]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
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
⊢ s.mulIndicator (g ∘ f) = g ∘ s.mulIndicator f
have h : ∀ (x : α), s.mulIndicator (g ∘ f) x = (g ∘ s.mulIndicator f) x
Tactic: funext
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
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 : α
⊢ (if x ∈ s then (g ∘ f) x else 1) = (g ∘ s.mulIndicator f) x
have pos : x ∈ s → (g ∘ f) x = (g ∘ s.mulIndicator f) x
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
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
⊢ (if x ∈ s then (g ∘ f) x else 1) = (g ∘ s.mulIndicator f) x
have neg : ¬x ∈ s → 1 = (g ∘ s.mulIndicator f) x
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
Goal:
α : Type u_1
M : Type u_3
inst : One M
t : Set α
s : Set M
⊢ Membership.mem (γ := Set (Set α)) {univ, ∅} (t.mulIndicator 1 ⁻¹' s)
have rw : Membership.mem (γ := Set (Set α)) {univ, ∅} (if 1 ∈ s then univ else ∅)
Tactic: rw [mulIndicator_one', Pi.one_def, Set.preimage_const]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
Goal:
α : Type u_1
M : Type u_3
inst : One M
t : Set α
s : Set M
⊢ Membership.mem (γ := Set (Set α)) {univ, ∅} (if 1 ∈ s then univ else ∅)
have pos : 1 ∈ s → Membership.mem (γ := Set (Set α)) {univ, ∅} univ
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
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
⊢ Membership.mem (γ := Set (Set α)) {univ, ∅} (if 1 ∈ s then univ else ∅)
have neg : ¬1 ∈ s → Membership.mem (γ := Set (Set α)) {univ, ∅} ∅
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
Goal:
α : Type u_1
M : Type u_3
inst : One M
t : Set α
s : Set M
⊢ Membership.mem (γ := Set (Set α)) {univ, ∅} (t.mulIndicator 1 ⁻¹' s)
have rw : Membership.mem (γ := Set (Set α)) {univ, ∅} (1 ⁻¹' s)
Tactic: classical
  rw [mulIndicator_one', Pi.one_def, Set.preimage_const]
  split_ifs <;> simp
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
Goal:
α : Type u_1
M : Type u_3
inst : One M
t : Set α
s : Set M
rw : Membership.mem (γ := Set (Set α)) {univ, ∅} (1 ⁻¹' s)
⊢ Membership.mem (γ := Set (Set α)) {univ, ∅} (t.mulIndicator 1 ⁻¹' s)
have rw₁ : Membership.mem (γ := Set (Set α)) {univ, ∅} ((fun (x : α) ↦ 1) ⁻¹' s)
Tactic: classical
  rw [mulIndicator_one', Pi.one_def, Set.preimage_const]
  split_ifs <;> simp
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
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)
⊢ Membership.mem (γ := Set (Set α)) {univ, ∅} (t.mulIndicator 1 ⁻¹' s)
have rw₂ : Membership.mem (γ := Set (Set α)) {univ, ∅} (if 1 ∈ s then univ else ∅)
Tactic: classical
  rw [mulIndicator_one', Pi.one_def, Set.preimage_const]
  split_ifs <;> simp
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
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)
⊢ (U.mulIndicator fun (x : α) ↦ a) ⁻¹' s = (if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅
have 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 ∅
Tactic: rw [mulIndicator_preimage, Pi.one_def, Set.preimage_const, preimage_const]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
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)
⊢ 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 ∅
have pos : a ∈ s → 1 ∈ s → U.ite univ univ = U ∪ Uᶜ
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
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ᶜ
⊢ 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 ∅
have neg : a ∈ s → ¬1 ∈ s → U.ite univ ∅ = U ∪ ∅
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
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 ∪ ∅
⊢ 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 ∅
have pos₁ : ¬a ∈ s → 1 ∈ s → U.ite ∅ univ = ∅ ∪ Uᶜ
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
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ᶜ
⊢ 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 ∅
have neg₁ : ¬a ∈ s → ¬1 ∈ s → U.ite ∅ ∅ = ∅ ∪ ∅
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
Goal:
α : Type u_1
M : Type u_3
inst : One M
U : Set α
s : Set M
a : M
⊢ Membership.mem (γ := Set (Set α)) {univ, U, Uᶜ, ∅} ((U.mulIndicator fun (x : α) ↦ a) ⁻¹' s)
have rw : Membership.mem (γ := Set (Set α)) {univ, U, Uᶜ, ∅} ((if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅)
Tactic: rw [mulIndicator_const_preimage_eq_union]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
Goal:
α : Type u_1
M : Type u_3
inst : One M
U : Set α
s : Set M
a : M
⊢ Membership.mem (γ := Set (Set α)) {univ, U, Uᶜ, ∅} ((if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅)
have pos : a ∈ s → 1 ∈ s → Membership.mem (γ := Set (Set α)) {univ, U, Uᶜ, ∅} (U ∪ Uᶜ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
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ᶜ)
⊢ Membership.mem (γ := Set (Set α)) {univ, U, Uᶜ, ∅} ((if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅)
have neg : a ∈ s → ¬1 ∈ s → Membership.mem (γ := Set (Set α)) {univ, U, Uᶜ, ∅} (U ∪ ∅)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
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 ∪ ∅)
⊢ Membership.mem (γ := Set (Set α)) {univ, U, Uᶜ, ∅} ((if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅)
have pos₁ : ¬a ∈ s → 1 ∈ s → Membership.mem (γ := Set (Set α)) {univ, U, Uᶜ, ∅} (∅ ∪ Uᶜ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
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ᶜ)
⊢ Membership.mem (γ := Set (Set α)) {univ, U, Uᶜ, ∅} ((if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅)
have neg₁ : ¬a ∈ s → ¬1 ∈ s → Membership.mem (γ := Set (Set α)) {univ, U, Uᶜ, ∅} (∅ ∪ ∅)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
Goal:
α : Type u_1
M : Type u_3
inst : One M
U : Set α
s : Set M
a : M
⊢ Membership.mem (γ := Set (Set α)) {univ, U, Uᶜ, ∅} ((U.mulIndicator fun (x : α) ↦ a) ⁻¹' s)
have rw : Membership.mem (γ := Set (Set α)) {univ, U, Uᶜ, ∅} ((if a ∈ s then U else ∅) ∪ if 1 ∈ s then Uᶜ else ∅)
Tactic: classical
    rw [mulIndicator_const_preimage_eq_union]
    split_ifs <;> simp
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha : a ∈ s → r (f a) (g a)
⊢ r (s.mulIndicator f a) (s.mulIndicator g a)
have simp : r (if a ∈ s then f a else 1) (if a ∈ s then g a else 1)
Tactic: simp only [mulIndicator]
-- Lean 4 proof step from Mathlib.Algebra.Notation.Indicator (goal)
Goal:
α : Type u_1
M : Type u_3
inst : One M
s : Set α
f g : α → M
a : α
r : M → M → Prop
h1 : r 1 1
ha pos : ∀ (has : a ∈ s), r (f a) (g a)
⊢ r (if a ∈ s then f a else 1) (if a ∈ s then g a else 1)
have neg : ∀ (has : ¬a ∈ s), r 1 1
Tactic: split_ifs with has
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.PositiveLinearMap (goal)
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid E₁
inst_2 : PartialOrder E₁
inst_3 : AddCommMonoid E₂
inst_4 : PartialOrder E₂
inst_5 : Module R E₁
inst_6 : Module R E₂
f g : E₁ →ₚ[R] E₂
h : Eq (α := (a : E₁) → E₂) ((fun (f : E₁ →ₚ[R] E₂) ↦ f.toFun) f) ((fun (f : E₁ →ₚ[R] E₂) ↦ f.toFun) g)
⊢ f = g
have mk : ∀ (toLinearMap : E₁ →ₗ[R] E₂) (monotone' : Monotone toLinearMap.toFun)
  (h :
    Eq (α := (a : E₁) → E₂) ((fun (f : E₁ →ₚ[R] E₂) ↦ f.toFun) { toLinearMap := toLinearMap, monotone' := monotone' })
      ((fun (f : E₁ →ₚ[R] E₂) ↦ f.toFun) g)),
  { toLinearMap := toLinearMap, monotone' := monotone' : E₁ →ₚ[R] E₂ } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.PositiveLinearMap (goal)
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid E₁
inst_2 : PartialOrder E₁
inst_3 : AddCommMonoid E₂
inst_4 : PartialOrder E₂
inst_5 : Module R E₁
inst_6 : Module R E₂
g : E₁ →ₚ[R] E₂
toLinearMap : E₁ →ₗ[R] E₂
monotone' : Monotone toLinearMap.toFun
h :
  Eq (α := (a : E₁) → E₂) ((fun (f : E₁ →ₚ[R] E₂) ↦ f.toFun) { toLinearMap := toLinearMap, monotone' := monotone' })
    ((fun (f : E₁ →ₚ[R] E₂) ↦ f.toFun) g)
⊢ { toLinearMap := toLinearMap, monotone' := monotone' : E₁ →ₚ[R] E₂ } = g
have mk : ∀ (toLinearMap_1 : E₁ →ₗ[R] E₂) (monotone'_1 : Monotone toLinearMap_1.toFun)
  (h :
    Eq (α := (a : E₁) → E₂) ((fun (f : E₁ →ₚ[R] E₂) ↦ f.toFun) { toLinearMap := toLinearMap, monotone' := monotone' })
      ((fun (f : E₁ →ₚ[R] E₂) ↦ f.toFun) { toLinearMap := toLinearMap_1, monotone' := monotone'_1 })),
  { toLinearMap := toLinearMap, monotone' := monotone' : E₁ →ₚ[R] E₂ } =
    { toLinearMap := toLinearMap_1, monotone' := monotone'_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Module.PositiveLinearMap (goal)
Goal:
R : Type u_1
E₁ : Type u_2
E₂ : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid E₁
inst_2 : PartialOrder E₁
inst_3 : AddCommMonoid E₂
inst_4 : PartialOrder E₂
inst_5 : Module R E₁
inst_6 : Module R E₂
toLinearMap : E₁ →ₗ[R] E₂
monotone' : Monotone toLinearMap.toFun
toLinearMap_1 : E₁ →ₗ[R] E₂
monotone'_1 : Monotone toLinearMap_1.toFun
h :
  Eq (α := (a : E₁) → E₂) ((fun (f : E₁ →ₚ[R] E₂) ↦ f.toFun) { toLinearMap := toLinearMap, monotone' := monotone' })
    ((fun (f : E₁ →ₚ[R] E₂) ↦ f.toFun) { toLinearMap := toLinearMap_1, monotone' := monotone'_1 })
⊢ { toLinearMap := toLinearMap, monotone' := monotone' : E₁ →ₚ[R] E₂ } =
    { toLinearMap := toLinearMap_1, monotone' := monotone'_1 }
have mk : toLinearMap = toLinearMap_1
Tactic: congr