harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Totient.lean
theorem totient_mul {m n : ℕ} (h : m.Coprime n) : φ (m * n) = φ m * φ n :=
  if hmn0 : m * n = 0 then by
    rcases Nat.mul_eq_zero.1 hmn0 with h | h <;>
      simp only [totient_zero, mul_zero, zero_mul, h]
  else by
    haveI : NeZero (m * n) := ⟨hmn0⟩
    haveI : NeZero m := ⟨left_ne_zero_of_mul hmn0⟩
    haveI : NeZero n := ⟨right_ne_zero_of_mul hmn0⟩
    simp only [← ZMod.card_units_eq_totient]
    rw [Fintype.card_congr (Units.mapEquiv (ZMod.chineseRemainder h).toMulEquiv).toEquiv,
      Fintype.card_congr (@MulEquiv.prodUnits (ZMod m) (ZMod n) _ _).toEquiv, Fintype.card_prod]

Proof state:
m n : ℕ
h : m.Coprime n
hmn0 : ¬m * n = 0
⊢ φ (m * n) = φ m * φ n

Tactic:
haveI : NeZero (m * n) := ⟨hmn0⟩

Result:
m n : ℕ
h : m.Coprime n
hmn0 : ¬m * n = 0
this : NeZero (m * n)
⊢ φ (m * n) = φ m * φ n

Proof state:
m n : ℕ
h : m.Coprime n
hmn0 : ¬m * n = 0
this : NeZero (m * n)
⊢ φ (m * n) = φ m * φ n

Tactic:
haveI : NeZero m := ⟨left_ne_zero_of_mul hmn0⟩

Result:
m n : ℕ
h : m.Coprime n
hmn0 : ¬m * n = 0
this✝ : NeZero (m * n)
this : NeZero m
⊢ φ (m * n) = φ m * φ n

Proof state:
m n : ℕ
h : m.Coprime n
hmn0 : ¬m * n = 0
this✝ : NeZero (m * n)
this : NeZero m
⊢ φ (m * n) = φ m * φ n

Tactic:
haveI : NeZero n := ⟨right_ne_zero_of_mul hmn0⟩

Result:
m n : ℕ
h : m.Coprime n
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
⊢ φ (m * n) = φ m * φ n

Proof state:
m n : ℕ
h : m.Coprime n
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
⊢ φ (m * n) = φ m * φ n

Tactic:
simp only [← ZMod.card_units_eq_totient]

Result:
m n : ℕ
h : m.Coprime n
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
⊢ Fintype.card (ZMod (m * n))ˣ = Fintype.card (ZMod m)ˣ * Fintype.card (ZMod n)ˣ

Proof state:
m n : ℕ
h : m.Coprime n
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
⊢ Fintype.card (ZMod (m * n))ˣ = Fintype.card (ZMod m)ˣ * Fintype.card (ZMod n)ˣ

Tactic:
rw [Fintype.card_congr (Units.mapEquiv (ZMod.chineseRemainder h).toMulEquiv).toEquiv,
  Fintype.card_congr (@MulEquiv.prodUnits (ZMod m) (ZMod n) _ _).toEquiv, Fintype.card_prod]

Result:
no goals

Proof state:
m n : ℕ
h : m.Coprime n
hmn0 : m * n = 0
⊢ φ (m * n) = φ m * φ n

Tactic:
rcases Nat.mul_eq_zero.1 hmn0 with h | h <;>
  simp only [totient_zero, mul_zero, zero_mul, h]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem degree_mul_of_mul_leadingCoeff_ne_zero {f g : MvPolynomial σ R}
    (hfg : m.leadingCoeff f * m.leadingCoeff g ≠ 0) :
    m.degree (f * g) = m.degree f + m.degree g

Proof state:
case a.hd
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hfg : m.leadingCoeff f * m.leadingCoeff g ≠ 0
⊢ m.degree f + m.degree g ∈ (f * g).support

Tactic:
rw [mem_support_iff, coeff_mul_of_degree_add]

Result:
case a.hd
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hfg : m.leadingCoeff f * m.leadingCoeff g ≠ 0
⊢ m.leadingCoeff f * m.leadingCoeff g ≠ 0

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hfg : m.leadingCoeff f * m.leadingCoeff g ≠ 0
⊢ m.degree (f * g) = m.degree f + m.degree g

Tactic:
apply m.toSyn.injective

Result:
case a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hfg : m.leadingCoeff f * m.leadingCoeff g ≠ 0
⊢ m.toSyn (m.degree (f * g)) = m.toSyn (m.degree f + m.degree g)

Proof state:
case a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hfg : m.leadingCoeff f * m.leadingCoeff g ≠ 0
⊢ m.toSyn (m.degree (f * g)) = m.toSyn (m.degree f + m.degree g)

Tactic:
apply le_antisymm degree_mul_le

Result:
case a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hfg : m.leadingCoeff f * m.leadingCoeff g ≠ 0
⊢ m.toSyn (m.degree f + m.degree g) ≤ m.toSyn (m.degree (f * g))

Proof state:
case a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hfg : m.leadingCoeff f * m.leadingCoeff g ≠ 0
⊢ m.toSyn (m.degree f + m.degree g) ≤ m.toSyn (m.degree (f * g))

Tactic:
apply le_degree

Result:
case a.hd
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hfg : m.leadingCoeff f * m.leadingCoeff g ≠ 0
⊢ m.degree f + m.degree g ∈ (f * g).support

Proof state:
case a.hd
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hfg : m.leadingCoeff f * m.leadingCoeff g ≠ 0
⊢ m.leadingCoeff f * m.leadingCoeff g ≠ 0

Tactic:
exact hfg

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean
theorem induction_on {C : Δ m → Prop} {A : Δ m} (hm : m ≠ 0)
    (h0 : ∀ A : Δ m, A.1 1 0 = 0 → 0 < A.1 0 0 → 0 ≤ A.1 0 1 → |(A.1 0 1)| < |(A.1 1 1)| → C A)
    (hS : ∀ B, C B → C (S • B)) (hT : ∀ B, C B → C (T • B)) : C A

Proof state:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
A : FixedDetMatrix (Fin 2) ℤ m
hm : m ≠ 0
h0 : ∀ (A : FixedDetMatrix (Fin 2) ℤ m), ↑A 1 0 = 0 → 0 < ↑A 0 0 → 0 ≤ ↑A 0 1 → |↑A 0 1| < |↑A 1 1| → C A
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
h_reduce : C (reduce A)
⊢ ∀ (A : FixedDetMatrix (Fin 2) ℤ m), C (reduce A) → C A

Tactic:
apply reduce_rec

Result:
case base
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
A : FixedDetMatrix (Fin 2) ℤ m
hm : m ≠ 0
h0 : ∀ (A : FixedDetMatrix (Fin 2) ℤ m), ↑A 1 0 = 0 → 0 < ↑A 0 0 → 0 ≤ ↑A 0 1 → |↑A 0 1| < |↑A 1 1| → C A
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
h_reduce : C (reduce A)
⊢ ∀ (A : FixedDetMatrix (Fin 2) ℤ m), ↑A 1 0 = 0 → C (reduce A) → C A

case step
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
A : FixedDetMatrix (Fin 2) ℤ m
hm : m ≠ 0
h0 : ∀ (A : FixedDetMatrix (Fin 2) ℤ m), ↑A 1 0 = 0 → 0 < ↑A 0 0 → 0 ≤ ↑A 0 1 → |↑A 0 1| < |↑A 1 1| → C A
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
h_reduce : C (reduce A)
⊢ ∀ (A : FixedDetMatrix (Fin 2) ℤ m), ↑A 1 0 ≠ 0 → (C (reduce (reduceStep A)) → C (reduceStep A)) → C (reduce A) → C A

Proof state:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
A : FixedDetMatrix (Fin 2) ℤ m
hm : m ≠ 0
h0 : ∀ (A : FixedDetMatrix (Fin 2) ℤ m), ↑A 1 0 = 0 → 0 < ↑A 0 0 → 0 ≤ ↑A 0 1 → |↑A 0 1| < |↑A 1 1| → C A
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
h_reduce : C (reduce A)
⊢ C A

Tactic:
suffices ∀ A : Δ m, C (reduce A) → C A from this _ h_reduce

Result:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
A : FixedDetMatrix (Fin 2) ℤ m
hm : m ≠ 0
h0 : ∀ (A : FixedDetMatrix (Fin 2) ℤ m), ↑A 1 0 = 0 → 0 < ↑A 0 0 → 0 ≤ ↑A 0 1 → |↑A 0 1| < |↑A 1 1| → C A
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
h_reduce : C (reduce A)
⊢ ∀ (A : FixedDetMatrix (Fin 2) ℤ m), C (reduce A) → C A

Proof state:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
A : FixedDetMatrix (Fin 2) ℤ m
hm : m ≠ 0
h0 : ∀ (A : FixedDetMatrix (Fin 2) ℤ m), ↑A 1 0 = 0 → 0 < ↑A 0 0 → 0 ≤ ↑A 0 1 → |↑A 0 1| < |↑A 1 1| → C A
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
⊢ C A

Tactic:
have h_reduce : C (reduce A) := by
  rcases reduce_mem_reps hm A with ⟨H1, H2, H3, H4⟩
  exact h0 _ H1 H2 H3 H4

Result:
m : ℤ
C : FixedDetMatrix (Fin 2) ℤ m → Prop
A : FixedDetMatrix (Fin 2) ℤ m
hm : m ≠ 0
h0 : ∀ (A : FixedDetMatrix (Fin 2) ℤ m), ↑A 1 0 = 0 → 0 < ↑A 0 0 → 0 ≤ ↑A 0 1 → |↑A 0 1| < |↑A 1 1| → C A
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (T • B)
h_reduce : C (reduce A)
⊢ C A
-- Mathlib/Data/List/Pairwise.lean
theorem Pairwise.rel_head_tail (h₁ : l.Pairwise R) (ha : a ∈ l.tail) :
    R (l.head <| ne_nil_of_mem <| mem_of_mem_tail ha) a

Proof state:
case nil
α : Type u_1
R : α → α → Prop
a : α
h₁ : Pairwise R []
ha : a ∈ [].tail
⊢ R ([].head ⋯) a

Tactic:
simp at ha

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
l : List α
a : α
h₁ : Pairwise R l
ha : a ∈ l.tail
⊢ R (l.head ⋯) a

Tactic:
cases l with
| nil => simp at ha
| cons b l => exact (pairwise_cons.1 h₁).1 a ha

Result:
no goals

Proof state:
case cons
α : Type u_1
R : α → α → Prop
a b : α
l : List α
h₁ : Pairwise R (b :: l)
ha : a ∈ (b :: l).tail
⊢ R ((b :: l).head ⋯) a

Tactic:
exact (pairwise_cons.1 h₁).1 a ha

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem find?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : List α)
    (H : ∀ (a : α), a ∈ xs → P a) (p : β → Bool) :
    (xs.pmap f H).find? p = (xs.attach.find? (fun ⟨a, m⟩ => p (f a (H a m)))).map fun ⟨a, m⟩ => f a (H a m)

Proof state:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
xs : List α
H : ∀ (a : α), a ∈ xs → P a
p : β → Bool
⊢ Option.map (fun x => f x.val ⋯) (find? (p ∘ fun x => f x.val ⋯) xs.attach) =
    Option.map (fun x => f x.val ⋯) (find? (fun x => p (f x.val ⋯)) xs.attach)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
xs : List α
H : ∀ (a : α), a ∈ xs → P a
p : β → Bool
⊢ find? p (pmap f xs H) =
    Option.map
      (fun x =>
        match x with
        | ⟨a, m⟩ => f a ⋯)
      (find?
        (fun x =>
          match x with
          | ⟨a, m⟩ => p (f a ⋯))
        xs.attach)

Tactic:
simp only [pmap_eq_map_attach, find?_map]

Result:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
xs : List α
H : ∀ (a : α), a ∈ xs → P a
p : β → Bool
⊢ Option.map (fun x => f x.val ⋯) (find? (p ∘ fun x => f x.val ⋯) xs.attach) =
    Option.map (fun x => f x.val ⋯) (find? (fun x => p (f x.val ⋯)) xs.attach)
-- Mathlib/RingTheory/Ideal/Quotient/Defs.lean
theorem lift_surjective_of_surjective {f : R →+* S} (H : ∀ a : R, a ∈ I → f a = 0)
    (hf : Function.Surjective f) : Function.Surjective (Ideal.Quotient.lift I f H)

Proof state:
R : Type u
inst✝² : Ring R
I : Ideal R
S : Type v
inst✝¹ : I.IsTwoSided
inst✝ : Semiring S
f : R →+* S
H : ∀ a ∈ I, f a = 0
hf : Function.Surjective ⇑f
⊢ Function.Surjective ⇑(lift I f H)

Tactic:
intro y

Result:
R : Type u
inst✝² : Ring R
I : Ideal R
S : Type v
inst✝¹ : I.IsTwoSided
inst✝ : Semiring S
f : R →+* S
H : ∀ a ∈ I, f a = 0
hf : Function.Surjective ⇑f
y : S
⊢ ∃ a, (lift I f H) a = y

Proof state:
case h
R : Type u
inst✝² : Ring R
I : Ideal R
S : Type v
inst✝¹ : I.IsTwoSided
inst✝ : Semiring S
f : R →+* S
H : ∀ a ∈ I, f a = 0
hf : Function.Surjective ⇑f
x : R
⊢ (lift I f H) ((mk I) x) = f x

Tactic:
simp only [Ideal.Quotient.lift_mk]

Result:
no goals

Proof state:
case intro
R : Type u
inst✝² : Ring R
I : Ideal R
S : Type v
inst✝¹ : I.IsTwoSided
inst✝ : Semiring S
f : R →+* S
H : ∀ a ∈ I, f a = 0
hf : Function.Surjective ⇑f
x : R
⊢ ∃ a, (lift I f H) a = f x

Tactic:
use Ideal.Quotient.mk I x

Result:
case h
R : Type u
inst✝² : Ring R
I : Ideal R
S : Type v
inst✝¹ : I.IsTwoSided
inst✝ : Semiring S
f : R →+* S
H : ∀ a ∈ I, f a = 0
hf : Function.Surjective ⇑f
x : R
⊢ (lift I f H) ((mk I) x) = f x

Proof state:
R : Type u
inst✝² : Ring R
I : Ideal R
S : Type v
inst✝¹ : I.IsTwoSided
inst✝ : Semiring S
f : R →+* S
H : ∀ a ∈ I, f a = 0
hf : Function.Surjective ⇑f
y : S
⊢ ∃ a, (lift I f H) a = y

Tactic:
obtain ⟨x, rfl⟩ := hf y

Result:
case intro
R : Type u
inst✝² : Ring R
I : Ideal R
S : Type v
inst✝¹ : I.IsTwoSided
inst✝ : Semiring S
f : R →+* S
H : ∀ a ∈ I, f a = 0
hf : Function.Surjective ⇑f
x : R
⊢ ∃ a, (lift I f H) a = f x
-- Mathlib/Data/List/ModifyLast.lean
theorem modifyLast_concat (f : α → α) (a : α) (l : List α) :
    modifyLast f (l ++ [a]) = l ++ [f a]

Proof state:
case cons
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ modifyLast f (head✝ :: tl ++ [a]) = head✝ :: tl ++ [f a]

Tactic:
simp only [cons_append, modifyLast]

Result:
case cons
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ modifyLast.go f (head✝ :: (tl ++ [a])) #[] = head✝ :: (tl ++ [f a])

Proof state:
α : Type u_1
f : α → α
a : α
l : List α
⊢ modifyLast f (l ++ [a]) = l ++ [f a]

Tactic:
cases l with
| nil =>
  simp only [nil_append, modifyLast, modifyLast.go, Array.toListAppend_eq, Array.toList_toArray]
| cons _ tl =>
  simp only [cons_append, modifyLast]
  rw [modifyLast.go]
  case x_3 => exact append_ne_nil_of_right_ne_nil tl (cons_ne_nil a [])
  rw [modifyLast.go_concat, Array.toListAppend_eq, Array.push_toList, Array.toList_toArray,
    nil_append, cons_append, nil_append, cons_inj_right]
  exact modifyLast_concat _ _ tl

Result:
no goals

Proof state:
case cons
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ modifyLast.go f (tl ++ [a]) #[] = tl ++ [f a]

Tactic:
exact modifyLast_concat _ _ tl

Result:
no goals

Proof state:
case cons
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ modifyLast.go f (tl ++ [a]) (#[].push head✝) = head✝ :: (tl ++ [f a])

case cons.x_3
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ tl ++ [a] = [] → False

Tactic:
case x_3 => exact append_ne_nil_of_right_ne_nil tl (cons_ne_nil a [])

Result:
case cons
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ modifyLast.go f (tl ++ [a]) (#[].push head✝) = head✝ :: (tl ++ [f a])

Proof state:
case nil
α : Type u_1
f : α → α
a : α
⊢ modifyLast f ([] ++ [a]) = [] ++ [f a]

Tactic:
simp only [nil_append, modifyLast, modifyLast.go, Array.toListAppend_eq, Array.toList_toArray]

Result:
no goals

Proof state:
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ tl ++ [a] = [] → False

Tactic:
exact append_ne_nil_of_right_ne_nil tl (cons_ne_nil a [])

Result:
no goals

Proof state:
case cons
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ modifyLast.go f (head✝ :: (tl ++ [a])) #[] = head✝ :: (tl ++ [f a])

Tactic:
rw [modifyLast.go]

Result:
case cons
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ modifyLast.go f (tl ++ [a]) (#[].push head✝) = head✝ :: (tl ++ [f a])

case cons.x_3
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ tl ++ [a] = [] → False

Proof state:
case cons
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ modifyLast.go f (tl ++ [a]) (#[].push head✝) = head✝ :: (tl ++ [f a])

Tactic:
rw [modifyLast.go_concat, Array.toListAppend_eq, Array.push_toList, Array.toList_toArray,
  nil_append, cons_append, nil_append, cons_inj_right]

Result:
case cons
α : Type u_1
f : α → α
a head✝ : α
tl : List α
⊢ modifyLast.go f (tl ++ [a]) #[] = tl ++ [f a]
-- Mathlib/Order/UpperLower/Basic.lean
theorem prod_eq_bot : s ×ˢ t = ⊥ ↔ s = ⊥ ∨ t = ⊥

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : LowerSet α
t : LowerSet β
⊢ ↑(s ×ˢ t) = ↑⊥ ↔ ↑s = ↑⊥ ∨ ↑t = ↑⊥

Tactic:
exact prod_eq_empty_iff

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : LowerSet α
t : LowerSet β
⊢ s ×ˢ t = ⊥ ↔ s = ⊥ ∨ t = ⊥

Tactic:
simp_rw [SetLike.ext'_iff]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : LowerSet α
t : LowerSet β
⊢ ↑(s ×ˢ t) = ↑⊥ ↔ ↑s = ↑⊥ ∨ ↑t = ↑⊥
-- Mathlib/RingTheory/Spectrum/Prime/Basic.lean
@[simp]
lemma zeroLocus_insert_zero (s : Set R) : zeroLocus (insert 0 s) = zeroLocus s

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set R
⊢ zeroLocus (insert 0 s) = zeroLocus s

Tactic:
rw [← Set.union_singleton, zeroLocus_union, zeroLocus_singleton_zero, Set.inter_univ]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem le_degree_of_ne_zero (h : coeff p n ≠ 0) : (n : WithBot ℕ) ≤ degree p

Proof state:
R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ ↑n ≤ p.degree

Tactic:
exact Finset.le_sup (mem_support_iff.2 h)

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem emultiplicity_add_eq_min {p a b : α}
    (h : emultiplicity p a ≠ emultiplicity p b) :
    emultiplicity p (a + b) = min (emultiplicity p a) (emultiplicity p b)

Proof state:
case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p b ≤ emultiplicity p a

Tactic:
exact le_of_lt hab

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
⊢ emultiplicity p (a + b) = emultiplicity p a ⊓ emultiplicity p b

Tactic:
rcases lt_trichotomy (emultiplicity p a) (emultiplicity p b) with (hab | _ | hab)

Result:
case inl
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p a < emultiplicity p b
⊢ emultiplicity p (a + b) = emultiplicity p a ⊓ emultiplicity p b

case inr.inl
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
h✝ : emultiplicity p a = emultiplicity p b
⊢ emultiplicity p (a + b) = emultiplicity p a ⊓ emultiplicity p b

case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (a + b) = emultiplicity p a ⊓ emultiplicity p b

Proof state:
case inl
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p a < emultiplicity p b
⊢ emultiplicity p (a + b) = emultiplicity p a ⊓ emultiplicity p b

Tactic:
rw [add_comm, emultiplicity_add_of_gt hab, min_eq_left]

Result:
case inl
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p a < emultiplicity p b
⊢ emultiplicity p a ≤ emultiplicity p b

Proof state:
case inl
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p a < emultiplicity p b
⊢ emultiplicity p a ≤ emultiplicity p b

Tactic:
exact le_of_lt hab

Result:
no goals

Proof state:
case inr.inl
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
h✝ : emultiplicity p a = emultiplicity p b
⊢ emultiplicity p (a + b) = emultiplicity p a ⊓ emultiplicity p b

Tactic:
contradiction

Result:
no goals

Proof state:
case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p (a + b) = emultiplicity p a ⊓ emultiplicity p b

Tactic:
rw [emultiplicity_add_of_gt hab, min_eq_right]

Result:
case inr.inr
α : Type u_1
inst✝ : Ring α
p a b : α
h : emultiplicity p a ≠ emultiplicity p b
hab : emultiplicity p b < emultiplicity p a
⊢ emultiplicity p b ≤ emultiplicity p a
-- Mathlib/Data/Set/Card/Arithmetic.lean
theorem exists_union_disjoint_cardinal_eq_iff (s : Set α) :
    Even (s.ncard) ↔ ∃ (t u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #t = #u

Proof state:
case mpr.intro.intro.intro.intro.inr
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #↑t = #↑u
hnfin : (t ∪ u).Infinite
⊢ Even (t ∪ u).ncard

Tactic:
simp [hnfin.ncard]

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro.inl
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #↑t = #↑u
hfin : t.Finite ∧ u.Finite
⊢ Even (t ∪ u).ncard

Tactic:
have hn : t.ncard = u.ncard := congrArg Cardinal.toNat hctu

Result:
case mpr.intro.intro.intro.intro.inl
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #↑t = #↑u
hfin : t.Finite ∧ u.Finite
hn : t.ncard = u.ncard
⊢ Even (t ∪ u).ncard

Proof state:
case mpr
α : Type u_1
s : Set α
⊢ (∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u) → Even s.ncard

Tactic:
rintro ⟨t, u, rfl, hdtu, hctu⟩

Result:
case mpr.intro.intro.intro.intro
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #↑t = #↑u
⊢ Even (t ∪ u).ncard

Proof state:
case mpr.intro.intro.intro.intro.inl
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #↑t = #↑u
hfin : (t ∪ u).Finite
⊢ Even (t ∪ u).ncard

Tactic:
rw [finite_union] at hfin

Result:
case mpr.intro.intro.intro.intro.inl
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #↑t = #↑u
hfin : t.Finite ∧ u.Finite
⊢ Even (t ∪ u).ncard

Proof state:
case mpr.intro.intro.intro.intro
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #↑t = #↑u
⊢ Even (t ∪ u).ncard

Tactic:
obtain hfin | hnfin := (t ∪ u).finite_or_infinite

Result:
case mpr.intro.intro.intro.intro.inl
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #↑t = #↑u
hfin : (t ∪ u).Finite
⊢ Even (t ∪ u).ncard

case mpr.intro.intro.intro.intro.inr
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #↑t = #↑u
hnfin : (t ∪ u).Infinite
⊢ Even (t ∪ u).ncard

Proof state:
case mpr.intro.intro.intro.intro.inl
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #↑t = #↑u
hfin : t.Finite ∧ u.Finite
hn : t.ncard = u.ncard
⊢ Even (t ∪ u).ncard

Tactic:
rw [ncard_union_eq hdtu hfin.1 hfin.2, hn]

Result:
case mpr.intro.intro.intro.intro.inl
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #↑t = #↑u
hfin : t.Finite ∧ u.Finite
hn : t.ncard = u.ncard
⊢ Even (u.ncard + u.ncard)

Proof state:
case mpr.intro.intro.intro.intro.inl
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #↑t = #↑u
hfin : t.Finite ∧ u.Finite
hn : t.ncard = u.ncard
⊢ Even (u.ncard + u.ncard)

Tactic:
exact Even.add_self u.ncard

Result:
no goals

Proof state:
α : Type u_1
s : Set α
⊢ Even s.ncard ↔ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

Tactic:
use exists_union_disjoint_cardinal_eq_of_even

Result:
case mpr
α : Type u_1
s : Set α
⊢ (∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u) → Even s.ncard
-- Mathlib/Algebra/Category/CoalgebraCat/ComonEquivalence.lean
theorem counit_tensorObj_tensorObj_right :
    Coalgebra.counit (R := R)
      (A := (CoalgebraCat.of R M ⊗ (CoalgebraCat.of R N ⊗ CoalgebraCat.of R P) : CoalgebraCat R))
      = Coalgebra.counit (A := M ⊗[R] (N ⊗[R] P))

Proof state:
R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
⊢ CoalgebraStruct.counit = CoalgebraStruct.counit

Tactic:
ext

Result:
case h
R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
x✝ : ↑(of R M ⊗ of R N ⊗ of R P).toModuleCat
⊢ CoalgebraStruct.counit x✝ = CoalgebraStruct.counit x✝

Proof state:
case h
R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
x✝ : ↑(of R M ⊗ of R N ⊗ of R P).toModuleCat
⊢ CoalgebraStruct.counit x✝ = CoalgebraStruct.counit x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Dynamics/Ergodic/MeasurePreserving.lean
theorem measure_preimage {f : α → β} (hf : MeasurePreserving f μa μb) {s : Set β}
    (hs : NullMeasurableSet s μb) : μa (f ⁻¹' s) = μb s

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
s : Set β
hs : NullMeasurableSet s (map f μa)
⊢ μa (f ⁻¹' s) = (map f μa) s

Tactic:
rw [map_apply₀ hf.1.aemeasurable hs]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
s : Set β
hs : NullMeasurableSet s μb
⊢ μa (f ⁻¹' s) = μb s

Tactic:
rw [← hf.map_eq] at hs ⊢

Result:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
s : Set β
hs : NullMeasurableSet s (map f μa)
⊢ μa (f ⁻¹' s) = (map f μa) s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem append_left_lt [LT α] {l₁ l₂ l₃ : List α} (h : l₂ < l₃) :
    l₁ ++ l₂ < l₁ ++ l₃

Proof state:
α : Type u_1
inst✝ : LT α
l₁ l₂ l₃ : List α
h : l₂ < l₃
⊢ l₁ ++ l₂ < l₁ ++ l₃

Tactic:
induction l₁ with
| nil => simp [h]
| cons a l₁ ih => simp [cons_lt_cons_iff, ih]

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : LT α
l₂ l₃ : List α
h : l₂ < l₃
a : α
l₁ : List α
ih : l₁ ++ l₂ < l₁ ++ l₃
⊢ a :: l₁ ++ l₂ < a :: l₁ ++ l₃

Tactic:
simp [cons_lt_cons_iff, ih]

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : LT α
l₂ l₃ : List α
h : l₂ < l₃
⊢ [] ++ l₂ < [] ++ l₃

Tactic:
simp [h]

Result:
no goals