awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
h : ¬(s x ↔ t x) → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
h₁ : x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s → ¬(s x ↔ t x)
h₂ : ¬s x → t x → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
h₃ : ¬¬s x → ¬t x → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
h₄ : ¬s x → t x → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
h₅ : ¬¬s x → ¬t x → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
h₆ : ¬s x → t x → ¬(x ∈ s ∧ x ∉ t) → x ∈ t
h₇ : ¬s x → t x → ¬(x ∈ s ∧ x ∉ t) → x ∉ s
h₈ : ¬¬s x → ¬t x → ¬(x ∈ s ∧ x ∉ t) → x ∈ t
h₉ : ¬¬s x → ¬t x → ¬(x ∈ s ∧ x ∉ t) → x ∉ s
h₁₀ : x ∈ s → x ∉ t → ¬(s x ↔ t x)
h₁₁ : x ∈ t → x ∉ s → ¬(s x ↔ t x)
h₁₂ : x ∈ s → x ∉ t → ¬(s x ↔ t x)
h₁₃ : x ∈ t → x ∉ s → ¬(s x ↔ t x)
h₁₄ : x ∈ s → x ∉ t → (s x ↔ t x) → False
h₁₅ : x ∈ t → x ∉ s → (s x ↔ t x) → False
h₁₆ : s x → ¬t x → x ∉ s → x ∈ t
h₁₇ : s x → ¬t x → ¬x ∉ t → x ∈ t
h₁₈ : s x → ¬t x → x ∈ s → x ∉ s → False
h₁₉ : s x → ¬t x → x ∈ s → ¬x ∉ t → False
h₂₀ : x ∈ s → x ∉ t → s x → t x → False
⊢ ¬(s x ↔ t x) ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have h₂₁ : x ∈ s → x ∉ t → ¬s x → ¬t x → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
h : ¬(s x ↔ t x) → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
h₁ : x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s → ¬(s x ↔ t x)
h₂ : ¬s x → t x → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
h₃ : ¬¬s x → ¬t x → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
h₄ : ¬s x → t x → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
h₅ : ¬¬s x → ¬t x → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
h₆ : ¬s x → t x → ¬(x ∈ s ∧ x ∉ t) → x ∈ t
h₇ : ¬s x → t x → ¬(x ∈ s ∧ x ∉ t) → x ∉ s
h₈ : ¬¬s x → ¬t x → ¬(x ∈ s ∧ x ∉ t) → x ∈ t
h₉ : ¬¬s x → ¬t x → ¬(x ∈ s ∧ x ∉ t) → x ∉ s
h₁₀ : x ∈ s → x ∉ t → ¬(s x ↔ t x)
h₁₁ : x ∈ t → x ∉ s → ¬(s x ↔ t x)
h₁₂ : x ∈ s → x ∉ t → ¬(s x ↔ t x)
h₁₃ : x ∈ t → x ∉ s → ¬(s x ↔ t x)
h₁₄ : x ∈ s → x ∉ t → (s x ↔ t x) → False
h₁₅ : x ∈ t → x ∉ s → (s x ↔ t x) → False
h₁₆ : s x → ¬t x → x ∉ s → x ∈ t
h₁₇ : s x → ¬t x → ¬x ∉ t → x ∈ t
h₁₈ : s x → ¬t x → x ∈ s → x ∉ s → False
h₁₉ : s x → ¬t x → x ∈ s → ¬x ∉ t → False
h₂₀ : x ∈ s → x ∉ t → s x → t x → False
h₂₁ : x ∈ s → x ∉ t → ¬s x → ¬t x → False
⊢ ¬(s x ↔ t x) ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have h₂₂ : x ∈ t → x ∉ s → s x → t x → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
h : ¬(s x ↔ t x) → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
h₁ : x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s → ¬(s x ↔ t x)
h₂ : ¬s x → t x → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
h₃ : ¬¬s x → ¬t x → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
h₄ : ¬s x → t x → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
h₅ : ¬¬s x → ¬t x → x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
h₆ : ¬s x → t x → ¬(x ∈ s ∧ x ∉ t) → x ∈ t
h₇ : ¬s x → t x → ¬(x ∈ s ∧ x ∉ t) → x ∉ s
h₈ : ¬¬s x → ¬t x → ¬(x ∈ s ∧ x ∉ t) → x ∈ t
h₉ : ¬¬s x → ¬t x → ¬(x ∈ s ∧ x ∉ t) → x ∉ s
h₁₀ : x ∈ s → x ∉ t → ¬(s x ↔ t x)
h₁₁ : x ∈ t → x ∉ s → ¬(s x ↔ t x)
h₁₂ : x ∈ s → x ∉ t → ¬(s x ↔ t x)
h₁₃ : x ∈ t → x ∉ s → ¬(s x ↔ t x)
h₁₄ : x ∈ s → x ∉ t → (s x ↔ t x) → False
h₁₅ : x ∈ t → x ∉ s → (s x ↔ t x) → False
h₁₆ : s x → ¬t x → x ∉ s → x ∈ t
h₁₇ : s x → ¬t x → ¬x ∉ t → x ∈ t
h₁₈ : s x → ¬t x → x ∈ s → x ∉ s → False
h₁₉ : s x → ¬t x → x ∈ s → ¬x ∉ t → False
h₂₀ : x ∈ s → x ∉ t → s x → t x → False
h₂₁ : x ∈ s → x ∉ t → ¬s x → ¬t x → False
h₂₂ : x ∈ t → x ∉ s → s x → t x → False
⊢ ¬(s x ↔ t x) ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
have h₂₃ : x ∈ t → x ∉ s → ¬s x → ¬t x → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set β) → ℝ≥0∞) {a : β | ¬(f '' s) a = (f '' t) a} : ℝ≥0∞) (0 : ℝ≥0∞)
have h_eq_α : {a : α | ¬s a = t a} = s \ t ∪ t \ s
Tactic: have h_eq_α : { a : α | ¬s a = t a } = s \ t ∪ t \ s := by
    ext1 x
    simp only [eq_iff_iff, mem_setOf_eq, mem_union, mem_diff]
    tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq_α : {a : α | ¬s a = t a} = s \ t ∪ t \ s
⊢ {a : β | ¬(f '' s) a = (f '' t) a} = f '' s \ f '' t ∪ f '' t \ f '' s
have h : ∀ (x : β), Membership.mem (γ := Set β) {a : β | ¬(f '' s) a = (f '' t) a} x ↔ x ∈ f '' s \ f '' t ∪ f '' t \ f '' s
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq_α : {a : α | ¬s a = t a} = s \ t ∪ t \ s
x : β
⊢ Membership.mem (γ := Set β) {a : β | ¬(f '' s) a = (f '' t) a} x ↔ x ∈ f '' s \ f '' t ∪ f '' t \ f '' s
have h : ¬((f '' s) x ↔ (f '' t) x) ↔ x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
Tactic: simp only [eq_iff_iff, mem_setOf_eq, mem_union, mem_diff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq_α : {a : α | ¬s a = t a} = s \ t ∪ t \ s
x : β
⊢ ¬((f '' s) x ↔ (f '' t) x) ↔ x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
have h : ¬((f '' s) x ↔ (f '' t) x) → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq_α : {a : α | ¬s a = t a} = s \ t ∪ t \ s
x : β
h : ¬((f '' s) x ↔ (f '' t) x) → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
⊢ ¬((f '' s) x ↔ (f '' t) x) ↔ x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
have h₁ : x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s → ¬((f '' s) x ↔ (f '' t) x)
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq_α : {a : α | ¬s a = t a} = s \ t ∪ t \ s
x : β
h : ¬((f '' s) x ↔ (f '' t) x) → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₁ : x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s → ¬((f '' s) x ↔ (f '' t) x)
⊢ ¬((f '' s) x ↔ (f '' t) x) ↔ x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
have h₂ : ¬(f '' s) x → (f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq_α : {a : α | ¬s a = t a} = s \ t ∪ t \ s
x : β
h : ¬((f '' s) x ↔ (f '' t) x) → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₁ : x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s → ¬((f '' s) x ↔ (f '' t) x)
h₂ : ¬(f '' s) x → (f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
⊢ ¬((f '' s) x ↔ (f '' t) x) ↔ x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
have h₃ : ¬¬(f '' s) x → ¬(f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq_α : {a : α | ¬s a = t a} = s \ t ∪ t \ s
x : β
h : ¬((f '' s) x ↔ (f '' t) x) → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₁ : x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s → ¬((f '' s) x ↔ (f '' t) x)
h₂ : ¬(f '' s) x → (f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₃ : ¬¬(f '' s) x → ¬(f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₄ : ¬(f '' s) x → (f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₅ : ¬¬(f '' s) x → ¬(f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
⊢ ¬((f '' s) x ↔ (f '' t) x) ↔ x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
have h₆ : ¬(f '' s) x → (f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∈ f '' t
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq_α : {a : α | ¬s a = t a} = s \ t ∪ t \ s
x : β
h : ¬((f '' s) x ↔ (f '' t) x) → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₁ : x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s → ¬((f '' s) x ↔ (f '' t) x)
h₂ : ¬(f '' s) x → (f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₃ : ¬¬(f '' s) x → ¬(f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₄ : ¬(f '' s) x → (f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₅ : ¬¬(f '' s) x → ¬(f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₆ : ¬(f '' s) x → (f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∈ f '' t
⊢ ¬((f '' s) x ↔ (f '' t) x) ↔ x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
have h₇ : ¬(f '' s) x → (f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∉ f '' s
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq_α : {a : α | ¬s a = t a} = s \ t ∪ t \ s
x : β
h : ¬((f '' s) x ↔ (f '' t) x) → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₁ : x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s → ¬((f '' s) x ↔ (f '' t) x)
h₂ : ¬(f '' s) x → (f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₃ : ¬¬(f '' s) x → ¬(f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₄ : ¬(f '' s) x → (f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₅ : ¬¬(f '' s) x → ¬(f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₆ : ¬(f '' s) x → (f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∈ f '' t
h₇ : ¬(f '' s) x → (f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∉ f '' s
⊢ ¬((f '' s) x ↔ (f '' t) x) ↔ x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
have h₈ : ¬¬(f '' s) x → ¬(f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∈ f '' t
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq_α : {a : α | ¬s a = t a} = s \ t ∪ t \ s
x : β
h : ¬((f '' s) x ↔ (f '' t) x) → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₁ : x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s → ¬((f '' s) x ↔ (f '' t) x)
h₂ : ¬(f '' s) x → (f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₃ : ¬¬(f '' s) x → ¬(f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₄ : ¬(f '' s) x → (f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₅ : ¬¬(f '' s) x → ¬(f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₆ : ¬(f '' s) x → (f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∈ f '' t
h₇ : ¬(f '' s) x → (f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∉ f '' s
h₈ : ¬¬(f '' s) x → ¬(f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∈ f '' t
⊢ ¬((f '' s) x ↔ (f '' t) x) ↔ x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
have h₉ : ¬¬(f '' s) x → ¬(f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∉ f '' s
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq_α : {a : α | ¬s a = t a} = s \ t ∪ t \ s
x : β
h : ¬((f '' s) x ↔ (f '' t) x) → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₁ : x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s → ¬((f '' s) x ↔ (f '' t) x)
h₂ : ¬(f '' s) x → (f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₃ : ¬¬(f '' s) x → ¬(f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₄ : ¬(f '' s) x → (f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₅ : ¬¬(f '' s) x → ¬(f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₆ : ¬(f '' s) x → (f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∈ f '' t
h₇ : ¬(f '' s) x → (f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∉ f '' s
h₈ : ¬¬(f '' s) x → ¬(f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∈ f '' t
h₉ : ¬¬(f '' s) x → ¬(f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∉ f '' s
⊢ ¬((f '' s) x ↔ (f '' t) x) ↔ x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
have h₁₀ : x ∈ f '' s → x ∉ f '' t → ¬((f '' s) x ↔ (f '' t) x)
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq_α : {a : α | ¬s a = t a} = s \ t ∪ t \ s
x : β
h : ¬((f '' s) x ↔ (f '' t) x) → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₁ : x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s → ¬((f '' s) x ↔ (f '' t) x)
h₂ : ¬(f '' s) x → (f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₃ : ¬¬(f '' s) x → ¬(f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₄ : ¬(f '' s) x → (f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₅ : ¬¬(f '' s) x → ¬(f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₆ : ¬(f '' s) x → (f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∈ f '' t
h₇ : ¬(f '' s) x → (f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∉ f '' s
h₈ : ¬¬(f '' s) x → ¬(f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∈ f '' t
h₉ : ¬¬(f '' s) x → ¬(f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∉ f '' s
h₁₀ : x ∈ f '' s → x ∉ f '' t → ¬((f '' s) x ↔ (f '' t) x)
⊢ ¬((f '' s) x ↔ (f '' t) x) ↔ x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
have h₁₁ : x ∈ f '' t → x ∉ f '' s → ¬((f '' s) x ↔ (f '' t) x)
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq_α : {a : α | ¬s a = t a} = s \ t ∪ t \ s
x : β
h : ¬((f '' s) x ↔ (f '' t) x) → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₁ : x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s → ¬((f '' s) x ↔ (f '' t) x)
h₂ : ¬(f '' s) x → (f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₃ : ¬¬(f '' s) x → ¬(f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₄ : ¬(f '' s) x → (f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₅ : ¬¬(f '' s) x → ¬(f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₆ : ¬(f '' s) x → (f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∈ f '' t
h₇ : ¬(f '' s) x → (f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∉ f '' s
h₈ : ¬¬(f '' s) x → ¬(f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∈ f '' t
h₉ : ¬¬(f '' s) x → ¬(f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∉ f '' s
h₁₀ : x ∈ f '' s → x ∉ f '' t → ¬((f '' s) x ↔ (f '' t) x)
h₁₁ : x ∈ f '' t → x ∉ f '' s → ¬((f '' s) x ↔ (f '' t) x)
h₁₂ : x ∈ f '' s → x ∉ f '' t → ¬((f '' s) x ↔ (f '' t) x)
h₁₃ : x ∈ f '' t → x ∉ f '' s → ¬((f '' s) x ↔ (f '' t) x)
h₁₄ : x ∈ f '' s → x ∉ f '' t → ((f '' s) x ↔ (f '' t) x) → False
h₁₅ : x ∈ f '' t → x ∉ f '' s → ((f '' s) x ↔ (f '' t) x) → False
⊢ ¬((f '' s) x ↔ (f '' t) x) ↔ x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
have h₁₆ : (f '' s) x → ¬(f '' t) x → x ∉ f '' s → x ∈ f '' t
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq_α : {a : α | ¬s a = t a} = s \ t ∪ t \ s
x : β
h : ¬((f '' s) x ↔ (f '' t) x) → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₁ : x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s → ¬((f '' s) x ↔ (f '' t) x)
h₂ : ¬(f '' s) x → (f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₃ : ¬¬(f '' s) x → ¬(f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₄ : ¬(f '' s) x → (f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₅ : ¬¬(f '' s) x → ¬(f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₆ : ¬(f '' s) x → (f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∈ f '' t
h₇ : ¬(f '' s) x → (f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∉ f '' s
h₈ : ¬¬(f '' s) x → ¬(f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∈ f '' t
h₉ : ¬¬(f '' s) x → ¬(f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∉ f '' s
h₁₀ : x ∈ f '' s → x ∉ f '' t → ¬((f '' s) x ↔ (f '' t) x)
h₁₁ : x ∈ f '' t → x ∉ f '' s → ¬((f '' s) x ↔ (f '' t) x)
h₁₂ : x ∈ f '' s → x ∉ f '' t → ¬((f '' s) x ↔ (f '' t) x)
h₁₃ : x ∈ f '' t → x ∉ f '' s → ¬((f '' s) x ↔ (f '' t) x)
h₁₄ : x ∈ f '' s → x ∉ f '' t → ((f '' s) x ↔ (f '' t) x) → False
h₁₅ : x ∈ f '' t → x ∉ f '' s → ((f '' s) x ↔ (f '' t) x) → False
h₁₆ : (f '' s) x → ¬(f '' t) x → x ∉ f '' s → x ∈ f '' t
⊢ ¬((f '' s) x ↔ (f '' t) x) ↔ x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
have h₁₇ : (f '' s) x → ¬(f '' t) x → ¬x ∉ f '' t → x ∈ f '' t
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq_α : {a : α | ¬s a = t a} = s \ t ∪ t \ s
x : β
h : ¬((f '' s) x ↔ (f '' t) x) → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₁ : x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s → ¬((f '' s) x ↔ (f '' t) x)
h₂ : ¬(f '' s) x → (f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₃ : ¬¬(f '' s) x → ¬(f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₄ : ¬(f '' s) x → (f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₅ : ¬¬(f '' s) x → ¬(f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₆ : ¬(f '' s) x → (f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∈ f '' t
h₇ : ¬(f '' s) x → (f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∉ f '' s
h₈ : ¬¬(f '' s) x → ¬(f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∈ f '' t
h₉ : ¬¬(f '' s) x → ¬(f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∉ f '' s
h₁₀ : x ∈ f '' s → x ∉ f '' t → ¬((f '' s) x ↔ (f '' t) x)
h₁₁ : x ∈ f '' t → x ∉ f '' s → ¬((f '' s) x ↔ (f '' t) x)
h₁₂ : x ∈ f '' s → x ∉ f '' t → ¬((f '' s) x ↔ (f '' t) x)
h₁₃ : x ∈ f '' t → x ∉ f '' s → ¬((f '' s) x ↔ (f '' t) x)
h₁₄ : x ∈ f '' s → x ∉ f '' t → ((f '' s) x ↔ (f '' t) x) → False
h₁₅ : x ∈ f '' t → x ∉ f '' s → ((f '' s) x ↔ (f '' t) x) → False
h₁₆ : (f '' s) x → ¬(f '' t) x → x ∉ f '' s → x ∈ f '' t
h₁₇ : (f '' s) x → ¬(f '' t) x → ¬x ∉ f '' t → x ∈ f '' t
⊢ ¬((f '' s) x ↔ (f '' t) x) ↔ x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
have h₁₈ : (f '' s) x → ¬(f '' t) x → x ∈ f '' s → x ∉ f '' s → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Comap (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : Eq (α := ℝ≥0∞) (((comap f μ : Measure α) : (a : Set α) → ℝ≥0∞) {a : α | ¬s a = t a} : ℝ≥0∞) (0 : ℝ≥0∞)
h_eq_α : {a : α | ¬s a = t a} = s \ t ∪ t \ s
x : β
h : ¬((f '' s) x ↔ (f '' t) x) → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₁ : x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s → ¬((f '' s) x ↔ (f '' t) x)
h₂ : ¬(f '' s) x → (f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₃ : ¬¬(f '' s) x → ¬(f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₄ : ¬(f '' s) x → (f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₅ : ¬¬(f '' s) x → ¬(f '' t) x → x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
h₆ : ¬(f '' s) x → (f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∈ f '' t
h₇ : ¬(f '' s) x → (f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∉ f '' s
h₈ : ¬¬(f '' s) x → ¬(f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∈ f '' t
h₉ : ¬¬(f '' s) x → ¬(f '' t) x → ¬(x ∈ f '' s ∧ x ∉ f '' t) → x ∉ f '' s
h₁₀ : x ∈ f '' s → x ∉ f '' t → ¬((f '' s) x ↔ (f '' t) x)
h₁₁ : x ∈ f '' t → x ∉ f '' s → ¬((f '' s) x ↔ (f '' t) x)
h₁₂ : x ∈ f '' s → x ∉ f '' t → ¬((f '' s) x ↔ (f '' t) x)
h₁₃ : x ∈ f '' t → x ∉ f '' s → ¬((f '' s) x ↔ (f '' t) x)
h₁₄ : x ∈ f '' s → x ∉ f '' t → ((f '' s) x ↔ (f '' t) x) → False
h₁₅ : x ∈ f '' t → x ∉ f '' s → ((f '' s) x ↔ (f '' t) x) → False
h₁₆ : (f '' s) x → ¬(f '' t) x → x ∉ f '' s → x ∈ f '' t
h₁₇ : (f '' s) x → ¬(f '' t) x → ¬x ∉ f '' t → x ∈ f '' t
h₁₈ : (f '' s) x → ¬(f '' t) x → x ∈ f '' s → x ∉ f '' s → False
⊢ ¬((f '' s) x ↔ (f '' t) x) ↔ x ∈ f '' s ∧ x ∉ f '' t ∨ x ∈ f '' t ∧ x ∉ f '' s
have h₁₉ : (f '' s) x → ¬(f '' t) x → x ∈ f '' s → ¬x ∉ f '' t → False
Tactic: tauto