harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma nonsingular_iff (P : Fin 3 → R) : W'.Nonsingular P ↔ W'.Equation P ∧
    (W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4) ≠ 0 ∨
      2 * P y + W'.a₁ * P x * P z + W'.a₃ * P z ^ 3 ≠ 0 ∨
      W'.a₁ * P x * P y + 3 * W'.a₃ * P y * P z ^ 2
        - (2 * W'.a₂ * P x ^ 2 * P z + 4 * W'.a₄ * P x * P z ^ 3 + 6 * W'.a₆ * P z ^ 5) ≠ 0)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ W'.Nonsingular P ↔
    W'.Equation P ∧
      (W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4) ≠ 0 ∨
        2 * P y + W'.a₁ * P x * P z + W'.a₃ * P z ^ 3 ≠ 0 ∨
          W'.a₁ * P x * P y + 3 * W'.a₃ * P y * P z ^ 2 -
              (2 * W'.a₂ * P x ^ 2 * P z + 4 * W'.a₄ * P x * P z ^ 3 + 6 * W'.a₆ * P z ^ 5) ≠
            0)

Tactic:
rw [Nonsingular, eval_polynomialX, eval_polynomialY, eval_polynomialZ]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem IsOpen.trans (ht : IsOpen t) (hs : IsOpen s) : IsOpen (t : Set X)

Proof state:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen s
s' : Set X
hs' : IsOpen s'
ht : IsOpen (s ↓∩ s')
⊢ IsOpen (s ∩ s')

Tactic:
exact hs.inter hs'

Result:
no goals

Proof state:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen s
s' : Set X
hs' : IsOpen s'
ht : IsOpen (s ↓∩ s')
⊢ IsOpen (Subtype.val '' s ↓∩ s')

Tactic:
rw [Subtype.image_preimage_coe]

Result:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen s
s' : Set X
hs' : IsOpen s'
ht : IsOpen (s ↓∩ s')
⊢ IsOpen (s ∩ s')

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
t : Set ↑s
ht : IsOpen t
hs : IsOpen s
⊢ IsOpen (Subtype.val '' t)

Tactic:
rcases isOpen_induced_iff.mp ht with ⟨s', hs', rfl⟩

Result:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen s
s' : Set X
hs' : IsOpen s'
ht : IsOpen (s ↓∩ s')
⊢ IsOpen (Subtype.val '' s ↓∩ s')
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ico_union_Ico (h₁ : min a b ≤ max c d) (h₂ : min c d ≤ max a b) :
    Ico a b ∪ Ico c d = Ico (min a c) (max b d)

Proof state:
case inl.inl
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
h₁ : a ≤ d
h₂ : c ≤ b
⊢ Ico a b ∪ Ico c d = Ico (a ⊓ c) (b ⊔ d)

Tactic:
exact Ico_union_Ico' h₂ h₁

Result:
no goals

Proof state:
case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : b ≤ a
hcd : d ≤ c
h₁ : b ≤ c
h₂ : d ≤ a
⊢ Ico a b ∪ Ico c d = Ico (a ⊓ c) (b ⊔ d)

Tactic:
simp [*]

Result:
no goals

Proof state:
case inl.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a ≤ b
hcd : d ≤ c
h₁ : a ≤ c
h₂ : d ≤ b
⊢ Ico a b ∪ Ico c d = Ico (a ⊓ c) (b ⊔ d)

case inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : b ≤ a
hcd : c ≤ d
h₁ : b ≤ d
h₂ : c ≤ a
⊢ Ico a b ∪ Ico c d = Ico (a ⊓ c) (b ⊔ d)

case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : b ≤ a
hcd : d ≤ c
h₁ : b ≤ c
h₂ : d ≤ a
⊢ Ico a b ∪ Ico c d = Ico (a ⊓ c) (b ⊔ d)

Tactic:
all_goals simp [*]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : a ⊓ b ≤ c ⊔ d
h₂ : c ⊓ d ≤ a ⊔ b
⊢ Ico a b ∪ Ico c d = Ico (a ⊓ c) (b ⊔ d)

Tactic:
rcases le_total a b with hab | hab <;> rcases le_total c d with hcd | hcd <;> simp [*] at h₁ h₂

Result:
case inl.inl
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
h₁ : a ≤ d
h₂ : c ≤ b
⊢ Ico a b ∪ Ico c d = Ico (a ⊓ c) (b ⊔ d)

case inl.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a ≤ b
hcd : d ≤ c
h₁ : a ≤ c
h₂ : d ≤ b
⊢ Ico a b ∪ Ico c d = Ico (a ⊓ c) (b ⊔ d)

case inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : b ≤ a
hcd : c ≤ d
h₁ : b ≤ d
h₂ : c ≤ a
⊢ Ico a b ∪ Ico c d = Ico (a ⊓ c) (b ⊔ d)

case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : b ≤ a
hcd : d ≤ c
h₁ : b ≤ c
h₂ : d ≤ a
⊢ Ico a b ∪ Ico c d = Ico (a ⊓ c) (b ⊔ d)
-- Mathlib/LinearAlgebra/Matrix/Block.lean
theorem blockTriangular_reindex_iff {b : n → α} {e : m ≃ n} :
    (reindex e e M).BlockTriangular b ↔ M.BlockTriangular (b ∘ e)

Proof state:
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
M : Matrix m m R
inst✝¹ : LT α
inst✝ : Zero R
b : n → α
e : m ≃ n
⊢ ((reindex e e) M).BlockTriangular b ↔ M.BlockTriangular (b ∘ ⇑e)

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Result:
case refine_1
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
M : Matrix m m R
inst✝¹ : LT α
inst✝ : Zero R
b : n → α
e : m ≃ n
h : ((reindex e e) M).BlockTriangular b
⊢ M.BlockTriangular (b ∘ ⇑e)

case refine_2
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
M : Matrix m m R
inst✝¹ : LT α
inst✝ : Zero R
b : n → α
e : m ≃ n
h : M.BlockTriangular (b ∘ ⇑e)
⊢ ((reindex e e) M).BlockTriangular b

Proof state:
case h.e'_7
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
M : Matrix m m R
inst✝¹ : LT α
inst✝ : Zero R
b : n → α
e : m ≃ n
h : M.BlockTriangular (b ∘ ⇑e)
⊢ b = (b ∘ ⇑e) ∘ ⇑e.symm

Tactic:
simp only [comp_assoc b e e.symm, Equiv.self_comp_symm, comp_id]

Result:
no goals

Proof state:
case refine_2
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
M : Matrix m m R
inst✝¹ : LT α
inst✝ : Zero R
b : n → α
e : m ≃ n
h : M.BlockTriangular (b ∘ ⇑e)
⊢ ((reindex e e) M).BlockTriangular b

Tactic:
convert h.submatrix

Result:
case h.e'_7
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
M : Matrix m m R
inst✝¹ : LT α
inst✝ : Zero R
b : n → α
e : m ≃ n
h : M.BlockTriangular (b ∘ ⇑e)
⊢ b = (b ∘ ⇑e) ∘ ⇑e.symm

Proof state:
case h.e'_6
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
M : Matrix m m R
inst✝¹ : LT α
inst✝ : Zero R
b : n → α
e : m ≃ n
h : ((reindex e e) M).BlockTriangular b
⊢ M = ((reindex e e) M).submatrix ⇑e ⇑e

Tactic:
simp only [reindex_apply, submatrix_submatrix, submatrix_id_id, Equiv.symm_comp_self]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
M : Matrix m m R
inst✝¹ : LT α
inst✝ : Zero R
b : n → α
e : m ≃ n
h : ((reindex e e) M).BlockTriangular b
⊢ M.BlockTriangular (b ∘ ⇑e)

Tactic:
convert h.submatrix

Result:
case h.e'_6
α : Type u_1
m : Type u_3
n : Type u_4
R : Type v
M : Matrix m m R
inst✝¹ : LT α
inst✝ : Zero R
b : n → α
e : m ≃ n
h : ((reindex e e) M).BlockTriangular b
⊢ M = ((reindex e e) M).submatrix ⇑e ⇑e
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem roots_list_prod (L : List R[X]) :
    (0 : R[X]) ∉ L → L.prod.roots = (L : Multiset R[X]).bind roots :=
  List.recOn L (fun _ => roots_one) fun hd tl ih H => by
    rw [List.mem_cons, not_or] at H
    rw [List.prod_cons, roots_mul (mul_ne_zero (Ne.symm H.1) <| List.prod_ne_zero H.2), ←
      Multiset.cons_coe, Multiset.cons_bind, ih H.2]

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
L : List R[X]
hd : R[X]
tl : List R[X]
ih : 0 ∉ tl → tl.prod.roots = (↑tl).bind roots
H : ¬0 = hd ∧ 0 ∉ tl
⊢ (hd :: tl).prod.roots = (↑(hd :: tl)).bind roots

Tactic:
rw [List.prod_cons, roots_mul (mul_ne_zero (Ne.symm H.1) <| List.prod_ne_zero H.2), ←
  Multiset.cons_coe, Multiset.cons_bind, ih H.2]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
L : List R[X]
hd : R[X]
tl : List R[X]
ih : 0 ∉ tl → tl.prod.roots = (↑tl).bind roots
H : 0 ∉ hd :: tl
⊢ (hd :: tl).prod.roots = (↑(hd :: tl)).bind roots

Tactic:
rw [List.mem_cons, not_or] at H

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
L : List R[X]
hd : R[X]
tl : List R[X]
ih : 0 ∉ tl → tl.prod.roots = (↑tl).bind roots
H : ¬0 = hd ∧ 0 ∉ tl
⊢ (hd :: tl).prod.roots = (↑(hd :: tl)).bind roots
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_alter_eq_add_one [LawfulBEq α] {k : α} {f : Option β → Option β}
    (h : m.WF) (h₁ : k ∉ m) (h₂ : (f (Const.get? m k)).isSome) :
    (Const.alter m k f).size = m.size + 1

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝ : LawfulBEq α
k : α
f : Option β → Option β
h : m.WF
h₁ : ¬k ∈ m
h₂ : (f (get? m k)).isSome = true
⊢ (alter m k f).size = m.size + 1

Tactic:
revert h₁ h₂

Result:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝ : LawfulBEq α
k : α
f : Option β → Option β
h : m.WF
⊢ ¬k ∈ m → (f (get? m k)).isSome = true → (alter m k f).size = m.size + 1

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝ : LawfulBEq α
k : α
f : Option β → Option β
h : m.WF
⊢ ¬k ∈ m → (f (get? m k)).isSome = true → (alter m k f).size = m.size + 1

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝ : LawfulBEq α
k : α
f : Option β → Option β
h : m.WF
⊢ m.contains k = false → (f (get? m k)).isSome = true → (alter m k f).size = m.size + 1

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝ : LawfulBEq α
k : α
f : Option β → Option β
h : m.WF
⊢ m.contains k = false → (f (get? m k)).isSome = true → (alter m k f).size = m.size + 1

Tactic:
simp_to_raw using Raw₀.Const.size_alter_eq_add_one

Result:
no goals
-- Mathlib/Analysis/Subadditive.lean
theorem apply_mul_add_le (k n r) : u (k * n + r) ≤ k * u n + u r

Proof state:
case zero
u : ℕ → ℝ
h : Subadditive u
n r : ℕ
⊢ u (0 * n + r) ≤ ↑0 * u n + u r

Tactic:
simp only [Nat.cast_zero, zero_mul, zero_add]

Result:
case zero
u : ℕ → ℝ
h : Subadditive u
n r : ℕ
⊢ u r ≤ u r

Proof state:
case succ
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ ↑k * u n + u r
⊢ u ((k + 1) * n + r) ≤ ↑(k + 1) * u n + u r

Tactic:
calc
  u ((k + 1) * n + r) = u (n + (k * n + r)) := by congr 1; ring
  _ ≤ u n + u (k * n + r) := h _ _
  _ ≤ u n + (k * u n + u r) := add_le_add_left IH _
  _ = (k + 1 : ℕ) * u n + u r := by simp; ring

Result:
no goals

Proof state:
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ ↑k * u n + u r
⊢ u ((k + 1) * n + r) = u (n + (k * n + r))

Tactic:
congr 1

Result:
case e_a
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ ↑k * u n + u r
⊢ (k + 1) * n + r = n + (k * n + r)

Proof state:
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ ↑k * u n + u r
⊢ u n + (↑k * u n + u r) = ↑(k + 1) * u n + u r

Tactic:
simp

Result:
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ ↑k * u n + u r
⊢ u n + (↑k * u n + u r) = (↑k + 1) * u n + u r

Proof state:
u : ℕ → ℝ
h : Subadditive u
k n r : ℕ
⊢ u (k * n + r) ≤ ↑k * u n + u r

Tactic:
induction k with
| zero => simp only [Nat.cast_zero, zero_mul, zero_add]; rfl
| succ k IH =>
  calc
    u ((k + 1) * n + r) = u (n + (k * n + r)) := by congr 1; ring
    _ ≤ u n + u (k * n + r) := h _ _
    _ ≤ u n + (k * u n + u r) := add_le_add_left IH _
    _ = (k + 1 : ℕ) * u n + u r := by simp; ring

Result:
no goals

Proof state:
case zero
u : ℕ → ℝ
h : Subadditive u
n r : ℕ
⊢ u r ≤ u r

Tactic:
rfl

Result:
no goals

Proof state:
case e_a
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ ↑k * u n + u r
⊢ (k + 1) * n + r = n + (k * n + r)

Tactic:
ring

Result:
no goals

Proof state:
u : ℕ → ℝ
h : Subadditive u
n r k : ℕ
IH : u (k * n + r) ≤ ↑k * u n + u r
⊢ u n + (↑k * u n + u r) = (↑k + 1) * u n + u r

Tactic:
ring

Result:
no goals
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem not_bddAbove_fp_bfamily (H : ∀ i hi, IsNormal (f i hi)) :
    ¬ BddAbove (⋂ (i) (hi), Function.fixedPoints (f i hi))

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
⊢ ∀ (x : Ordinal.{max u v}), ∃ y ∈ ⋂ i, ⋂ (hi : i < o), fixedPoints (f i hi), x < y

Tactic:
refine fun a ↦ ⟨nfpBFamily _ f (succ a), ?_, (lt_succ a).trans_le (le_nfpBFamily f _)⟩

Result:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ o.nfpBFamily f (succ a) ∈ ⋂ i, ⋂ (hi : i < o), fixedPoints (f i hi)

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ o.nfpBFamily f (succ a) ∈ ⋂ i, ⋂ (hi : i < o), fixedPoints (f i hi)

Tactic:
rw [Set.mem_iInter₂]

Result:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ ∀ (i : Ordinal.{u}) (j : i < o), o.nfpBFamily f (succ a) ∈ fixedPoints (f i j)

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
⊢ ¬BddAbove (⋂ i, ⋂ (hi : i < o), fixedPoints (f i hi))

Tactic:
rw [not_bddAbove_iff]

Result:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
⊢ ∀ (x : Ordinal.{max u v}), ∃ y ∈ ⋂ i, ⋂ (hi : i < o), fixedPoints (f i hi), x < y

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ ∀ (i : Ordinal.{u}) (j : i < o), o.nfpBFamily f (succ a) ∈ fixedPoints (f i j)

Tactic:
exact fun i hi ↦ nfpBFamily_fp (H i hi) _

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma succ_div_of_not_dvd (hba : ¬b ∣ a + 1) : (a + 1) / b = a / b

Proof state:
a b : ℕ
hba : ¬b ∣ a + 1
⊢ (a + 1) / b = a / b

Tactic:
rw [succ_div, if_neg hba, Nat.add_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem shiftLeft_add_distrib {x y : BitVec w} {n : Nat} :
    (x + y) <<< n = x <<< n + y <<< n

Proof state:
w : Nat
x y : BitVec w
⊢ (x + y) <<< 0 = x <<< 0 + y <<< 0

Tactic:
simp

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
n : Nat
ih : (x + y) <<< n = x <<< n + y <<< n
⊢ (x + y) <<< (n + 1) = x <<< (n + 1) + y <<< (n + 1)

Tactic:
simp [ih, toNat_eq, Nat.shiftLeft_eq, ← Nat.add_mul]

Result:
no goals

Proof state:
case succ
w : Nat
x y : BitVec w
n✝ : Nat
a✝ : (x + y) <<< n✝ = x <<< n✝ + y <<< n✝
⊢ (x + y) <<< (n✝ + 1) = x <<< (n✝ + 1) + y <<< (n✝ + 1)

Tactic:
case succ n ih =>
  simp [ih, toNat_eq, Nat.shiftLeft_eq, ← Nat.add_mul]

Result:
no goals

Proof state:
case zero
w : Nat
x y : BitVec w
⊢ (x + y) <<< 0 = x <<< 0 + y <<< 0

case succ
w : Nat
x y : BitVec w
n✝ : Nat
a✝ : (x + y) <<< n✝ = x <<< n✝ + y <<< n✝
⊢ (x + y) <<< (n✝ + 1) = x <<< (n✝ + 1) + y <<< (n✝ + 1)

Tactic:
case zero =>
  simp

Result:
case succ
w : Nat
x y : BitVec w
n✝ : Nat
a✝ : (x + y) <<< n✝ = x <<< n✝ + y <<< n✝
⊢ (x + y) <<< (n✝ + 1) = x <<< (n✝ + 1) + y <<< (n✝ + 1)

Proof state:
w : Nat
x y : BitVec w
n : Nat
⊢ (x + y) <<< n = x <<< n + y <<< n

Tactic:
induction n

Result:
case zero
w : Nat
x y : BitVec w
⊢ (x + y) <<< 0 = x <<< 0 + y <<< 0

case succ
w : Nat
x y : BitVec w
n✝ : Nat
a✝ : (x + y) <<< n✝ = x <<< n✝ + y <<< n✝
⊢ (x + y) <<< (n✝ + 1) = x <<< (n✝ + 1) + y <<< (n✝ + 1)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem LiftRel.swap (h : LiftRel r s x y) : LiftRel s r x.swap y.swap

Proof state:
case inl
α✝¹ : Type u_1
α✝ : Type u_2
r : α✝¹ → α✝ → Prop
β✝¹ : Type u_3
β✝ : Type u_4
s : β✝¹ → β✝ → Prop
a✝¹ : α✝¹
c✝ : α✝
a✝ : r a✝¹ c✝
⊢ LiftRel s r (inl a✝¹).swap (inl c✝).swap

Tactic:
exact LiftRel.inr ‹_›

Result:
no goals

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
r : α✝¹ → α✝ → Prop
β✝¹ : Type u_3
β✝ : Type u_4
s : β✝¹ → β✝ → Prop
x : α✝¹ ⊕ β✝¹
y : α✝ ⊕ β✝
h : LiftRel r s x y
⊢ LiftRel s r x.swap y.swap

Tactic:
cases h

Result:
case inl
α✝¹ : Type u_1
α✝ : Type u_2
r : α✝¹ → α✝ → Prop
β✝¹ : Type u_3
β✝ : Type u_4
s : β✝¹ → β✝ → Prop
a✝¹ : α✝¹
c✝ : α✝
a✝ : r a✝¹ c✝
⊢ LiftRel s r (inl a✝¹).swap (inl c✝).swap

case inr
α✝¹ : Type u_1
α✝ : Type u_2
r : α✝¹ → α✝ → Prop
β✝¹ : Type u_3
β✝ : Type u_4
s : β✝¹ → β✝ → Prop
b✝ : β✝¹
d✝ : β✝
a✝ : s b✝ d✝
⊢ LiftRel s r (inr b✝).swap (inr d✝).swap

Proof state:
case inr
α✝¹ : Type u_1
α✝ : Type u_2
r : α✝¹ → α✝ → Prop
β✝¹ : Type u_3
β✝ : Type u_4
s : β✝¹ → β✝ → Prop
b✝ : β✝¹
d✝ : β✝
a✝ : s b✝ d✝
⊢ LiftRel s r (inr b✝).swap (inr d✝).swap

Tactic:
exact LiftRel.inl ‹_›

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem sum_tmul {α : Type*} (s : Finset α) (m : α → M) (n : N) :
    (∑ a ∈ s, m a) ⊗ₜ[R] n = ∑ a ∈ s, m a ⊗ₜ[R] n

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
α : Type u_11
s : Finset α
m : α → M
n : N
⊢ (∑ a ∈ s, m a) ⊗ₜ[R] n = ∑ a ∈ s, m a ⊗ₜ[R] n

Tactic:
induction s using Finset.induction with
| empty => simp
| insert has ih => simp [Finset.sum_insert has, add_tmul, ih]

Result:
no goals

Proof state:
case insert
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
α : Type u_11
m : α → M
n : N
a✝ : α
s✝ : Finset α
has : a✝ ∉ s✝
ih : (∑ a ∈ s✝, m a) ⊗ₜ[R] n = ∑ a ∈ s✝, m a ⊗ₜ[R] n
⊢ (∑ a ∈ insert a✝ s✝, m a) ⊗ₜ[R] n = ∑ a ∈ insert a✝ s✝, m a ⊗ₜ[R] n

Tactic:
simp [Finset.sum_insert has, add_tmul, ih]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
α : Type u_11
s : Finset α
m : α → M
n : N
⊢ (∑ a ∈ s, m a) ⊗ₜ[R] n = ∑ a ∈ s, m a ⊗ₜ[R] n

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp
  | insert has ih => simp [Finset.sum_insert has, add_tmul, ih]

Result:
no goals

Proof state:
case empty
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
α : Type u_11
m : α → M
n : N
⊢ (∑ a ∈ ∅, m a) ⊗ₜ[R] n = ∑ a ∈ ∅, m a ⊗ₜ[R] n

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Archimedean.lean
theorem Filter.Eventually.ratCast_atBot [LinearOrderedField R] [Archimedean R] {p : R → Prop}
    (h : ∀ᶠ (x : R) in atBot, p x) : ∀ᶠ (n : ℚ) in atBot, p n

Proof state:
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atBot, p x
⊢ ∀ᶠ (n : ℚ) in atBot, p ↑n

Tactic:
rw [← Rat.comap_cast_atBot (R := R)]

Result:
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atBot, p x
⊢ ∀ᶠ (n : ℚ) in Filter.comap Rat.cast atBot, p ↑n

Proof state:
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atBot, p x
⊢ ∀ᶠ (n : ℚ) in Filter.comap Rat.cast atBot, p ↑n

Tactic:
exact h.comap _

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
@[simp]
lemma DifferentiableOn.add_iff_left (hg : DifferentiableOn 𝕜 g s) :
    DifferentiableOn 𝕜 (fun y => f y + g y) s ↔ DifferentiableOn 𝕜 f s

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
s : Set E
hg : DifferentiableOn 𝕜 g s
h : DifferentiableOn 𝕜 (fun y => f y + g y) s
⊢ DifferentiableOn 𝕜 f s

Tactic:
simpa only [add_sub_cancel_right] using h.sub hg

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
s : Set E
hg : DifferentiableOn 𝕜 g s
⊢ DifferentiableOn 𝕜 (fun y => f y + g y) s ↔ DifferentiableOn 𝕜 f s

Tactic:
refine ⟨fun h ↦ ?_, fun hf ↦ hf.add hg⟩

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
s : Set E
hg : DifferentiableOn 𝕜 g s
h : DifferentiableOn 𝕜 (fun y => f y + g y) s
⊢ DifferentiableOn 𝕜 f s
-- Mathlib/CategoryTheory/Filtered/Basic.lean
theorem of_cone_nonempty (h : ∀ {J : Type w} [SmallCategory J] [FinCategory J] (F : J ⥤ C),
    Nonempty (Cone F)) : IsCofiltered C

Proof state:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
this : Nonempty C
⊢ ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), ∃ W h, h ≫ f = h ≫ g

Tactic:
intros X Y f g

Result:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
⊢ ∃ W h, h ≫ f = h ≫ g

Proof state:
case refine_2.intro
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
⊢ ∃ W h, h ≫ f = h ≫ g

Tactic:
refine ⟨c.pt, c.π.app ⟨WalkingParallelPair.zero⟩, ?_⟩

Result:
case refine_2.intro
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
⊢ c.π.app { down := WalkingParallelPair.zero } ≫ f = c.π.app { down := WalkingParallelPair.zero } ≫ g

Proof state:
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
this✝ : Nonempty C
this : IsCofilteredOrEmpty C
⊢ IsCofiltered C

Tactic:
apply IsCofiltered.mk

Result:
no goals
-- Mathlib/Analysis/Normed/Group/SemiNormedGrp/Kernels.lean
theorem explicitCokernelIso_inv_π {X Y : SemiNormedGrp.{u}} (f : X ⟶ Y) :
    cokernel.π f ≫ (explicitCokernelIso f).inv = explicitCokernelπ f

Proof state:
X Y : SemiNormedGrp
f : X ⟶ Y
⊢ cokernel.π f ≫ (explicitCokernelIso f).inv = explicitCokernelπ f

Tactic:
simp [explicitCokernelπ, explicitCokernelIso]

Result:
no goals
-- Mathlib/Analysis/Calculus/DSlope.lean
theorem dslope_of_ne (f : 𝕜 → E) (h : b ≠ a) : dslope f a b = slope f a b

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : 𝕜
f : 𝕜 → E
h : b ≠ a
⊢ dslope f a b = slope f a b

Tactic:
exact update_of_ne h ..

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : 𝕜
f : 𝕜 → E
h : b ≠ a
⊢ dslope f a b = slope f a b

Tactic:
classical
exact update_of_ne h ..

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arccos_nhdsGE (h : Tendsto f l (𝓝[≥] x)) :
    Tendsto (arccos <| f ·) l (𝓝[≤] (arccos x))

Proof state:
α : Type u_1
l : Filter α
x : ℝ
f : α → ℝ
h : Tendsto f l (𝓝[≥] x)
⊢ Tendsto (fun x => arccos (f x)) l (𝓝[≤] arccos x)

Tactic:
refine ((continuous_arccos.tendsto _).inf <| MapsTo.tendsto fun y hy ↦ ?_).comp h

Result:
α : Type u_1
l : Filter α
x : ℝ
f : α → ℝ
h : Tendsto f l (𝓝[≥] x)
y : ℝ
hy : y ∈ Ici x
⊢ arccos y ∈ Iic (arccos x)

Proof state:
α : Type u_1
l : Filter α
x : ℝ
f : α → ℝ
h : Tendsto f l (𝓝[≥] x)
y : ℝ
hy : x ≤ y
⊢ arccos y ≤ arccos x

Tactic:
exact antitone_arccos hy

Result:
no goals

Proof state:
α : Type u_1
l : Filter α
x : ℝ
f : α → ℝ
h : Tendsto f l (𝓝[≥] x)
y : ℝ
hy : y ∈ Ici x
⊢ arccos y ∈ Iic (arccos x)

Tactic:
simp only [mem_Ici, mem_Iic] at hy ⊢

Result:
α : Type u_1
l : Filter α
x : ℝ
f : α → ℝ
h : Tendsto f l (𝓝[≥] x)
y : ℝ
hy : x ≤ y
⊢ arccos y ≤ arccos x