harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/Configuration.lean
theorem HasLines.exists_bijective_of_card_eq [HasLines P L] [Fintype P] [Fintype L]
    (h : Fintype.card P = Fintype.card L) :
    ∃ f : L → P, Function.Bijective f ∧ ∀ l, pointCount P l = lineCount L (f l)

Proof state:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
⊢ ∃ f, Function.Bijective f ∧ ∀ (l : L), pointCount P l = lineCount L (f l)

Tactic:
obtain ⟨f, hf1, hf2⟩ := Nondegenerate.exists_injective_of_card_le (ge_of_eq h)

Result:
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
f : L → P
hf1 : Function.Injective f
hf2 : ∀ (l : L), f l ∉ l
⊢ ∃ f, Function.Bijective f ∧ ∀ (l : L), pointCount P l = lineCount L (f l)

Proof state:
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
f : L → P
hf1 : Function.Injective f
hf2 : ∀ (l : L), f l ∉ l
hf3 : Function.Bijective f
⊢ ∃ f, Function.Bijective f ∧ ∀ (l : L), pointCount P l = lineCount L (f l)

Tactic:
exact ⟨f, hf3, fun l ↦ (sum_eq_sum_iff_of_le fun l _ ↦ pointCount_le_lineCount (hf2 l)).1
      ((hf3.sum_comp _).trans (sum_lineCount_eq_sum_pointCount P L)).symm _ <| mem_univ _⟩

Result:
no goals

Proof state:
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
f : L → P
hf1 : Function.Injective f
hf2 : ∀ (l : L), f l ∉ l
⊢ ∃ f, Function.Bijective f ∧ ∀ (l : L), pointCount P l = lineCount L (f l)

Tactic:
have hf3 := (Fintype.bijective_iff_injective_and_card f).mpr ⟨hf1, h.symm⟩

Result:
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
f : L → P
hf1 : Function.Injective f
hf2 : ∀ (l : L), f l ∉ l
hf3 : Function.Bijective f
⊢ ∃ f, Function.Bijective f ∧ ∀ (l : L), pointCount P l = lineCount L (f l)

Proof state:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card P = Fintype.card L
⊢ ∃ f, Function.Bijective f ∧ ∀ (l : L), pointCount P l = lineCount L (f l)

Tactic:
classical
  obtain ⟨f, hf1, hf2⟩ := Nondegenerate.exists_injective_of_card_le (ge_of_eq h)
  have hf3 := (Fintype.bijective_iff_injective_and_card f).mpr ⟨hf1, h.symm⟩
  exact ⟨f, hf3, fun l ↦ (sum_eq_sum_iff_of_le fun l _ ↦ pointCount_le_lineCount (hf2 l)).1
        ((hf3.sum_comp _).trans (sum_lineCount_eq_sum_pointCount P L)).symm _ <| mem_univ _⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem append_of_mem {a : α} {l : Vector α n} (h : a ∈ l) :
    ∃ (m k : Nat) (w : m + 1 + k = n) (s : Vector α m) (t : Vector α k),
      l = (s.push a ++ t).cast w

Proof state:
α : Type u_1
a : α
l : Array α
h : a ∈ { toArray := l, size_toArray := ⋯ }
⊢ ?m.213753 ∈ ?m.213754

Tactic:
simpa using h

Result:
no goals

Proof state:
case mk
α : Type u_1
a : α
l : Array α
h : a ∈ { toArray := l, size_toArray := ⋯ }
⊢ ∃ m k w s t, { toArray := l, size_toArray := ⋯ } = Vector.cast w (s.push a ++ t)

Tactic:
obtain ⟨s, t, rfl⟩ := Array.append_of_mem (by simpa using h)

Result:
case mk.intro.intro
α : Type u_1
a : α
s t : Array α
h : a ∈ { toArray := s.push a ++ t, size_toArray := ⋯ }
⊢ ∃ m k w s_1 t_1, { toArray := s.push a ++ t, size_toArray := ⋯ } = Vector.cast w (s_1.push a ++ t_1)

Proof state:
α : Type u_1
a : α
s t : Array α
h : a ∈ { toArray := s.push a ++ t, size_toArray := ⋯ }
⊢ s.size + 1 + t.size = (s.push a ++ t).size

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : α
l : Vector α n
h : a ∈ l
⊢ ∃ m k w s t, l = Vector.cast w (s.push a ++ t)

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
a : α
l : Array α
h : a ∈ { toArray := l, size_toArray := ⋯ }
⊢ ∃ m k w s t, { toArray := l, size_toArray := ⋯ } = Vector.cast w (s.push a ++ t)

Proof state:
case mk.intro.intro
α : Type u_1
a : α
s t : Array α
h : a ∈ { toArray := s.push a ++ t, size_toArray := ⋯ }
⊢ ∃ m k w s_1 t_1, { toArray := s.push a ++ t, size_toArray := ⋯ } = Vector.cast w (s_1.push a ++ t_1)

Tactic:
refine ⟨_, _, by simp, s.toVector, t.toVector, by simp_all⟩

Result:
no goals

Proof state:
α : Type u_1
a : α
s t : Array α
h : a ∈ { toArray := s.push a ++ t, size_toArray := ⋯ }
⊢ { toArray := s.push a ++ t, size_toArray := ⋯ } = Vector.cast ⋯ (s.toVector.push a ++ t.toVector)

Tactic:
simp_all

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_le_ncard_diff_add_ncard (s t : Set α) (ht : t.Finite

Proof state:
α : Type u_1
s t : Set α
ht : autoParam t.Finite _auto✝
⊢ s.ncard ≤ (s \ t).ncard + t.ncard

Tactic:
rcases s.finite_or_infinite with hs | hs

Result:
case inl
α : Type u_1
s t : Set α
ht : autoParam t.Finite _auto✝
hs : s.Finite
⊢ s.ncard ≤ (s \ t).ncard + t.ncard

case inr
α : Type u_1
s t : Set α
ht : autoParam t.Finite _auto✝
hs : s.Infinite
⊢ s.ncard ≤ (s \ t).ncard + t.ncard

Proof state:
case inl
α : Type u_1
s t : Set α
ht : autoParam t.Finite _auto✝
hs : s.Finite
⊢ ↑s.ncard ≤ ↑(s \ t).ncard + ↑t.ncard

Tactic:
rw [ht.cast_ncard_eq, hs.cast_ncard_eq, hs.diff.cast_ncard_eq]

Result:
case inl
α : Type u_1
s t : Set α
ht : autoParam t.Finite _auto✝
hs : s.Finite
⊢ s.encard ≤ (s \ t).encard + t.encard

Proof state:
case inr
α : Type u_1
s t : Set α
ht : autoParam t.Finite _auto✝
hs : s.Infinite
⊢ s.ncard ≤ (s \ t).ncard + t.ncard

Tactic:
convert Nat.zero_le _

Result:
case h.e'_3
α : Type u_1
s t : Set α
ht : autoParam t.Finite _auto✝
hs : s.Infinite
⊢ s.ncard = 0

Proof state:
case inl
α : Type u_1
s t : Set α
ht : autoParam t.Finite _auto✝
hs : s.Finite
⊢ s.ncard ≤ (s \ t).ncard + t.ncard

Tactic:
to_encard_tac

Result:
case inl
α : Type u_1
s t : Set α
ht : autoParam t.Finite _auto✝
hs : s.Finite
⊢ ↑s.ncard ≤ ↑(s \ t).ncard + ↑t.ncard

Proof state:
case h.e'_3
α : Type u_1
s t : Set α
ht : autoParam t.Finite _auto✝
hs : s.Infinite
⊢ s.ncard = 0

Tactic:
rw [hs.ncard]

Result:
no goals

Proof state:
case inl
α : Type u_1
s t : Set α
ht : autoParam t.Finite _auto✝
hs : s.Finite
⊢ s.encard ≤ (s \ t).encard + t.encard

Tactic:
apply encard_le_encard_diff_add_encard

Result:
no goals
-- Mathlib/Data/Set/Subsingleton.lean
lemma eq_singleton_or_nontrivial (ha : a ∈ s) : s = {a} ∨ s.Nontrivial

Proof state:
α : Type u
a : α
s : Set α
ha : a ∈ s
⊢ s.Subsingleton ∨ s.Nontrivial

Tactic:
exact s.subsingleton_or_nontrivial

Result:
no goals

Proof state:
α : Type u
a : α
s : Set α
ha : a ∈ s
⊢ s = {a} ∨ s.Nontrivial

Tactic:
rw [← subsingleton_iff_singleton ha]

Result:
α : Type u
a : α
s : Set α
ha : a ∈ s
⊢ s.Subsingleton ∨ s.Nontrivial
-- Mathlib/LinearAlgebra/Dual.lean
theorem dualCopairing_nondegenerate (W : Subspace K V₁) : W.dualCopairing.Nondegenerate

Proof state:
case right
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ (dualCopairing W).SeparatingRight

Tactic:
rintro ⟨x⟩

Result:
case right.mk
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
y✝ : V₁ ⧸ W
x : V₁
⊢ (∀ (x_1 : ↥(dualAnnihilator W)), ((dualCopairing W) x_1) (Quot.mk (⇑(quotientRel W)) x) = 0) →
    Quot.mk (⇑(quotientRel W)) x = 0

Proof state:
case left
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ LinearMap.ker ↑(dualQuotEquivDualAnnihilator W).symm = ⊥

Tactic:
apply LinearEquiv.ker

Result:
no goals

Proof state:
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ (dualCopairing W).Nondegenerate

Tactic:
constructor

Result:
case left
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ (dualCopairing W).SeparatingLeft

case right
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ (dualCopairing W).SeparatingRight

Proof state:
case right.mk
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
y✝ : V₁ ⧸ W
x : V₁
⊢ (∀ (x_1 : ↥(dualAnnihilator W)), ((dualCopairing W) x_1) (Quot.mk (⇑(quotientRel W)) x) = 0) →
    Quot.mk (⇑(quotientRel W)) x = 0

Tactic:
simp only [Quotient.quot_mk_eq_mk, dualCopairing_apply, Quotient.mk_eq_zero]

Result:
case right.mk
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
y✝ : V₁ ⧸ W
x : V₁
⊢ (∀ (x_1 : ↥(dualAnnihilator W)), x_1 x = 0) → x ∈ W

Proof state:
case left
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ (dualCopairing W).SeparatingLeft

Tactic:
rw [LinearMap.separatingLeft_iff_ker_eq_bot, dualCopairing_eq]

Result:
case left
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ LinearMap.ker ↑(dualQuotEquivDualAnnihilator W).symm = ⊥

Proof state:
case right.mk
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
y✝ : V₁ ⧸ W
x : V₁
⊢ (∀ (x_1 : Dual K V₁) (h : x_1 ∈ dualAnnihilator W), ⟨x_1, h⟩ x = 0) → ∀ φ ∈ dualAnnihilator W, φ x = 0

Tactic:
exact id

Result:
no goals

Proof state:
case right.mk
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
y✝ : V₁ ⧸ W
x : V₁
⊢ (∀ (x_1 : ↥(dualAnnihilator W)), x_1 x = 0) → x ∈ W

Tactic:
rw [← forall_mem_dualAnnihilator_apply_eq_zero_iff, SetLike.forall]

Result:
case right.mk
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
y✝ : V₁ ⧸ W
x : V₁
⊢ (∀ (x_1 : Dual K V₁) (h : x_1 ∈ dualAnnihilator W), ⟨x_1, h⟩ x = 0) → ∀ φ ∈ dualAnnihilator W, φ x = 0
-- Mathlib/Algebra/Group/Defs.lean
theorem npowRec_eq_npowBinRec : @npowRecAuto = @npowBinRecAuto

Proof state:
case h.h.h.h.h
M : Type u_2
x✝¹ : Semigroup M
x✝ : One M
k : ℕ
m : M
⊢ npowRec k m = npowBinRec.go k 1 m

Tactic:
match k with
| 0 => rw [npowRec, npowBinRec.go, Nat.binaryRec_zero]
| k + 1 => rw [npowBinRec.go_spec, npowRec_eq]

Result:
no goals

Proof state:
case h.h.h.h.h
M : Type u_2
x✝¹ : Semigroup M
x✝ : One M
k : ℕ
m : M
⊢ npowRecAuto k m = npowBinRecAuto k m

Tactic:
rw [npowBinRecAuto, npowRecAuto, npowBinRec]

Result:
case h.h.h.h.h
M : Type u_2
x✝¹ : Semigroup M
x✝ : One M
k : ℕ
m : M
⊢ npowRec k m = npowBinRec.go k 1 m

Proof state:
⊢ @npowRecAuto = @npowBinRecAuto

Tactic:
funext M _ _ k m

Result:
case h.h.h.h.h
M : Type u_2
x✝¹ : Semigroup M
x✝ : One M
k : ℕ
m : M
⊢ npowRecAuto k m = npowBinRecAuto k m

Proof state:
M : Type u_2
x✝¹ : Semigroup M
x✝ : One M
k : ℕ
m : M
⊢ npowRec 0 m = npowBinRec.go 0 1 m

Tactic:
rw [npowRec, npowBinRec.go, Nat.binaryRec_zero]

Result:
no goals

Proof state:
M : Type u_2
x✝¹ : Semigroup M
x✝ : One M
k✝ : ℕ
m : M
k : ℕ
⊢ npowRec (k + 1) m = npowBinRec.go (k + 1) 1 m

Tactic:
rw [npowBinRec.go_spec, npowRec_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem umod_eq_of_lt {x y : BitVec w} (h : x < y) :
    x % y = x

Proof state:
case a
w : Nat
x y : BitVec w
h : x < y
⊢ (x % y).toNat = x.toNat

Tactic:
simp [Nat.mod_eq_of_lt h]

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
h : x < y
⊢ x % y = x

Tactic:
apply eq_of_toNat_eq

Result:
case a
w : Nat
x y : BitVec w
h : x < y
⊢ (x % y).toNat = x.toNat
-- Mathlib/NumberTheory/Dioph.lean
theorem div_dioph : DiophFn fun v => f v / g v :=
  have :
    Dioph fun v : Vector3 ℕ 3 =>
      v &2 = 0 ∧ v &0 = 0 ∨ v &0 * v &2 ≤ v &1 ∧ v &1 < (v &0 + 1) * v &2 :=
    (D&2 D= D.0 D∧ D&0 D= D.0) D∨ D&0 D* D&2 D≤ D&1 D∧ D&1 D< (D&0 D+ D.1) D* D&2
  diophFn_comp2 df dg <|
    (diophFn_vec _).2 <|
      ext this <|
        (vectorAll_iff_forall _).1 fun z x y =>
          show y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < (z + 1) * y ↔ x / y = z by
            refine Iff.trans ?_ eq_comm
            exact y.eq_zero_or_pos.elim
              (fun y0 => by
                rw [y0, Nat.div_zero]
                exact ⟨fun o => (o.resolve_right fun ⟨_, h2⟩ => Nat.not_lt_zero _ h2).right,
                  fun z0 => Or.inl ⟨rfl, z0⟩⟩)
              fun ypos =>
                Iff.trans ⟨fun o => o.resolve_left fun ⟨h1, _⟩ => Nat.ne_of_gt ypos h1, Or.inr⟩
                  (le_antisymm_iff.trans <| and_congr (Nat.le_div_iff_mul_le ypos) <|
                    Iff.trans ⟨lt_succ_of_le, le_of_lt_succ⟩ (div_lt_iff_lt_mul ypos)).symm

Proof state:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph fun v => v &2 = 0 ∧ v &0 = 0 ∨ v &0 * v &2 ≤ v &1 ∧ v &1 < (v &0 + 1) * v &2
z x y : ℕ
⊢ y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < (z + 1) * y ↔ x / y = z

Tactic:
refine Iff.trans ?_ eq_comm

Result:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph fun v => v &2 = 0 ∧ v &0 = 0 ∨ v &0 * v &2 ≤ v &1 ∧ v &1 < (v &0 + 1) * v &2
z x y : ℕ
⊢ y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < (z + 1) * y ↔ z = x / y

Proof state:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph fun v => v &2 = 0 ∧ v &0 = 0 ∨ v &0 * v &2 ≤ v &1 ∧ v &1 < (v &0 + 1) * v &2
z x y : ℕ
⊢ y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < (z + 1) * y ↔ z = x / y

Tactic:
exact y.eq_zero_or_pos.elim
  (fun y0 => by
    rw [y0, Nat.div_zero]
    exact ⟨fun o => (o.resolve_right fun ⟨_, h2⟩ => Nat.not_lt_zero _ h2).right,
      fun z0 => Or.inl ⟨rfl, z0⟩⟩)
  fun ypos =>
    Iff.trans ⟨fun o => o.resolve_left fun ⟨h1, _⟩ => Nat.ne_of_gt ypos h1, Or.inr⟩
      (le_antisymm_iff.trans <| and_congr (Nat.le_div_iff_mul_le ypos) <|
        Iff.trans ⟨lt_succ_of_le, le_of_lt_succ⟩ (div_lt_iff_lt_mul ypos)).symm

Result:
no goals

Proof state:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph fun v => v &2 = 0 ∧ v &0 = 0 ∨ v &0 * v &2 ≤ v &1 ∧ v &1 < (v &0 + 1) * v &2
z x y : ℕ
y0 : y = 0
⊢ y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < (z + 1) * y ↔ z = x / y

Tactic:
rw [y0, Nat.div_zero]

Result:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph fun v => v &2 = 0 ∧ v &0 = 0 ∨ v &0 * v &2 ≤ v &1 ∧ v &1 < (v &0 + 1) * v &2
z x y : ℕ
y0 : y = 0
⊢ 0 = 0 ∧ z = 0 ∨ z * 0 ≤ x ∧ x < (z + 1) * 0 ↔ z = 0

Proof state:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph fun v => v &2 = 0 ∧ v &0 = 0 ∨ v &0 * v &2 ≤ v &1 ∧ v &1 < (v &0 + 1) * v &2
z x y : ℕ
y0 : y = 0
⊢ 0 = 0 ∧ z = 0 ∨ z * 0 ≤ x ∧ x < (z + 1) * 0 ↔ z = 0

Tactic:
exact ⟨fun o => (o.resolve_right fun ⟨_, h2⟩ => Nat.not_lt_zero _ h2).right,
  fun z0 => Or.inl ⟨rfl, z0⟩⟩

Result:
no goals
-- Mathlib/Topology/Instances/ENat.lean
theorem continuousAt_sub {a b : ℕ∞} (h : a ≠ ⊤ ∨ b ≠ ⊤) :
    ContinuousAt (· - ·).uncurry (a, b)

Proof state:
a b✝ : ℕ∞
h : a ≠ ⊤ ∨ b✝ ≠ ⊤
b : ℕ
x✝ : ⊤ ≠ ⊤ ∨ ↑b ≠ ⊤
⊢ ∀ (n : ℕ), ∀ᶠ (a : ℕ∞) in 𝓝 ⊤, ↑b + ↑n < a

Tactic:
exact fun n ↦ lt_mem_nhds <| WithTop.coe_lt_top (b + n)

Result:
no goals

Proof state:
a✝ b : ℕ∞
h : a✝ ≠ ⊤ ∨ b ≠ ⊤
a : ℕ
x✝ : ↑a ≠ ⊤ ∨ ⊤ ≠ ⊤
this : ∀ᶠ (b : ℕ∞) in 𝓝 ⊤, ↑a - b = 0
⊢ ContinuousAt (Function.uncurry fun x1 x2 => x1 - x2) (↑a, ⊤)

Tactic:
simpa [ContinuousAt, nhds_prod_eq, tsub_eq_zero_of_le]

Result:
no goals

Proof state:
a✝ b : ℕ∞
h : a✝ ≠ ⊤ ∨ b ≠ ⊤
a : ℕ
x✝ : ↑a ≠ ⊤ ∨ ⊤ ≠ ⊤
⊢ ∀ᶠ (b : ℕ∞) in 𝓝 ⊤, ↑a - b = 0

Tactic:
filter_upwards [le_mem_nhds (WithTop.coe_lt_top a)] with b using tsub_eq_zero_of_le

Result:
no goals

Proof state:
a✝ b : ℕ∞
h : a✝ ≠ ⊤ ∨ b ≠ ⊤
a : ℕ
x✝ : ↑a ≠ ⊤ ∨ ⊤ ≠ ⊤
⊢ ContinuousAt (Function.uncurry fun x1 x2 => x1 - x2) (↑a, ⊤)

Tactic:
suffices ∀ᶠ b in 𝓝 ⊤, (a - b : ℕ∞) = 0 by
  simpa [ContinuousAt, nhds_prod_eq, tsub_eq_zero_of_le]

Result:
a✝ b : ℕ∞
h : a✝ ≠ ⊤ ∨ b ≠ ⊤
a : ℕ
x✝ : ↑a ≠ ⊤ ∨ ⊤ ≠ ⊤
⊢ ∀ᶠ (b : ℕ∞) in 𝓝 ⊤, ↑a - b = 0

Proof state:
a✝ b✝ : ℕ∞
h : a✝ ≠ ⊤ ∨ b✝ ≠ ⊤
a b : ℕ
x✝ : ↑a ≠ ⊤ ∨ ↑b ≠ ⊤
⊢ ContinuousAt (Function.uncurry fun x1 x2 => x1 - x2) (↑a, ↑b)

Tactic:
simp [ContinuousAt, nhds_prod_eq]

Result:
no goals
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem Step.sublist (H : Red.Step L₁ L₂) : L₂ <+ L₁

Proof state:
α : Type u
L₁ L₂ : List (α × Bool)
H : Step L₁ L₂
⊢ L₂ <+ L₁

Tactic:
cases H

Result:
case not
α : Type u
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ L₁✝ ++ L₂✝ <+ L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝

Proof state:
case not
α : Type u
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ L₁✝ ++ L₂✝ <+ L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Homotopy/Product.lean
theorem comp_prod_eq_prod_comp : prod q₁ q₂ ⬝ prod r₁ r₂ = prod (q₁ ⬝ r₁) (q₂ ⬝ r₂)

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
a✝ : Path a₁ a₂
b✝ : Path b₁ b₂
⊢ prod ⟦a✝⟧ ⟦b✝⟧ ⬝ prod r₁ r₂ = prod (⟦a✝⟧ ⬝ r₁) (⟦b✝⟧ ⬝ r₂)

Tactic:
induction r₁, r₂ using Quotient.inductionOn₂

Result:
case h.h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
a✝¹ : Path a₁ a₂
b✝¹ : Path b₁ b₂
a✝ : Path a₂ a₃
b✝ : Path b₂ b₃
⊢ prod ⟦a✝¹⟧ ⟦b✝¹⟧ ⬝ prod ⟦a✝⟧ ⟦b✝⟧ = prod (⟦a✝¹⟧ ⬝ ⟦a✝⟧) (⟦b✝¹⟧ ⬝ ⟦b✝⟧)

Proof state:
case h.h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
a✝¹ : Path a₁ a₂
b✝¹ : Path b₁ b₂
a✝ : Path a₂ a₃
b✝ : Path b₂ b₃
⊢ prod ⟦a✝¹⟧ ⟦b✝¹⟧ ⬝ prod ⟦a✝⟧ ⟦b✝⟧ = prod (⟦a✝¹⟧ ⬝ ⟦a✝⟧) (⟦b✝¹⟧ ⬝ ⟦b✝⟧)

Tactic:
simp only [prod_lift, ← Path.Homotopic.comp_lift, Path.trans_prod_eq_prod_trans]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
⊢ prod q₁ q₂ ⬝ prod r₁ r₂ = prod (q₁ ⬝ r₁) (q₂ ⬝ r₂)

Tactic:
induction q₁, q₂ using Quotient.inductionOn₂

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a₁ a₂ a₃ : α
b₁ b₂ b₃ : β
q₁ : Homotopic.Quotient a₁ a₂
q₂ : Homotopic.Quotient b₁ b₂
r₁ : Homotopic.Quotient a₂ a₃
r₂ : Homotopic.Quotient b₂ b₃
a✝ : Path a₁ a₂
b✝ : Path b₁ b₂
⊢ prod ⟦a✝⟧ ⟦b✝⟧ ⬝ prod r₁ r₂ = prod (⟦a✝⟧ ⬝ r₁) (⟦b✝⟧ ⬝ r₂)
-- Mathlib/Probability/Kernel/Proper.lean
/-- Auxiliary lemma for `IsProper.lintegral_mul` and
`IsProper.setLIntegral_eq_indicator_mul_lintegral`. -/
private lemma IsProper.lintegral_indicator_mul_indicator (hπ : IsProper π) (h𝓑𝓧 : 𝓑 ≤ 𝓧)
    (hA : MeasurableSet[𝓧] A) (hB : MeasurableSet[𝓑] B) :
    ∫⁻ x, B.indicator 1 x * A.indicator 1 x ∂(π x₀) =
      B.indicator 1 x₀ * ∫⁻ x, A.indicator 1 x ∂(π x₀)

Proof state:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∫⁻ (a : X) in B ∩ A, 1 a * 1 a ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (a : X) in A, 1 a ∂π x₀

Tactic:
simp only [MeasureTheory.lintegral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter,
  Pi.one_apply, one_mul]

Result:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hA : MeasurableSet A
hB : MeasurableSet B
⊢ (π x₀) (B ∩ A) = B.indicator 1 x₀ * (π x₀) A

Proof state:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∫⁻ (x : X), B.indicator 1 x * A.indicator 1 x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), A.indicator 1 x ∂π x₀

Tactic:
simp_rw [← inter_indicator_mul]

Result:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∫⁻ (x : X), (B ∩ A).indicator (fun j => 1 j * 1 j) x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), A.indicator 1 x ∂π x₀

Proof state:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hA : MeasurableSet A
hB : MeasurableSet B
⊢ (π x₀) (B ∩ A) = B.indicator 1 x₀ * (π x₀) A

Tactic:
rw [← hπ.inter_eq_indicator_mul h𝓑𝓧 hA hB, inter_comm]

Result:
no goals

Proof state:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∫⁻ (x : X), (B ∩ A).indicator (fun j => 1 j * 1 j) x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), A.indicator 1 x ∂π x₀

Tactic:
rw [lintegral_indicator ((h𝓑𝓧 _ hB).inter hA), lintegral_indicator hA]

Result:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∫⁻ (a : X) in B ∩ A, 1 a * 1 a ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (a : X) in A, 1 a ∂π x₀
-- Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
theorem norm_le_norm_mul_left (x : ℤ[i]) {y : ℤ[i]} (hy : y ≠ 0) :
    (norm x).natAbs ≤ (norm (x * y)).natAbs

Proof state:
x y : ℤ[i]
hy : y ≠ 0
⊢ ↑1 ≤ norm y

Tactic:
exact Int.add_one_le_of_lt (norm_pos.2 hy)

Result:
no goals

Proof state:
x y : ℤ[i]
hy : y ≠ 0
⊢ ↑1 ≤ ↑(norm y).natAbs

Tactic:
rw [abs_natCast_norm]

Result:
x y : ℤ[i]
hy : y ≠ 0
⊢ ↑1 ≤ norm y

Proof state:
x y : ℤ[i]
hy : y ≠ 0
⊢ (norm x).natAbs ≤ (norm (x * y)).natAbs

Tactic:
rw [Zsqrtd.norm_mul, Int.natAbs_mul]

Result:
x y : ℤ[i]
hy : y ≠ 0
⊢ (norm x).natAbs ≤ (norm x).natAbs * (norm y).natAbs

Proof state:
x y : ℤ[i]
hy : y ≠ 0
⊢ (norm x).natAbs ≤ (norm x).natAbs * (norm y).natAbs

Tactic:
exact le_mul_of_one_le_right (Nat.zero_le _) (Int.ofNat_le.1 (by
  rw [abs_natCast_norm]
  exact Int.add_one_le_of_lt (norm_pos.2 hy)))

Result:
no goals
-- Mathlib/RingTheory/PolynomialAlgebra.lean
theorem matPolyEquiv_symm_apply_coeff (p : (Matrix n n R)[X]) (i j : n) (k : ℕ) :
    coeff (matPolyEquiv.symm p i j) k = coeff p k i j

Proof state:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : (Matrix n n R)[X]
i j : n
k : ℕ
t : p = matPolyEquiv (matPolyEquiv.symm p)
⊢ (matPolyEquiv.symm p i j).coeff k = (matPolyEquiv (matPolyEquiv.symm p)).coeff k i j

Tactic:
simp only [matPolyEquiv_coeff_apply]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : (Matrix n n R)[X]
i j : n
k : ℕ
⊢ p = matPolyEquiv (matPolyEquiv.symm p)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : (Matrix n n R)[X]
i j : n
k : ℕ
⊢ (matPolyEquiv.symm p i j).coeff k = p.coeff k i j

Tactic:
have t : p = matPolyEquiv (matPolyEquiv.symm p) := by simp

Result:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : (Matrix n n R)[X]
i j : n
k : ℕ
t : p = matPolyEquiv (matPolyEquiv.symm p)
⊢ (matPolyEquiv.symm p i j).coeff k = p.coeff k i j

Proof state:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : (Matrix n n R)[X]
i j : n
k : ℕ
t : p = matPolyEquiv (matPolyEquiv.symm p)
⊢ (matPolyEquiv.symm p i j).coeff k = p.coeff k i j

Tactic:
conv_rhs => rw [t]

Result:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : (Matrix n n R)[X]
i j : n
k : ℕ
t : p = matPolyEquiv (matPolyEquiv.symm p)
⊢ (matPolyEquiv.symm p i j).coeff k = (matPolyEquiv (matPolyEquiv.symm p)).coeff k i j
-- Mathlib/Algebra/Category/Ring/Basic.lean
lemma comp_apply {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) (r : R) :
    (f ≫ g) r = g (f r)

Proof state:
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
r : ↑R
⊢ (ConcreteCategory.hom (f ≫ g)) r = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) r)

Tactic:
simp

Result:
no goals