harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem getElem?_zipWith' {f : α → β → γ} {i : Nat} :
    (zipWith f l₁ l₂)[i]? = (l₁[i]?.map f).bind fun g => l₂[i]?.map g

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
l₂ : Array β
f : α → β → γ
i : Nat
toList✝ : List α
⊢ (zipWith f { toList := toList✝ } l₂)[i]? = (Option.map f { toList := toList✝ }[i]?).bind fun g => Option.map g l₂[i]?

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
i : Nat
toList✝¹ : List α
toList✝ : List β
⊢ (zipWith f { toList := toList✝¹ } { toList := toList✝ })[i]? =
    (Option.map f { toList := toList✝¹ }[i]?).bind fun g => Option.map g { toList := toList✝ }[i]?

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
i : Nat
toList✝¹ : List α
toList✝ : List β
⊢ (zipWith f { toList := toList✝¹ } { toList := toList✝ })[i]? =
    (Option.map f { toList := toList✝¹ }[i]?).bind fun g => Option.map g { toList := toList✝ }[i]?

Tactic:
simp [List.getElem?_zipWith']

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
l₁ : Array α
l₂ : Array β
f : α → β → γ
i : Nat
⊢ (zipWith f l₁ l₂)[i]? = (Option.map f l₁[i]?).bind fun g => Option.map g l₂[i]?

Tactic:
cases l₁

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
l₂ : Array β
f : α → β → γ
i : Nat
toList✝ : List α
⊢ (zipWith f { toList := toList✝ } l₂)[i]? = (Option.map f { toList := toList✝ }[i]?).bind fun g => Option.map g l₂[i]?
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
lemma _root_.AntitoneOn.mapsTo_uIcc (hf : AntitoneOn f (uIcc a b)) :
    MapsTo f (uIcc a b) (uIcc (f a) (f b))

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Lattice β
f : α → β
a b : α
hf : AntitoneOn f [[a, b]]
⊢ MapsTo f [[a, b]] [[f a, f b]]

Tactic:
rw [uIcc, uIcc, ← hf.map_sup, ← hf.map_inf] <;>
  apply_rules [left_mem_uIcc, right_mem_uIcc, hf.mapsTo_Icc]

Result:
no goals
-- Mathlib/Algebra/Order/AddGroupWithTop.lean
lemma strictMono_add_left_of_ne_top (b : α) (h : b ≠ ⊤) : StrictMono (fun x ↦ x + b)

Proof state:
case h₂
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
b : α
h : b ≠ ⊤
⊢ Function.Injective fun x => x + b

Tactic:
apply injective_add_left_of_ne_top _ h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
b : α
h : b ≠ ⊤
⊢ StrictMono fun x => x + b

Tactic:
apply Monotone.strictMono_of_injective

Result:
case h₁
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
b : α
h : b ≠ ⊤
⊢ Monotone fun x => x + b

case h₂
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
b : α
h : b ≠ ⊤
⊢ Function.Injective fun x => x + b

Proof state:
case h₁
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
b : α
h : b ≠ ⊤
⊢ Monotone fun x => x + b

Tactic:
apply Monotone.add_const monotone_id

Result:
no goals
-- Mathlib/Algebra/Ring/Associated.lean
lemma neg_left (h : Associated a b) : Associated (-a) b := let ⟨u, hu⟩ := h; ⟨-u, by simp [hu]⟩

Proof state:
M : Type u_1
inst✝¹ : Monoid M
inst✝ : HasDistribNeg M
a b : M
h : Associated a b
u : Mˣ
hu : a * ↑u = b
⊢ -a * ↑(-u) = b

Tactic:
simp [hu]

Result:
no goals
-- Mathlib/Topology/Algebra/UniformGroup/Defs.lean
theorem Filter.HasBasis.uniformity_of_nhds_one {ι} {p : ι → Prop} {U : ι → Set α}
    (h : (𝓝 (1 : α)).HasBasis p U) :
    (𝓤 α).HasBasis p fun i => { x : α × α | x.2 / x.1 ∈ U i }

Proof state:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : (𝓝 1).HasBasis p U
⊢ (Filter.comap (fun x => x.2 / x.1) (𝓝 1)).HasBasis p fun i => {x | x.2 / x.1 ∈ U i}

Tactic:
exact h.comap _

Result:
no goals

Proof state:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : (𝓝 1).HasBasis p U
⊢ (𝓤 α).HasBasis p fun i => {x | x.2 / x.1 ∈ U i}

Tactic:
rw [uniformity_eq_comap_nhds_one]

Result:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : (𝓝 1).HasBasis p U
⊢ (Filter.comap (fun x => x.2 / x.1) (𝓝 1)).HasBasis p fun i => {x | x.2 / x.1 ∈ U i}
-- Mathlib/RingTheory/PowerBasis.lean
theorem degree_minpolyGen [Nontrivial A] (pb : PowerBasis A S) :
    degree (minpolyGen pb) = pb.dim

Proof state:
S : Type u_2
inst✝³ : Ring S
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra A S
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ pb.minpolyGen.degree = ↑pb.dim

Tactic:
unfold minpolyGen

Result:
S : Type u_2
inst✝³ : Ring S
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra A S
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ (X ^ pb.dim - ∑ i : Fin pb.dim, C ((pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i).degree = ↑pb.dim

Proof state:
S : Type u_2
inst✝³ : Ring S
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra A S
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ (∑ i : Fin pb.dim, C ((pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i).degree < ↑pb.dim

Tactic:
apply degree_sum_fin_lt

Result:
no goals

Proof state:
S : Type u_2
inst✝³ : Ring S
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra A S
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ (X ^ pb.dim - ∑ i : Fin pb.dim, C ((pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i).degree = ↑pb.dim

Tactic:
rw [degree_sub_eq_left_of_degree_lt] <;> rw [degree_X_pow]

Result:
S : Type u_2
inst✝³ : Ring S
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra A S
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ (∑ i : Fin pb.dim, C ((pb.basis.repr (pb.gen ^ pb.dim)) i) * X ^ ↑i).degree < ↑pb.dim
-- Mathlib/Data/Ordmap/Ordset.lean
theorem size_balanceR {l x r} (hl : Balanced l) (hr : Balanced r) (sl : Sized l) (sr : Sized r)
    (H : (∃ l', Raised (size l) l' ∧ BalancedSz l' (size r)) ∨
        ∃ r', Raised r' (size r) ∧ BalancedSz (size l) r') :
    size (@balanceR α l x r) = size l + size r + 1

Proof state:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'
⊢ (l.balanceR x r).size = l.size + r.size + 1

Tactic:
rw [balanceR_eq_balance' hl hr sl sr H, size_balance' sl sr]

Result:
no goals
-- Mathlib/Data/Nat/Find.lean
@[simp] lemma lt_find_iff (h : ∃ n : ℕ, p n) (n : ℕ) : n < Nat.find h ↔ ∀ m ≤ n, ¬ p m

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
n : ℕ
⊢ n < Nat.find h ↔ ∀ (m : ℕ), m ≤ n → ¬p m

Tactic:
simp only [← succ_le_iff, le_find_iff, succ_le_succ_iff]

Result:
no goals
-- Mathlib/Data/List/Sym.lean
theorem sym2_map (f : α → β) (xs : List α) :
    (xs.map f).sym2 = xs.sym2.map (Sym2.map f)

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → β
⊢ (map f []).sym2 = map (Sym2.map f) [].sym2

Tactic:
simp [List.sym2]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
xs : List α
⊢ (map f xs).sym2 = map (Sym2.map f) xs.sym2

Tactic:
induction xs with
| nil => simp [List.sym2]
| cons x xs ih => simp [List.sym2, ih, Function.comp]

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → β
x : α
xs : List α
ih : (map f xs).sym2 = map (Sym2.map f) xs.sym2
⊢ (map f (x :: xs)).sym2 = map (Sym2.map f) (x :: xs).sym2

Tactic:
simp [List.sym2, ih, Function.comp]

Result:
no goals
-- Mathlib/Data/List/Sublists.lean
theorem sublistsLen_sublist_sublists' :
    ∀ (n) (l : List α), sublistsLen n l <+ sublists' l
  | 0, l => by simp
  | _ + 1, [] => nil_sublist _
  | n + 1, a :: l => by
    rw [sublistsLen_succ_cons, sublists'_cons]
    exact (sublistsLen_sublist_sublists' _ _).append ((sublistsLen_sublist_sublists' _ _).map _)

Proof state:
α : Type u
n : ℕ
a : α
l : List α
⊢ sublistsLen (n + 1) (a :: l) <+ (a :: l).sublists'

Tactic:
rw [sublistsLen_succ_cons, sublists'_cons]

Result:
α : Type u
n : ℕ
a : α
l : List α
⊢ sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l) <+ l.sublists' ++ map (cons a) l.sublists'

Proof state:
α : Type u
n : ℕ
a : α
l : List α
⊢ sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l) <+ l.sublists' ++ map (cons a) l.sublists'

Tactic:
exact (sublistsLen_sublist_sublists' _ _).append ((sublistsLen_sublist_sublists' _ _).map _)

Result:
no goals

Proof state:
α : Type u
l : List α
⊢ sublistsLen 0 l <+ l.sublists'

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem mul_ne_zero {a b : Ordinal} : a ≠ 0 → b ≠ 0 → a * b ≠ 0

Proof state:
a b : Ordinal.{u_4}
⊢ a ≠ 0 → b ≠ 0 → a * b ≠ 0

Tactic:
simpa only [Ordinal.pos_iff_ne_zero] using mul_pos

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem succ_eq_last_succ {n : Nat} {i : Fin n.succ} :
    i.succ = last (n + 1) ↔ i = last n

Proof state:
n : Nat
i : Fin n.succ
⊢ i.succ = last (n + 1) ↔ i = last n

Tactic:
rw [← succ_last, succ_inj]

Result:
no goals
-- Mathlib/Logic/Equiv/Option.lean
theorem removeNone_aux_some {x : α} (h : ∃ x', e (some x) = some x') :
    some (removeNone_aux e x) = e (some x)

Proof state:
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h : ∃ x', e (some x) = some x'
⊢ some (e.removeNone_aux x) = e (some x)

Tactic:
simp [removeNone_aux, Option.isSome_iff_exists.mpr h]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem toOrderedSMul : OrderedSMul ℝ K :=
  OrderedSMul.mk' fun a b r hab hr => by
    replace hab := hab.le
    rw [RCLike.le_iff_re_im] at hab
    rw [RCLike.le_iff_re_im, smul_re, smul_re, smul_im, smul_im]
    exact hab.imp (fun h => mul_le_mul_of_nonneg_left h hr.le) (congr_arg _)

Proof state:
K : Type u_1
inst✝ : RCLike K
a b : K
r : ℝ
hr : 0 < r
hab : a ≤ b
⊢ r • a ≤ r • b

Tactic:
rw [RCLike.le_iff_re_im] at hab

Result:
K : Type u_1
inst✝ : RCLike K
a b : K
r : ℝ
hr : 0 < r
hab : re a ≤ re b ∧ im a = im b
⊢ r • a ≤ r • b

Proof state:
K : Type u_1
inst✝ : RCLike K
a b : K
r : ℝ
hr : 0 < r
hab : re a ≤ re b ∧ im a = im b
⊢ r • a ≤ r • b

Tactic:
rw [RCLike.le_iff_re_im, smul_re, smul_re, smul_im, smul_im]

Result:
K : Type u_1
inst✝ : RCLike K
a b : K
r : ℝ
hr : 0 < r
hab : re a ≤ re b ∧ im a = im b
⊢ r * re a ≤ r * re b ∧ r * im a = r * im b

Proof state:
K : Type u_1
inst✝ : RCLike K
a b : K
r : ℝ
hab : a < b
hr : 0 < r
⊢ r • a ≤ r • b

Tactic:
replace hab := hab.le

Result:
K : Type u_1
inst✝ : RCLike K
a b : K
r : ℝ
hr : 0 < r
hab : a ≤ b
⊢ r • a ≤ r • b

Proof state:
K : Type u_1
inst✝ : RCLike K
a b : K
r : ℝ
hr : 0 < r
hab : re a ≤ re b ∧ im a = im b
⊢ r * re a ≤ r * re b ∧ r * im a = r * im b

Tactic:
exact hab.imp (fun h => mul_le_mul_of_nonneg_left h hr.le) (congr_arg _)

Result:
no goals
-- Mathlib/Data/Rat/Lemmas.lean
theorem inv_natCast_den_of_pos {a : ℕ} (ha0 : 0 < a) : (a : ℚ)⁻¹.den = a

Proof state:
a : ℕ
ha0 : 0 < a
⊢ 0 < ↑a

Tactic:
rwa [Int.natCast_pos]

Result:
no goals

Proof state:
a : ℕ
ha0 : 0 < a
⊢ (↑a)⁻¹.den = a

Tactic:
rw [← Int.ofNat_inj, ← Int.cast_natCast a, inv_intCast_den_of_pos]

Result:
a : ℕ
ha0 : 0 < a
⊢ 0 < ↑a
-- Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
theorem decomp' (f : V1 →ᵃ[k] V2) : (f.linear : V1 → V2) = ⇑f - fun _ => f 0

Proof state:
k : Type u_1
V1 : Type u_2
V2 : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V1
inst✝² : Module k V1
inst✝¹ : AddCommGroup V2
inst✝ : Module k V2
f : V1 →ᵃ[k] V2
⊢ ⇑f.linear = (⇑f.linear + fun x => f 0) - fun x => (⇑f.linear + fun x => f 0) 0

Tactic:
simp only [LinearMap.map_zero, Pi.add_apply, add_sub_cancel_right, zero_add]

Result:
no goals

Proof state:
k : Type u_1
V1 : Type u_2
V2 : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V1
inst✝² : Module k V1
inst✝¹ : AddCommGroup V2
inst✝ : Module k V2
f : V1 →ᵃ[k] V2
⊢ ⇑f.linear = ⇑f - fun x => f 0

Tactic:
rw [decomp]

Result:
k : Type u_1
V1 : Type u_2
V2 : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V1
inst✝² : Module k V1
inst✝¹ : AddCommGroup V2
inst✝ : Module k V2
f : V1 →ᵃ[k] V2
⊢ ⇑f.linear = (⇑f.linear + fun x => f 0) - fun x => (⇑f.linear + fun x => f 0) 0
-- Mathlib/GroupTheory/HNNExtension.lean
theorem toSubgroupEquiv_neg_apply (u : ℤˣ) (a : toSubgroup A B u) :
    (toSubgroupEquiv φ (-u) (toSubgroupEquiv φ u a) : G) = a

Proof state:
case inr
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥(toSubgroup A B (-1))
⊢ ↑((toSubgroupEquiv φ (- -1)) ((toSubgroupEquiv φ (-1)) a)) = ↑a

Tactic:
simp only [toSubgroup_neg_one, toSubgroupEquiv_neg_one, SetLike.coe_eq_coe]

Result:
case inr
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥(toSubgroup A B (-1))
⊢ (toSubgroupEquiv φ (- -1)) (φ.symm a) = a

Proof state:
case inl
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥(toSubgroup A B 1)
⊢ φ.symm (φ a) = a

Tactic:
erw [MulEquiv.symm_apply_apply]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
u : ℤˣ
a : ↥(toSubgroup A B u)
⊢ ↑((toSubgroupEquiv φ (-u)) ((toSubgroupEquiv φ u) a)) = ↑a

Tactic:
rcases Int.units_eq_one_or u with rfl | rfl

Result:
case inl
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥(toSubgroup A B 1)
⊢ ↑((toSubgroupEquiv φ (-1)) ((toSubgroupEquiv φ 1) a)) = ↑a

case inr
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥(toSubgroup A B (-1))
⊢ ↑((toSubgroupEquiv φ (- -1)) ((toSubgroupEquiv φ (-1)) a)) = ↑a

Proof state:
case inl
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥(toSubgroup A B 1)
⊢ ↑((toSubgroupEquiv φ (-1)) ((toSubgroupEquiv φ 1) a)) = ↑a

Tactic:
simp

Result:
case inl
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥(toSubgroup A B 1)
⊢ φ.symm (φ a) = a

Proof state:
case inr
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥(toSubgroup A B (-1))
⊢ (toSubgroupEquiv φ (- -1)) (φ.symm a) = a

Tactic:
exact φ.apply_symm_apply a

Result:
no goals
-- Mathlib/Data/Matrix/RowCol.lean
theorem map_updateRow [DecidableEq m] (f : α → β) :
    map (updateRow M i b) f = updateRow (M.map f) i (f ∘ b)

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
i : m
b : n → α
inst✝ : DecidableEq m
f : α → β
i✝ : m
j✝ : n
⊢ f (if i✝ = i then b j✝ else M i✝ j✝) = if i✝ = i then (f ∘ b) j✝ else f (M i✝ j✝)

Tactic:
exact apply_ite f _ _ _

Result:
no goals

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
i : m
b : n → α
inst✝ : DecidableEq m
f : α → β
i✝ : m
j✝ : n
⊢ (M.updateRow i b).map f i✝ j✝ = (M.map f).updateRow i (f ∘ b) i✝ j✝

Tactic:
rw [updateRow_apply, map_apply, map_apply, updateRow_apply]

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
i : m
b : n → α
inst✝ : DecidableEq m
f : α → β
i✝ : m
j✝ : n
⊢ f (if i✝ = i then b j✝ else M i✝ j✝) = if i✝ = i then (f ∘ b) j✝ else f (M i✝ j✝)

Proof state:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
i : m
b : n → α
inst✝ : DecidableEq m
f : α → β
⊢ (M.updateRow i b).map f = (M.map f).updateRow i (f ∘ b)

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
i : m
b : n → α
inst✝ : DecidableEq m
f : α → β
i✝ : m
j✝ : n
⊢ (M.updateRow i b).map f i✝ j✝ = (M.map f).updateRow i (f ∘ b) i✝ j✝
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_cons_eq_true [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
    (containsKey a (⟨k, v⟩ :: l)) ↔ (k == a) ∨ (containsKey a l)

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k a : α
v : β k
⊢ containsKey a (⟨k, v⟩ :: l) = true ↔ (k == a) = true ∨ containsKey a l = true

Tactic:
simp [containsKey_cons]

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

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
hg : Differentiable 𝕜 g
⊢ (Differentiable 𝕜 fun y => f y - g y) ↔ Differentiable 𝕜 f

Tactic:
simp only [sub_eq_add_neg, differentiable_neg_iff, hg, add_iff_left]

Result:
no goals
-- Mathlib/Data/Matrix/Notation.lean
theorem vec3_eq {a₀ a₁ a₂ b₀ b₁ b₂ : α} (h₀ : a₀ = b₀) (h₁ : a₁ = b₁) (h₂ : a₂ = b₂) :
    ![a₀, a₁, a₂] = ![b₀, b₁, b₂]

Proof state:
α : Type u
b₀ b₁ b₂ : α
⊢ ![b₀, b₁, b₂] = ![b₀, b₁, b₂]

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
a₀ a₁ a₂ b₀ b₁ b₂ : α
h₀ : a₀ = b₀
h₁ : a₁ = b₁
h₂ : a₂ = b₂
⊢ ![a₀, a₁, a₂] = ![b₀, b₁, b₂]

Tactic:
subst_vars

Result:
α : Type u
b₀ b₁ b₂ : α
⊢ ![b₀, b₁, b₂] = ![b₀, b₁, b₂]
-- Mathlib/Data/Nat/Nth.lean
lemma nth_add_eq_sub {m n : ℕ} (h0 : ∀ k < m, ¬p k) (h : nth p n ≠ 0) :
    nth (fun i ↦ p (i + m)) n = nth p n - m

Proof state:
p : ℕ → Prop
m n : ℕ
h0 : ∀ k < m, ¬p k
h : nth p n ≠ 0
⊢ nth (fun i => p (i + m)) n = nth p n - m

Tactic:
rw [← nth_add h0 h, Nat.add_sub_cancel]

Result:
no goals
-- Mathlib/Data/Multiset/UnionInter.lean
lemma cons_inter_distrib (a : α) (s t : Multiset α) : a ::ₘ s ∩ t = (a ::ₘ s) ∩ (a ::ₘ t)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ a ::ₘ s ∩ t = (a ::ₘ s) ∩ (a ::ₘ t)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Rat/Cast/Defs.lean
@[norm_cast] lemma cast_mul_of_ne_zero (hp : (p.den : α) ≠ 0) (hq : (q.den : α) ≠ 0) :
    ↑(p * q) = (p * q : α)

Proof state:
case hb
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑(p.den * q.den) ≠ 0

Tactic:
push_cast

Result:
case hb
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑p.den * ↑q.den ≠ 0

Proof state:
case hb
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑p.den * ↑q.den ≠ 0

Tactic:
exact mul_ne_zero hp hq

Result:
no goals

Proof state:
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑p.num * ↑q.num / (↑p.den * ↑q.den) = ↑p.num * ↑q.num / (↑p.den * ↑q.den)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑(p * q) = ↑p * ↑q

Tactic:
rw [mul_eq_mkRat, cast_mkRat_of_ne_zero, cast_def, cast_def,
  (Nat.commute_cast _ _).div_mul_div_comm (Int.commute_cast _ _)]

Result:
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑(p.num * q.num) / ↑(p.den * q.den) = ↑p.num * ↑q.num / (↑p.den * ↑q.den)

case hb
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑(p.den * q.den) ≠ 0

Proof state:
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑(p.num * q.num) / ↑(p.den * q.den) = ↑p.num * ↑q.num / (↑p.den * ↑q.den)

Tactic:
push_cast

Result:
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑p.num * ↑q.num / (↑p.den * ↑q.den) = ↑p.num * ↑q.num / (↑p.den * ↑q.den)
-- Mathlib/Geometry/Manifold/BumpFunction.lean
theorem isOpen_support : IsOpen (support f)

Proof state:
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
⊢ IsOpen ((chartAt H c).source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) f.rOut)

Tactic:
exact isOpen_extChartAt_preimage c isOpen_ball

Result:
no goals

Proof state:
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
⊢ IsOpen (support ↑f)

Tactic:
rw [support_eq_inter_preimage]

Result:
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
⊢ IsOpen ((chartAt H c).source ∩ ↑(extChartAt I c) ⁻¹' ball (↑(extChartAt I c) c) f.rOut)
-- Mathlib/Data/Nat/Prime/Basic.lean
theorem Prime.mod_two_eq_one_iff_ne_two {p : ℕ} [Fact p.Prime] : p % 2 = 1 ↔ p ≠ 2

Proof state:
p : ℕ
inst✝ : Fact (Prime p)
⊢ p % 2 = 1 ↔ p ≠ 2

Tactic:
refine ⟨fun h hf => ?_, (Nat.Prime.eq_two_or_odd <| @Fact.out p.Prime _).resolve_left⟩

Result:
p : ℕ
inst✝ : Fact (Prime p)
h : p % 2 = 1
hf : p = 2
⊢ False

Proof state:
p : ℕ
inst✝ : Fact (Prime p)
h : 2 % 2 = 1
hf : p = 2
⊢ False

Tactic:
simp at h

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Prime p)
h : p % 2 = 1
hf : p = 2
⊢ False

Tactic:
rw [hf] at h

Result:
p : ℕ
inst✝ : Fact (Prime p)
h : 2 % 2 = 1
hf : p = 2
⊢ False
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem continuous_proj :
    Continuous (Proj J : (I → Bool) → (I → Bool))

Proof state:
case h
I : Type u
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
⊢ ∀ (i : I), Continuous fun a => if J i then a i else false

Tactic:
intro i

Result:
case h
I : Type u
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
i : I
⊢ Continuous fun a => if J i then a i else false

Proof state:
I : Type u
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
⊢ Continuous fun c i => if J i then c i else false

Tactic:
apply continuous_pi

Result:
case h
I : Type u
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
⊢ ∀ (i : I), Continuous fun a => if J i then a i else false

Proof state:
I : Type u
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
⊢ Continuous (Proj J)

Tactic:
dsimp (config := { unfoldPartialApp := true }) [Proj]

Result:
I : Type u
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
⊢ Continuous fun c i => if J i then c i else false

Proof state:
case h
I : Type u
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
i : I
⊢ Continuous fun a => if J i then a i else false

Tactic:
split

Result:
case h.isTrue
I : Type u
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
i : I
h✝ : J i
⊢ Continuous fun a => a i

case h.isFalse
I : Type u
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
i : I
h✝ : ¬J i
⊢ Continuous fun a => false

Proof state:
case h.isFalse
I : Type u
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
i : I
h✝ : ¬J i
⊢ Continuous fun a => false

Tactic:
apply continuous_const

Result:
no goals

Proof state:
case h.isTrue
I : Type u
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
i : I
h✝ : J i
⊢ Continuous fun a => a i

Tactic:
apply continuous_apply

Result:
no goals
-- Mathlib/NumberTheory/Dioph.lean
theorem abs_poly_dioph (p : Poly α) : DiophFn fun v => (p v).natAbs :=
  of_no_dummies _ ((p.map some - Poly.proj none) * (p.map some + Poly.proj none))
    fun v => (by dsimp; exact Int.eq_natAbs_iff_mul_eq_zero)

Proof state:
α : Type u
p : Poly α
v : Option α → ℕ
⊢ {v | (p (v ∘ some)).natAbs = v none} v ↔ (p (v ∘ some) - ↑(v none)) * (p (v ∘ some) + ↑(v none)) = 0

Tactic:
exact Int.eq_natAbs_iff_mul_eq_zero

Result:
no goals

Proof state:
α : Type u
p : Poly α
v : Option α → ℕ
⊢ {v | (fun v => (p v).natAbs) (v ∘ some) = v none} v ↔
    ((Poly.map some p - Poly.proj none) * (Poly.map some p + Poly.proj none)) v = 0

Tactic:
dsimp

Result:
α : Type u
p : Poly α
v : Option α → ℕ
⊢ {v | (p (v ∘ some)).natAbs = v none} v ↔ (p (v ∘ some) - ↑(v none)) * (p (v ∘ some) + ↑(v none)) = 0
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isDetector_def (G : C) :
    IsDetector G ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ h : G ⟶ Y, ∃! h', h' ≫ f = h) → IsIso f :=
  ⟨fun hG X Y f hf =>
    hG _ fun H hH h => by
      obtain rfl := Set.mem_singleton_iff.1 hH
      exact hf h,
    fun hG _ _ _ hf => hG _ fun _ => hf _ (Set.mem_singleton _) _⟩

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
H : C
h : H ⟶ Y
hG : IsDetector H
hf : ∀ (h : H ⟶ Y), ∃! h', h' ≫ f = h
hH : H ∈ {H}
⊢ ∃! h', h' ≫ f = h

Tactic:
exact hf h

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
hG : IsDetector G
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
H : C
hH : H ∈ {G}
h : H ⟶ Y
⊢ ∃! h', h' ≫ f = h

Tactic:
obtain rfl := Set.mem_singleton_iff.1 hH

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
H : C
h : H ⟶ Y
hG : IsDetector H
hf : ∀ (h : H ⟶ Y), ∃! h', h' ≫ f = h
hH : H ∈ {H}
⊢ ∃! h', h' ≫ f = h