harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Stream/Init.lean
theorem tail_interleave (s₁ s₂ : Stream' α) : tail (s₁ ⋈ s₂) = s₂ ⋈ tail s₁

Proof state:
α : Type u
s₁ s₂ : Stream' α
⊢ (corec
        (fun x =>
          match x with
          | (s₁, snd) => s₁.head)
        (fun x =>
          match x with
          | (s₁, s₂) => (s₂, s₁.tail))
        (s₁, s₂)).tail =
    corec
      (fun x =>
        match x with
        | (s₁, snd) => s₁.head)
      (fun x =>
        match x with
        | (s₁, s₂) => (s₂, s₁.tail))
      (s₂, s₁.tail)

Tactic:
rw [corec_eq]

Result:
α : Type u
s₁ s₂ : Stream' α
⊢ ((match (s₁, s₂) with
        | (s₁, snd) => s₁.head) ::
        corec
          (fun x =>
            match x with
            | (s₁, snd) => s₁.head)
          (fun x =>
            match x with
            | (s₁, s₂) => (s₂, s₁.tail))
          (match (s₁, s₂) with
          | (s₁, s₂) => (s₂, s₁.tail))).tail =
    corec
      (fun x =>
        match x with
        | (s₁, snd) => s₁.head)
      (fun x =>
        match x with
        | (s₁, s₂) => (s₂, s₁.tail))
      (s₂, s₁.tail)

Proof state:
α : Type u
s₁ s₂ : Stream' α
⊢ (s₁ ⋈ s₂).tail = s₂ ⋈ s₁.tail

Tactic:
unfold interleave corecOn

Result:
α : Type u
s₁ s₂ : Stream' α
⊢ (corec
        (fun x =>
          match x with
          | (s₁, snd) => s₁.head)
        (fun x =>
          match x with
          | (s₁, s₂) => (s₂, s₁.tail))
        (s₁, s₂)).tail =
    corec
      (fun x =>
        match x with
        | (s₁, snd) => s₁.head)
      (fun x =>
        match x with
        | (s₁, s₂) => (s₂, s₁.tail))
      (s₂, s₁.tail)

Proof state:
α : Type u
s₁ s₂ : Stream' α
⊢ ((match (s₁, s₂) with
        | (s₁, snd) => s₁.head) ::
        corec
          (fun x =>
            match x with
            | (s₁, snd) => s₁.head)
          (fun x =>
            match x with
            | (s₁, s₂) => (s₂, s₁.tail))
          (match (s₁, s₂) with
          | (s₁, s₂) => (s₂, s₁.tail))).tail =
    corec
      (fun x =>
        match x with
        | (s₁, snd) => s₁.head)
      (fun x =>
        match x with
        | (s₁, s₂) => (s₂, s₁.tail))
      (s₂, s₁.tail)

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/CharP/MixedCharZero.lean
theorem to_not_mixedCharZero (h : ∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I)) :
    ∀ p > 0, ¬MixedCharZero R p

Proof state:
case intro.intro
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
p : ℕ
p_pos : p > 0
hp_mixedChar : MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
hI_p : CharP (R ⧸ I) p
⊢ False

Tactic:
replace hI_zero : CharP (R ⧸ I) 0 := @CharP.ofCharZero _ _ (h I hI_ne_top)

Result:
case intro.intro
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
p : ℕ
p_pos : p > 0
hp_mixedChar : MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
hI_p : CharP (R ⧸ I) p
hI_zero : CharP (R ⧸ I) 0
⊢ False

Proof state:
case intro.intro
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
p : ℕ
p_pos : p > 0
hp_mixedChar : MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
hI_p : CharP (R ⧸ I) p
hI_zero : CharP (R ⧸ I) 0
⊢ False

Tactic:
exact absurd (CharP.eq (R ⧸ I) hI_p hI_zero) (ne_of_gt p_pos)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
⊢ ∀ p > 0, ¬MixedCharZero R p

Tactic:
intro p p_pos

Result:
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
p : ℕ
p_pos : p > 0
⊢ ¬MixedCharZero R p

Proof state:
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
p : ℕ
p_pos : p > 0
⊢ ¬MixedCharZero R p

Tactic:
by_contra hp_mixedChar

Result:
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
p : ℕ
p_pos : p > 0
hp_mixedChar : MixedCharZero R p
⊢ False

Proof state:
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
p : ℕ
p_pos : p > 0
hp_mixedChar : MixedCharZero R p
⊢ False

Tactic:
rcases hp_mixedChar.charP_quotient with ⟨I, hI_ne_top, hI_p⟩

Result:
case intro.intro
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
p : ℕ
p_pos : p > 0
hp_mixedChar : MixedCharZero R p
I : Ideal R
hI_ne_top : I ≠ ⊤
hI_p : CharP (R ⧸ I) p
⊢ False
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem length_mul_right_ne (w : W) : ℓ (t * w) ≠ ℓ w

Proof state:
case intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w✝ w : W
i : B
⊢ cs.lengthParity (w * cs.simple i * w⁻¹ * w✝) ≠ cs.lengthParity w✝

Tactic:
simp [lengthParity_simple]

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
⊢ cs.lengthParity (t * w) ≠ cs.lengthParity w

Tactic:
rcases ht with ⟨w, i, rfl⟩

Result:
case intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w✝ w : W
i : B
⊢ cs.lengthParity (w * cs.simple i * w⁻¹ * w✝) ≠ cs.lengthParity w✝

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
this : cs.lengthParity (t * w) ≠ cs.lengthParity w
⊢ cs.length (t * w) ≠ cs.length w

Tactic:
contrapose! this

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
this : cs.length (t * w) = cs.length w
⊢ cs.lengthParity (t * w) = cs.lengthParity w

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
⊢ cs.length (t * w) ≠ cs.length w

Tactic:
suffices cs.lengthParity (t * w) ≠ cs.lengthParity w by
  contrapose! this
  simp only [lengthParity_eq_ofAdd_length, this]

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
⊢ cs.lengthParity (t * w) ≠ cs.lengthParity w

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
this : cs.length (t * w) = cs.length w
⊢ cs.lengthParity (t * w) = cs.lengthParity w

Tactic:
simp only [lengthParity_eq_ofAdd_length, this]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
lemma pow_mul_eq_zero_of_le {a b : M₀} {m n : ℕ} (hmn : m ≤ n)
    (h : a ^ m * b = 0) : a ^ n * b = 0

Proof state:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
m n : ℕ
hmn : m ≤ n
h : a ^ m * b = 0
⊢ a ^ (n - m) * 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
m n : ℕ
hmn : m ≤ n
h : a ^ m * b = 0
⊢ a ^ n * b = 0

Tactic:
rw [show n = n - m + m by omega, pow_add, mul_assoc, h]

Result:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
m n : ℕ
hmn : m ≤ n
h : a ^ m * b = 0
⊢ a ^ (n - m) * 0 = 0

Proof state:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
m n : ℕ
hmn : m ≤ n
h : a ^ m * b = 0
⊢ n = n - m + m

Tactic:
omega

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Addition.lean
theorem embDomain_smul (f : Γ ↪o Γ') (r : R) (x : HahnSeries Γ R) :
    embDomain f (r • x) = r • embDomain f x

Proof state:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Semiring R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
r : R
x : HahnSeries Γ R
⊢ embDomain f (r • x) = r • embDomain f x

Tactic:
ext g

Result:
case coeff.h
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Semiring R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
r : R
x : HahnSeries Γ R
g : Γ'
⊢ (embDomain f (r • x)).coeff g = (r • embDomain f x).coeff g

Proof state:
case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Semiring R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
r : R
x : HahnSeries Γ R
g : Γ'
hg : g ∉ Set.range ⇑f
⊢ (embDomain f (r • x)).coeff g = (r • embDomain f x).coeff g

Tactic:
simp [embDomain_notin_range hg]

Result:
no goals

Proof state:
case pos.intro
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Semiring R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
r : R
x : HahnSeries Γ R
a : Γ
⊢ (embDomain f (r • x)).coeff (f a) = (r • embDomain f x).coeff (f a)

Tactic:
simp

Result:
no goals

Proof state:
case coeff.h
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Semiring R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
r : R
x : HahnSeries Γ R
g : Γ'
⊢ (embDomain f (r • x)).coeff g = (r • embDomain f x).coeff g

Tactic:
by_cases hg : g ∈ Set.range f

Result:
case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Semiring R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
r : R
x : HahnSeries Γ R
g : Γ'
hg : g ∈ Set.range ⇑f
⊢ (embDomain f (r • x)).coeff g = (r • embDomain f x).coeff g

case neg
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Semiring R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
r : R
x : HahnSeries Γ R
g : Γ'
hg : g ∉ Set.range ⇑f
⊢ (embDomain f (r • x)).coeff g = (r • embDomain f x).coeff g

Proof state:
case pos
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Semiring R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
r : R
x : HahnSeries Γ R
g : Γ'
hg : g ∈ Set.range ⇑f
⊢ (embDomain f (r • x)).coeff g = (r • embDomain f x).coeff g

Tactic:
obtain ⟨a, rfl⟩ := hg

Result:
case pos.intro
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Semiring R
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
r : R
x : HahnSeries Γ R
a : Γ
⊢ (embDomain f (r • x)).coeff (f a) = (r • embDomain f x).coeff (f a)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem all_eq_not_any_not (l : List α) (p : α → Bool) : l.all p = !l.any (!p .)

Proof state:
α : Type u_1
l : List α
p : α → Bool
⊢ l.all p = !l.any fun x => !p x

Tactic:
simp only [not_any_eq_all_not, Bool.not_not]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem node4L_size {l x m y r} (hm : Sized m) :
    size (@node4L α l x m y r) = size l + size m + size r + 2

Proof state:
case node
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : (node size✝ l✝ x✝ r✝).Sized
⊢ l.size + l✝.size + 1 + (r✝.size + r.size + 1) = l.size + size✝ + r.size + 1

Tactic:
simp [size, hm.1]

Result:
case node
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : (node size✝ l✝ x✝ r✝).Sized
⊢ ((match l with
          | nil => 0
          | node sz l x r => sz) +
          match l✝ with
          | nil => 0
          | node sz l x r => sz) +
        1 +
      (((match r✝ with
          | nil => 0
          | node sz l x r => sz) +
          match r with
          | nil => 0
          | node sz l x r => sz) +
        1) =
    ((match l with
          | nil => 0
          | node sz l x r => sz) +
          (((match l✝ with
              | nil => 0
              | node sz l x r => sz) +
              match r✝ with
              | nil => 0
              | node sz l x r => sz) +
            1) +
        match r with
        | nil => 0
        | node sz l x r => sz) +
      1

Proof state:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
hm : m.Sized
⊢ (l.node4L x m y r).size = l.size + m.size + r.size + 2

Tactic:
cases m <;> simp [node4L, node3L, node'] <;> [abel; (simp [size, hm.1]; abel)]

Result:
no goals

Proof state:
case node
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : (node size✝ l✝ x✝ r✝).Sized
⊢ ((match l with
          | nil => 0
          | node sz l x r => sz) +
          match l✝ with
          | nil => 0
          | node sz l x r => sz) +
        1 +
      (((match r✝ with
          | nil => 0
          | node sz l x r => sz) +
          match r with
          | nil => 0
          | node sz l x r => sz) +
        1) =
    ((match l with
          | nil => 0
          | node sz l x r => sz) +
          (((match l✝ with
              | nil => 0
              | node sz l x r => sz) +
              match r✝ with
              | nil => 0
              | node sz l x r => sz) +
            1) +
        match r with
        | nil => 0
        | node sz l x r => sz) +
      1

Tactic:
abel

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem EventuallyLE.sup_le [SemilatticeSup β] {l : Filter α} {f g h : α → β} (hf : f ≤ᶠ[l] h)
    (hg : g ≤ᶠ[l] h) : f ⊔ g ≤ᶠ[l] h

Proof state:
α : Type u
β : Type v
inst✝ : SemilatticeSup β
l : Filter α
f g h : α → β
hf : f ≤ᶠ[l] h
hg : g ≤ᶠ[l] h
⊢ f ⊔ g ≤ᶠ[l] h

Tactic:
filter_upwards [hf, hg] with x hfx hgx using _root_.sup_le hfx hgx

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem sum_sum {ι' : Type*} (μ : ι → ι' → Measure α) :
    (sum fun n => sum (μ n)) = sum (fun (p : ι × ι') ↦ μ p.1 p.2)

Proof state:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
ι' : Type u_8
μ : ι → ι' → Measure α
⊢ (sum fun n => sum (μ n)) = sum fun p => μ p.1 p.2

Tactic:
ext1 s hs

Result:
case h
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
ι' : Type u_8
μ : ι → ι' → Measure α
s : Set α
hs : MeasurableSet s
⊢ (sum fun n => sum (μ n)) s = (sum fun p => μ p.1 p.2) s

Proof state:
case h
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
ι' : Type u_8
μ : ι → ι' → Measure α
s : Set α
hs : MeasurableSet s
⊢ (sum fun n => sum (μ n)) s = (sum fun p => μ p.1 p.2) s

Tactic:
simp [sum_apply _ hs, ENNReal.tsum_prod']

Result:
no goals
-- Mathlib/Topology/DenseEmbedding.lean
theorem Filter.HasBasis.hasBasis_of_isDenseInducing [TopologicalSpace α] [TopologicalSpace β]
    [T3Space β] {ι : Type*} {s : ι → Set α} {p : ι → Prop} {x : α} (h : (𝓝 x).HasBasis p s)
    {f : α → β} (hf : IsDenseInducing f) : (𝓝 (f x)).HasBasis p fun i => closure <| f '' s i

Proof state:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
i : ι
hi : p i
hi' : closure (f '' s i) ⊆ T
⊢ T ∈ 𝓝 (f x)

Tactic:
suffices closure (f '' s i) ∈ 𝓝 (f x) by filter_upwards [this] using hi'

Result:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
i : ι
hi : p i
hi' : closure (f '' s i) ⊆ T
⊢ closure (f '' s i) ∈ 𝓝 (f x)

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
hT : ∃ i, p i ∧ closure (f '' s i) ⊆ T
⊢ T ∈ 𝓝 (f x)

Tactic:
obtain ⟨i, hi, hi'⟩ := hT

Result:
case refine_2.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
i : ι
hi : p i
hi' : closure (f '' s i) ⊆ T
⊢ T ∈ 𝓝 (f x)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : (𝓝 x).HasBasis p s
f : α → β
hf : IsDenseInducing f
⊢ (𝓝 (f x)).HasBasis p fun i => closure (f '' s i)

Tactic:
rw [Filter.hasBasis_iff] at h ⊢

Result:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
⊢ ∀ (t : Set β), t ∈ 𝓝 (f x) ↔ ∃ i, p i ∧ closure (f '' s i) ⊆ t
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
theorem Ring.inverse_eq_inv (a : G₀) : Ring.inverse a = a⁻¹

Proof state:
case inl
G₀ : Type u_3
inst✝ : GroupWithZero G₀
⊢ inverse 0 = 0⁻¹

Tactic:
simp

Result:
no goals

Proof state:
case inr
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
⊢ inverse a = a⁻¹

Tactic:
exact Ring.inverse_unit (Units.mk0 a ha)

Result:
no goals

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
⊢ inverse a = a⁻¹

Tactic:
obtain rfl | ha := eq_or_ne a 0

Result:
case inl
G₀ : Type u_3
inst✝ : GroupWithZero G₀
⊢ inverse 0 = 0⁻¹

case inr
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
⊢ inverse a = a⁻¹
-- Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean
theorem measurableSingletonClass_of_countablySeparated
    [MeasurableSpace α] [CountablySeparated α] :
    MeasurableSingletonClass α

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablySeparated α
f : α → ℕ → Bool
fmeas : Measurable f
finj : Injective f
⊢ MeasurableSingletonClass α

Tactic:
refine ⟨fun x ↦ ?_⟩

Result:
case intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablySeparated α
f : α → ℕ → Bool
fmeas : Measurable f
finj : Injective f
x : α
⊢ MeasurableSet {x}

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablySeparated α
⊢ MeasurableSingletonClass α

Tactic:
rcases measurable_injection_nat_bool_of_countablySeparated α with ⟨f, fmeas, finj⟩

Result:
case intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablySeparated α
f : α → ℕ → Bool
fmeas : Measurable f
finj : Injective f
⊢ MeasurableSingletonClass α

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablySeparated α
f : α → ℕ → Bool
fmeas : Measurable f
finj : Injective f
x : α
⊢ MeasurableSet (f ⁻¹' {f x})

Tactic:
exact fmeas <| MeasurableSet.singleton _

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablySeparated α
f : α → ℕ → Bool
fmeas : Measurable f
finj : Injective f
x : α
⊢ MeasurableSet {x}

Tactic:
rw [← finj.preimage_image {x}, image_singleton]

Result:
case intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablySeparated α
f : α → ℕ → Bool
fmeas : Measurable f
finj : Injective f
x : α
⊢ MeasurableSet (f ⁻¹' {f x})
-- Mathlib/Algebra/Order/Monovary.lean
@[to_additive (attr := simp)] lemma monovary_inv_left : Monovary f⁻¹ g ↔ Antivary f g

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : OrderedCommGroup α
inst✝ : OrderedCommGroup β
f : ι → α
g : ι → β
⊢ Monovary f⁻¹ g ↔ Antivary f g

Tactic:
simp [Monovary, Antivary]

Result:
no goals
-- Mathlib/Data/Fintype/Pi.lean
lemma eval_image_piFinset (t : ∀ a, Finset (δ a)) (a : α) [DecidableEq (δ a)]
    (ht : ∀ b, a ≠ b → (t b).Nonempty) : ((piFinset t).image fun f ↦ f a) = t a

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
a : α
inst✝ : DecidableEq (δ a)
x : δ a
h : x ∈ t a
f : (b : α) → a ≠ b → δ b
hf : ∀ (b : α) (a : a ≠ b), f b a ∈ t b
⊢ (fun b => if h : a = b then h ▸ x else f b h) a = x

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
a : α
inst✝ : DecidableEq (δ a)
ht : ∀ (b : α), a ≠ b → (t b).Nonempty
⊢ image (fun f => f a) (piFinset t) = t a

Tactic:
refine (eval_image_piFinset_subset _ _).antisymm fun x h ↦ mem_image.2 ?_

Result:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
a : α
inst✝ : DecidableEq (δ a)
ht : ∀ (b : α), a ≠ b → (t b).Nonempty
x : δ a
h : x ∈ t a
⊢ ∃ a_1 ∈ piFinset t, a_1 a = x

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
a : α
inst✝ : DecidableEq (δ a)
x : δ a
h : x ∈ t a
f : (b : α) → a ≠ b → δ b
hf : ∀ (b : α) (a : a ≠ b), f b a ∈ t b
⊢ ∃ a_1 ∈ piFinset t, a_1 a = x

Tactic:
exact ⟨fun b ↦ if h : a = b then h ▸ x else f _ h, by aesop, by simp⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
a : α
inst✝ : DecidableEq (δ a)
x : δ a
h : x ∈ t a
f : (b : α) → a ≠ b → δ b
hf : ∀ (b : α) (a : a ≠ b), f b a ∈ t b
⊢ (fun b => if h : a = b then h ▸ x else f b h) ∈ piFinset t

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
a : α
inst✝ : DecidableEq (δ a)
ht : ∀ (b : α), a ≠ b → (t b).Nonempty
x : δ a
h : x ∈ t a
⊢ ∃ a_1 ∈ piFinset t, a_1 a = x

Tactic:
choose f hf using ht

Result:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
a : α
inst✝ : DecidableEq (δ a)
x : δ a
h : x ∈ t a
f : (b : α) → a ≠ b → δ b
hf : ∀ (b : α) (a : a ≠ b), f b a ∈ t b
⊢ ∃ a_1 ∈ piFinset t, a_1 a = x
-- Mathlib/Order/Interval/Finset/Basic.lean
@[simp]
lemma nonempty_Iio : (Iio a).Nonempty ↔ ¬ IsMin a

Proof state:
α : Type u_2
a : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
⊢ (Iio a).Nonempty ↔ ¬IsMin a

Tactic:
simp [Finset.Nonempty]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem comap_isInducing_of_surjective (hf : Surjective f) : IsInducing (comap f) where
  eq_induced

Proof state:
case intro.intro.intro
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Surjective ⇑f
s : Set (PrimeSpectrum S)
F : Set R
hF : ⇑(comap f) ⁻¹' zeroLocus F = sᶜ
⊢ ∃ s_1, sᶜ = zeroLocus s_1

Tactic:
exact ⟨f '' F, hF.symm.trans (preimage_comap_zeroLocus f F)⟩

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Surjective ⇑f
⊢ zariskiTopology = TopologicalSpace.induced (⇑(comap f)) zariskiTopology

Tactic:
simp only [TopologicalSpace.ext_iff, ← isClosed_compl_iff, isClosed_iff_zeroLocus,
  isClosed_induced_iff]

Result:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Surjective ⇑f
⊢ ∀ (s : Set (PrimeSpectrum S)), (∃ s_1, sᶜ = zeroLocus s_1) ↔ ∃ t, (∃ s, t = zeroLocus s) ∧ ⇑(comap f) ⁻¹' t = sᶜ

Proof state:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Surjective ⇑f
s : Set (PrimeSpectrum S)
⊢ (∃ t, (∃ s, t = zeroLocus s) ∧ ⇑(comap f) ⁻¹' t = sᶜ) → ∃ s_1, sᶜ = zeroLocus s_1

Tactic:
rintro ⟨-, ⟨F, rfl⟩, hF⟩

Result:
case intro.intro.intro
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Surjective ⇑f
s : Set (PrimeSpectrum S)
F : Set R
hF : ⇑(comap f) ⁻¹' zeroLocus F = sᶜ
⊢ ∃ s_1, sᶜ = zeroLocus s_1

Proof state:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Surjective ⇑f
⊢ ∀ (s : Set (PrimeSpectrum S)), (∃ s_1, sᶜ = zeroLocus s_1) ↔ ∃ t, (∃ s, t = zeroLocus s) ∧ ⇑(comap f) ⁻¹' t = sᶜ

Tactic:
refine fun s =>
  ⟨fun ⟨F, hF⟩ =>
    ⟨zeroLocus (f ⁻¹' F), ⟨f ⁻¹' F, rfl⟩, by
      rw [preimage_comap_zeroLocus, Function.Surjective.image_preimage hf, hF]⟩,
    ?_⟩

Result:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Surjective ⇑f
s : Set (PrimeSpectrum S)
⊢ (∃ t, (∃ s, t = zeroLocus s) ∧ ⇑(comap f) ⁻¹' t = sᶜ) → ∃ s_1, sᶜ = zeroLocus s_1

Proof state:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Surjective ⇑f
s : Set (PrimeSpectrum S)
x✝ : ∃ s_1, sᶜ = zeroLocus s_1
F : Set S
hF : sᶜ = zeroLocus F
⊢ ⇑(comap f) ⁻¹' zeroLocus (⇑f ⁻¹' F) = sᶜ

Tactic:
rw [preimage_comap_zeroLocus, Function.Surjective.image_preimage hf, hF]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Iic_subset_Iic : Iic a ⊆ Iic b ↔ a ≤ b

Proof state:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
⊢ Iic a ⊆ Iic b ↔ a ≤ b

Tactic:
simp [← coe_subset]

Result:
no goals