harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/AdicCompletion/Functoriality.lean
theorem sumInv_comp_sum : sumInv I M ∘ₗ sum I M = LinearMap.id

Proof state:
case h
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
j : ι
x : AdicCauchySequence I (M j)
i : ι
n : ℕ
⊢ Submodule.Quotient.mk (if h : j = i then Eq.recOn h (↑x n) else 0) =
    ↑(if h : j = i then Eq.recOn h ((mk I (M j)) x) else 0) n

Tactic:
split

Result:
case h.isTrue
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
j : ι
x : AdicCauchySequence I (M j)
i : ι
n : ℕ
h✝ : j = i
⊢ Submodule.Quotient.mk (Eq.recOn h✝ (↑x n)) = ↑(Eq.recOn h✝ ((mk I (M j)) x)) n

case h.isFalse
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
j : ι
x : AdicCauchySequence I (M j)
i : ι
n : ℕ
h✝ : ¬j = i
⊢ Submodule.Quotient.mk 0 = ↑0 n
-- Mathlib/NumberTheory/FactorisationProperties.lean
theorem not_pseudoperfect_iff_forall :
    ¬ Pseudoperfect n ↔ n = 0 ∨ ∀ s ⊆ properDivisors n, ∑ i ∈ s, i ≠ n

Proof state:
n : ℕ
⊢ ¬n.Pseudoperfect ↔ n = 0 ∨ ∀ s ⊆ n.properDivisors, ∑ i ∈ s, i ≠ n

Tactic:
rw [Pseudoperfect, not_and_or]

Result:
n : ℕ
⊢ (¬0 < n ∨ ¬∃ s ⊆ n.properDivisors, ∑ i ∈ s, i = n) ↔ n = 0 ∨ ∀ s ⊆ n.properDivisors, ∑ i ∈ s, i ≠ n

Proof state:
n : ℕ
⊢ (¬0 < n ∨ ¬∃ s ⊆ n.properDivisors, ∑ i ∈ s, i = n) ↔ n = 0 ∨ ∀ s ⊆ n.properDivisors, ∑ i ∈ s, i ≠ n

Tactic:
simp only [not_lt, nonpos_iff_eq_zero, mem_powerset, not_exists, not_and, ne_eq]

Result:
no goals
-- Mathlib/Data/Finset/Sym.lean
theorem sym_eq_empty : s.sym n = ∅ ↔ n ≠ 0 ∧ s = ∅

Proof state:
case succ.intro
α : Type u_1
inst✝ : DecidableEq α
n✝ : ℕ
left✝ : n✝ + 1 ≠ 0
⊢ ∅.sym (n✝ + 1) = ∅

Tactic:
exact sym_empty _

Result:
no goals

Proof state:
case succ
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ : ℕ
⊢ n✝ + 1 ≠ 0 ∧ s = ∅ → s.sym (n✝ + 1) = ∅

Tactic:
rintro ⟨_, rfl⟩

Result:
case succ.intro
α : Type u_1
inst✝ : DecidableEq α
n✝ : ℕ
left✝ : n✝ + 1 ≠ 0
⊢ ∅.sym (n✝ + 1) = ∅

Proof state:
case succ
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ : ℕ
⊢ s.sym (n✝ + 1) = ∅ ↔ n✝ + 1 ≠ 0 ∧ s = ∅

Tactic:
refine ⟨fun h ↦ ⟨Nat.succ_ne_zero _, eq_empty_of_sym_eq_empty h⟩, ?_⟩

Result:
case succ
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ : ℕ
⊢ n✝ + 1 ≠ 0 ∧ s = ∅ → s.sym (n✝ + 1) = ∅

Proof state:
case zero
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ s.sym 0 = ∅ ↔ 0 ≠ 0 ∧ s = ∅

Tactic:
exact iff_of_false (singleton_ne_empty _) fun h ↦ (h.1 rfl).elim

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
⊢ s.sym n = ∅ ↔ n ≠ 0 ∧ s = ∅

Tactic:
cases n

Result:
case zero
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ s.sym 0 = ∅ ↔ 0 ≠ 0 ∧ s = ∅

case succ
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ : ℕ
⊢ s.sym (n✝ + 1) = ∅ ↔ n✝ + 1 ≠ 0 ∧ s = ∅
-- Mathlib/CategoryTheory/Action/Limits.lean
/-- `F : C ⥤ Action V G` preserves limits of some size
if it does after postcomposing with the forgetful functor `Action V G ⥤ V`. -/
lemma preservesLimitsOfSize_of_preserves (F : C ⥤ Action V G)
    (h : PreservesLimitsOfSize.{w₂, w₁} (F ⋙ Action.forget V G)) :
    PreservesLimitsOfSize.{w₂, w₁} F

Proof state:
case preservesLimitsOfShape
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
h : PreservesLimitsOfSize.{w₂, w₁, t₂, u, t₁, u + 1} (F ⋙ forget V G)
J : Type w₁
inst✝ : Category.{w₂, w₁} J
⊢ PreservesLimitsOfShape J F

Tactic:
apply Action.preservesLimitsOfShape_of_preserves

Result:
case preservesLimitsOfShape.h
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
h : PreservesLimitsOfSize.{w₂, w₁, t₂, u, t₁, u + 1} (F ⋙ forget V G)
J : Type w₁
inst✝ : Category.{w₂, w₁} J
⊢ PreservesLimitsOfShape J (F ⋙ forget V G)

Proof state:
case preservesLimitsOfShape
V : Type (u + 1)
inst✝² : LargeCategory V
G : Type u
inst✝¹ : Monoid G
C : Type t₁
inst✝ : Category.{t₂, t₁} C
F : C ⥤ Action V G
h : PreservesLimitsOfSize.{w₂, w₁, t₂, u, t₁, u + 1} (F ⋙ forget V G)
⊢ autoParam (∀ {J : Type w₁} [inst : Category.{w₂, w₁} J], PreservesLimitsOfShape J F) _auto✝

Tactic:
intro J _

Result:
case preservesLimitsOfShape
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
h : PreservesLimitsOfSize.{w₂, w₁, t₂, u, t₁, u + 1} (F ⋙ forget V G)
J : Type w₁
inst✝ : Category.{w₂, w₁} J
⊢ PreservesLimitsOfShape J F

Proof state:
case preservesLimitsOfShape.h
V : Type (u + 1)
inst✝³ : LargeCategory V
G : Type u
inst✝² : Monoid G
C : Type t₁
inst✝¹ : Category.{t₂, t₁} C
F : C ⥤ Action V G
h : PreservesLimitsOfSize.{w₂, w₁, t₂, u, t₁, u + 1} (F ⋙ forget V G)
J : Type w₁
inst✝ : Category.{w₂, w₁} J
⊢ PreservesLimitsOfShape J (F ⋙ forget V G)

Tactic:
exact PreservesLimitsOfSize.preservesLimitsOfShape

Result:
no goals

Proof state:
V : Type (u + 1)
inst✝² : LargeCategory V
G : Type u
inst✝¹ : Monoid G
C : Type t₁
inst✝ : Category.{t₂, t₁} C
F : C ⥤ Action V G
h : PreservesLimitsOfSize.{w₂, w₁, t₂, u, t₁, u + 1} (F ⋙ forget V G)
⊢ PreservesLimitsOfSize.{w₂, w₁, t₂, u, t₁, u + 1} F

Tactic:
constructor

Result:
case preservesLimitsOfShape
V : Type (u + 1)
inst✝² : LargeCategory V
G : Type u
inst✝¹ : Monoid G
C : Type t₁
inst✝ : Category.{t₂, t₁} C
F : C ⥤ Action V G
h : PreservesLimitsOfSize.{w₂, w₁, t₂, u, t₁, u + 1} (F ⋙ forget V G)
⊢ autoParam (∀ {J : Type w₁} [inst : Category.{w₂, w₁} J], PreservesLimitsOfShape J F) _auto✝
-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem adjugate_zero [Nontrivial n] : adjugate (0 : Matrix n n α) = 0

Proof state:
case a.intro
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Nontrivial n
i j j' : n
hj' : j' ≠ j
⊢ adjugate 0 i j = 0 i j

Tactic:
apply det_eq_zero_of_column_eq_zero j'

Result:
case a.intro
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Nontrivial n
i j j' : n
hj' : j' ≠ j
⊢ ∀ (i_1 : n), 0ᵀ.updateCol j (Pi.single i 1) i_1 j' = 0

Proof state:
case a.intro
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Nontrivial n
i j j' : n
hj' : j' ≠ j
j'' : n
⊢ 0ᵀ.updateCol j (Pi.single i 1) j'' j' = 0

Tactic:
simp [updateCol_ne hj']

Result:
no goals

Proof state:
case a
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Nontrivial n
i j : n
⊢ adjugate 0 i j = 0 i j

Tactic:
obtain ⟨j', hj'⟩ : ∃ j', j' ≠ j := exists_ne j

Result:
case a.intro
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Nontrivial n
i j j' : n
hj' : j' ≠ j
⊢ adjugate 0 i j = 0 i j

Proof state:
case a.intro
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Nontrivial n
i j j' : n
hj' : j' ≠ j
⊢ ∀ (i_1 : n), 0ᵀ.updateCol j (Pi.single i 1) i_1 j' = 0

Tactic:
intro j''

Result:
case a.intro
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Nontrivial n
i j j' : n
hj' : j' ≠ j
j'' : n
⊢ 0ᵀ.updateCol j (Pi.single i 1) j'' j' = 0

Proof state:
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Nontrivial n
⊢ adjugate 0 = 0

Tactic:
ext i j

Result:
case a
n : Type v
α : Type w
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : CommRing α
inst✝ : Nontrivial n
i j : n
⊢ adjugate 0 i j = 0 i j
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : ReadyForRupAdd f)
    (units : CNF.Clause (PosFin n)) :
    AssignmentsInvariant (insertRupUnits f units).1

Proof state:
case inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
units : CNF.Clause (PosFin n)
h :
  let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  InsertUnitInvariant f.assignments ⋯ rupUnits assignments hsize
hsize : (f.insertRupUnits units).fst.assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.insertRupUnits units).fst.assignments[i.val] = true
p : PosFin n → Bool
hp :
  ∀ (x : DefaultClause n),
    (some x ∈ (f.insertRupUnits units).fst.clauses.toList ∨
        (∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.rupUnits.toList ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.rupUnits.toList ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRupUnits units).fst.ratUnits.toList ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRupUnits units).fst.ratUnits.toList ∧ unit (a, true) = x) →
      ∃ a, (a, false) ∈ Clause.toList x ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList x ∧ p a = true
pf : p ⊨ f
j1 j2 : Fin (f.insertRupUnits units).fst.rupUnits.size
i_gt_zero : ↑⟨i.val, ⋯⟩ > 0
h1 : (f.insertRupUnits units).fst.rupUnits[↑j1] = (⟨i.val, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[↑j2] = (⟨i.val, ⋯⟩, false)
left✝¹ : (f.insertRupUnits units).fst.assignments[↑⟨i.val, ⋯⟩] = both
left✝ : f.assignments[↑⟨i.val, ⋯⟩] = unassigned
right✝ :
  ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
    k ≠ j1 → k ≠ j2 → (f.insertRupUnits units).fst.rupUnits[k].fst.val ≠ ↑⟨i.val, ⋯⟩
j1_unit : DefaultClause n := unit (f.insertRupUnits units).fst.rupUnits[j1]
j1_unit_def : j1_unit = unit (f.insertRupUnits units).fst.rupUnits[j1]
j1_unit_in_insertRupUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.toList ∧ unit (i, false) = j1_unit ∨
      (i, true) ∈ (f.insertRupUnits units).fst.rupUnits.toList ∧ unit (i, true) = j1_unit
j2_unit : DefaultClause n := unit (f.insertRupUnits units).fst.rupUnits[j2]
j2_unit_def : j2_unit = unit (f.insertRupUnits units).fst.rupUnits[j2]
j2_unit_in_insertRupUnits_res :
  ∃ i,
    (i, false) ∈ (f.insertRupUnits units).fst.rupUnits.toList ∧ unit (i, false) = j2_unit ∨
      (i, true) ∈ (f.insertRupUnits units).fst.rupUnits.toList ∧ unit (i, true) = j2_unit
i1 i2 : PosFin n
hp1 : i1 = ⟨i.val, ⋯⟩ ∧ p i1 = true
hp2 : p i1 = false
⊢ p ⊨ (i, b)

Tactic:
simp [hp1.2] at hp2

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem natDegree_comp_eq_of_mul_ne_zero (h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0) :
    natDegree (p.comp q) = natDegree p * natDegree q

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
hq : q.natDegree = 0
⊢ p.natDegree * q.natDegree ≤ (p.comp q).natDegree

Tactic:
simp [hq]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
hq : ¬q.natDegree = 0
⊢ (p.comp q).coeff (p.natDegree * q.natDegree) ≠ 0

Tactic:
rwa [coeff_comp_degree_mul_degree hq]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Tactic:
by_cases hq : natDegree q = 0

Result:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
hq : q.natDegree = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
hq : ¬q.natDegree = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
hq : ¬q.natDegree = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Tactic:
apply natDegree_eq_of_le_of_coeff_ne_zero natDegree_comp_le

Result:
case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
hq : ¬q.natDegree = 0
⊢ (p.comp q).coeff (p.natDegree * q.natDegree) ≠ 0

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
hq : q.natDegree = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Tactic:
exact le_antisymm natDegree_comp_le (by simp [hq])

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
@[simp]
lemma properDivisors_eq_empty : n.properDivisors = ∅ ↔ n ≤ 1

Proof state:
n : ℕ
⊢ n.properDivisors = ∅ ↔ n ≤ 1

Tactic:
rw [← not_nonempty_iff_eq_empty, nonempty_properDivisors, not_lt]

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem IsBasis.isBasis_sUnion {Xs : Set (Set α)} (hne : Xs.Nonempty)
    (h : ∀ X ∈ Xs, M.IsBasis I X) : M.IsBasis I (⋃₀ Xs)

Proof state:
α : Type u_1
M : Matroid α
I : Set α
Xs : Set (Set α)
hne : Xs.Nonempty
h : ∀ X ∈ Xs, M.IsBasis I X
⊢ M.IsBasis I (⋃ i, ↑i)

Tactic:
have := Iff.mpr nonempty_coe_sort hne

Result:
α : Type u_1
M : Matroid α
I : Set α
Xs : Set (Set α)
hne : Xs.Nonempty
h : ∀ X ∈ Xs, M.IsBasis I X
this : Nonempty ↑Xs
⊢ M.IsBasis I (⋃ i, ↑i)

Proof state:
α : Type u_1
M : Matroid α
I : Set α
Xs : Set (Set α)
hne : Xs.Nonempty
h : ∀ X ∈ Xs, M.IsBasis I X
⊢ M.IsBasis I (⋃₀ Xs)

Tactic:
rw [sUnion_eq_iUnion]

Result:
α : Type u_1
M : Matroid α
I : Set α
Xs : Set (Set α)
hne : Xs.Nonempty
h : ∀ X ∈ Xs, M.IsBasis I X
⊢ M.IsBasis I (⋃ i, ↑i)

Proof state:
α : Type u_1
M : Matroid α
I : Set α
Xs : Set (Set α)
hne : Xs.Nonempty
h : ∀ X ∈ Xs, M.IsBasis I X
this : Nonempty ↑Xs
⊢ M.IsBasis I (⋃ i, ↑i)

Tactic:
exact IsBasis.isBasis_iUnion _ fun X ↦ (h X X.prop)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem attach_filterMap {l : Array α} {f : α → Option β} :
    (l.filterMap f).attach = l.attach.filterMap
      fun ⟨x, h⟩ => (f x).pbind (fun b m => some ⟨b, mem_filterMap.mpr ⟨x, h, m⟩⟩)

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
toList✝ : List α
⊢ (filterMap f { toList := toList✝ }).attach =
    filterMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => (f x).pbind fun b m => some ⟨b, ⋯⟩)
      { toList := toList✝ }.attach

Tactic:
rw [attach_congr (List.filterMap_toArray f _)]

Result:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
toList✝ : List α
⊢ map (fun x => ⟨x.val, ⋯⟩) (List.filterMap f toList✝).toArray.attach =
    filterMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => (f x).pbind fun b m => some ⟨b, ⋯⟩)
      { toList := toList✝ }.attach

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
toList✝ : List α
⊢ map (fun x => ⟨x.val, ⋯⟩) (List.filterMap f toList✝).toArray.attach =
    filterMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => (f x).pbind fun b m => some ⟨b, ⋯⟩)
      { toList := toList✝ }.attach

Tactic:
simp [List.attach_filterMap, List.map_filterMap, Function.comp_def]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : α → Option β
⊢ (filterMap f l).attach =
    filterMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => (f x).pbind fun b m => some ⟨b, ⋯⟩)
      l.attach

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
toList✝ : List α
⊢ (filterMap f { toList := toList✝ }).attach =
    filterMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => (f x).pbind fun b m => some ⟨b, ⋯⟩)
      { toList := toList✝ }.attach
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
/-- Rectangles of countably spanning sets are countably spanning. -/
lemma IsCountablySpanning.prod {C : Set (Set α)} {D : Set (Set β)} (hC : IsCountablySpanning C)
    (hD : IsCountablySpanning D) : IsCountablySpanning (image2 (· ×ˢ ·) C D)

Proof state:
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ IsCountablySpanning (image2 (fun x1 x2 => x1 ×ˢ x2) C D)

Tactic:
rcases hC, hD with ⟨⟨s, h1s, h2s⟩, t, h1t, h2t⟩

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
s : ℕ → Set α
h1s : ∀ (n : ℕ), s n ∈ C
h2s : ⋃ n, s n = univ
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : ⋃ n, t n = univ
⊢ IsCountablySpanning (image2 (fun x1 x2 => x1 ×ˢ x2) C D)

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
s : ℕ → Set α
h1s : ∀ (n : ℕ), s n ∈ C
h2s : ⋃ n, s n = univ
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : ⋃ n, t n = univ
⊢ ⋃ n, (fun n => s (Nat.unpair n).1 ×ˢ t (Nat.unpair n).2) n = univ

Tactic:
rw [iUnion_unpair_prod, h2s, h2t, univ_prod_univ]

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
s : ℕ → Set α
h1s : ∀ (n : ℕ), s n ∈ C
h2s : ⋃ n, s n = univ
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : ⋃ n, t n = univ
⊢ IsCountablySpanning (image2 (fun x1 x2 => x1 ×ˢ x2) C D)

Tactic:
refine ⟨fun n => s n.unpair.1 ×ˢ t n.unpair.2, fun n => mem_image2_of_mem (h1s _) (h1t _), ?_⟩

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
s : ℕ → Set α
h1s : ∀ (n : ℕ), s n ∈ C
h2s : ⋃ n, s n = univ
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : ⋃ n, t n = univ
⊢ ⋃ n, (fun n => s (Nat.unpair n).1 ×ˢ t (Nat.unpair n).2) n = univ
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem natDegree_mul' (h : leadingCoeff p * leadingCoeff q ≠ 0) :
    natDegree (p * q) = natDegree p + natDegree q :=
  have hp : p ≠ 0 := mt leadingCoeff_eq_zero.2 fun h₁ => h <| by rw [h₁, zero_mul]
  have hq : q ≠ 0 := mt leadingCoeff_eq_zero.2 fun h₁ => h <| by rw [h₁, mul_zero]
  natDegree_eq_of_degree_eq_some <| by
    rw [degree_mul' h, Nat.cast_add, degree_eq_natDegree hp, degree_eq_natDegree hq]

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
h₁ : q.leadingCoeff = 0
⊢ p.leadingCoeff * q.leadingCoeff = 0

Tactic:
rw [h₁, mul_zero]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
h₁ : p.leadingCoeff = 0
⊢ p.leadingCoeff * q.leadingCoeff = 0

Tactic:
rw [h₁, zero_mul]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).degree = ↑(p.natDegree + q.natDegree)

Tactic:
rw [degree_mul' h, Nat.cast_add, degree_eq_natDegree hp, degree_eq_natDegree hq]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Split.lean
theorem coe_eq_of_mem_split_of_mem_le {y : ι → ℝ} (h₁ : J ∈ split I i x) (h₂ : y ∈ J)
    (h₃ : y i ≤ x) : (J : Set (ι → ℝ)) = ↑I ∩ { y | y i ≤ x }

Proof state:
ι : Type u_1
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ ↑I ∩ {y | x < y i}
h₃ : y i ≤ x
H : ↑J = ↑I ∩ {y | x < y i}
⊢ False

Tactic:
exact h₃.not_lt h₂.2

Result:
no goals

Proof state:
ι : Type u_1
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ J
h₃ : y i ≤ x
⊢ ↑J = ↑I ∩ {y | y i ≤ x}

Tactic:
refine (mem_split_iff'.1 h₁).resolve_right fun H => ?_

Result:
ι : Type u_1
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ J
h₃ : y i ≤ x
H : ↑J = ↑I ∩ {y | x < y i}
⊢ False

Proof state:
ι : Type u_1
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ J
h₃ : y i ≤ x
H : ↑J = ↑I ∩ {y | x < y i}
⊢ False

Tactic:
rw [← Box.mem_coe, H] at h₂

Result:
ι : Type u_1
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ ↑I ∩ {y | x < y i}
h₃ : y i ≤ x
H : ↑J = ↑I ∩ {y | x < y i}
⊢ False
-- Mathlib/Algebra/Module/Torsion.lean
theorem isTorsionBySet_singleton_iff : IsTorsionBySet R M {a} ↔ IsTorsionBy R M a

Proof state:
case mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
b : R
h : IsTorsionBy R M b
⊢ ↑⟨b, ⋯⟩ • x = 0

Tactic:
exact @h _

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
⊢ IsTorsionBySet R M {a} ↔ IsTorsionBy R M a

Tactic:
refine ⟨fun h x => @h _ ⟨_, Set.mem_singleton _⟩, fun h x => ?_⟩

Result:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
h : IsTorsionBy R M a
x : M
⊢ ∀ ⦃a_1 : ↑{a}⦄, ↑a_1 • x = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
h : IsTorsionBy R M a
x : M
⊢ ∀ ⦃a_1 : ↑{a}⦄, ↑a_1 • x = 0

Tactic:
rintro ⟨b, rfl : b = a⟩

Result:
case mk
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
b : R
h : IsTorsionBy R M b
⊢ ↑⟨b, ⋯⟩ • x = 0
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem uniformContinuousOn_iff_restrict [UniformSpace α] [UniformSpace β] {f : α → β} {s : Set α} :
    UniformContinuousOn f s ↔ UniformContinuous (s.restrict f)

Proof state:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
⊢ UniformContinuousOn f s ↔ UniformContinuous (s.restrict f)

Tactic:
delta UniformContinuousOn UniformContinuous

Result:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
⊢ Tendsto (fun x => (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (s ×ˢ s)) (𝓤 β) ↔
    Tendsto (fun x => (s.restrict f x.1, s.restrict f x.2)) (𝓤 ↑s) (𝓤 β)

Proof state:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
⊢ Tendsto (fun x => (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (s ×ˢ s)) (𝓤 β) ↔
    Tendsto (fun x => (s.restrict f x.1, s.restrict f x.2)) (𝓤 ↑s) (𝓤 β)

Tactic:
rw [← map_uniformity_set_coe, tendsto_map'_iff]

Result:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
⊢ Tendsto ((fun x => (f x.1, f x.2)) ∘ Prod.map Subtype.val Subtype.val) (𝓤 ↑s) (𝓤 β) ↔
    Tendsto (fun x => (s.restrict f x.1, s.restrict f x.2)) (𝓤 ↑s) (𝓤 β)

Proof state:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
⊢ Tendsto ((fun x => (f x.1, f x.2)) ∘ Prod.map Subtype.val Subtype.val) (𝓤 ↑s) (𝓤 β) ↔
    Tendsto (fun x => (s.restrict f x.1, s.restrict f x.2)) (𝓤 ↑s) (𝓤 β)

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Convex/Gauge.lean
theorem gauge_le_of_mem (ha : 0 ≤ a) (hx : x ∈ a • s) : gauge s x ≤ a

Proof state:
case inr
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x : E
a : ℝ
ha : 0 ≤ a
hx : x ∈ a • s
ha' : 0 < a
⊢ gauge s x ≤ a

Tactic:
exact csInf_le gauge_set_bddBelow ⟨ha', hx⟩

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x : E
a : ℝ
ha : 0 ≤ a
hx : x ∈ a • s
⊢ gauge s x ≤ a

Tactic:
obtain rfl | ha' := ha.eq_or_lt

Result:
case inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x : E
ha : 0 ≤ 0
hx : x ∈ 0 • s
⊢ gauge s x ≤ 0

case inr
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x : E
a : ℝ
ha : 0 ≤ a
hx : x ∈ a • s
ha' : 0 < a
⊢ gauge s x ≤ a

Proof state:
case inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x : E
ha : 0 ≤ 0
hx : x ∈ 0 • s
⊢ gauge s x ≤ 0

Tactic:
rw [mem_singleton_iff.1 (zero_smul_set_subset _ hx), gauge_zero]

Result:
no goals