harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/ModelTheory/Encoding.lean
theorem card_sigma : #(Σn, L.Term (α ⊕ (Fin n))) = max ℵ₀ #(α ⊕ (Σi, L.Functions i))

Proof state:
case refine_1
L : Language
α : Type u'
⊢ ℵ₀ ≤ ℵ₀ ⊔ #(α ⊕ (i : ℕ) × L.Functions i) ∧ ∀ (i : ℕ), #(L.Term (α ⊕ Fin i)) ≤ ℵ₀ ⊔ #(α ⊕ (i : ℕ) × L.Functions i)

Tactic:
refine ⟨le_max_left _ _, fun i => card_le.trans ?_⟩

Result:
case refine_1
L : Language
α : Type u'
i : ℕ
⊢ ℵ₀ ⊔ #((α ⊕ Fin i) ⊕ (i : ℕ) × L.Functions i) ≤ ℵ₀ ⊔ #(α ⊕ (i : ℕ) × L.Functions i)

Proof state:
case refine_1
L : Language
α : Type u'
i : ℕ
⊢ ℵ₀ ⊔ #((α ⊕ Fin i) ⊕ (i : ℕ) × L.Functions i) ≤ ℵ₀ ⊔ #(α ⊕ (i : ℕ) × L.Functions i)

Tactic:
refine max_le (le_max_left _ _) ?_

Result:
case refine_1
L : Language
α : Type u'
i : ℕ
⊢ #((α ⊕ Fin i) ⊕ (i : ℕ) × L.Functions i) ≤ ℵ₀ ⊔ #(α ⊕ (i : ℕ) × L.Functions i)

Proof state:
case refine_1
L : Language
α : Type u'
i : ℕ
⊢ ↑i + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))

Tactic:
exact add_le_add_right (nat_lt_aleph0 _).le _

Result:
no goals

Proof state:
case refine_2.refine_2
L : Language
α : Type u'
⊢ #(α ⊕ (i : ℕ) × L.Functions i) ≤ #((n : ℕ) × L.Term (α ⊕ Fin n))

Tactic:
rw [Cardinal.le_def]

Result:
case refine_2.refine_2
L : Language
α : Type u'
⊢ Nonempty (α ⊕ (i : ℕ) × L.Functions i ↪ (n : ℕ) × L.Term (α ⊕ Fin n))

Proof state:
case refine_1
L : Language
α : Type u'
⊢ ⨆ i, #(L.Term (α ⊕ Fin i)) ≠ 0

Tactic:
rw [← one_le_iff_ne_zero]

Result:
case refine_1
L : Language
α : Type u'
⊢ 1 ≤ ⨆ i, #(L.Term (α ⊕ Fin i))

Proof state:
case refine_1
L : Language
α : Type u'
⊢ 1 ≤ #(L.Term (α ⊕ Fin 1))

Tactic:
rw [one_le_iff_ne_zero, mk_ne_zero_iff]

Result:
case refine_1
L : Language
α : Type u'
⊢ Nonempty (L.Term (α ⊕ Fin 1))

Proof state:
case refine_1
L : Language
α : Type u'
i : ℕ
⊢ #((α ⊕ Fin i) ⊕ (i : ℕ) × L.Functions i) ≤ ℵ₀ ⊔ #(α ⊕ (i : ℕ) × L.Functions i)

Tactic:
rw [← add_eq_max le_rfl, mk_sum, mk_sum, mk_sum, add_comm (Cardinal.lift #α), lift_add,
  add_assoc, lift_lift, lift_lift, mk_fin, lift_natCast]

Result:
case refine_1
L : Language
α : Type u'
i : ℕ
⊢ ↑i + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
-- Mathlib/CategoryTheory/Shift/Basic.lean
@[reassoc]
lemma shiftFunctorAdd_assoc_hom_app (a₁ a₂ a₃ : A) (X : C) :
    (shiftFunctorAdd C (a₁ + a₂) a₃).hom.app X ≫
      ((shiftFunctorAdd C a₁ a₂).hom.app X)⟦a₃⟧' =
    (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) (add_assoc _ _ _).symm).hom.app X ≫
      (shiftFunctorAdd C a₂ a₃).hom.app (X⟦a₁⟧)

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
X : C
⊢ (shiftFunctorAdd C (a₁ + a₂) a₃).hom.app X ≫ (shiftFunctor C a₃).map ((shiftFunctorAdd C a₁ a₂).hom.app X) =
    (shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯).hom.app X ≫
      (shiftFunctorAdd C a₂ a₃).hom.app ((shiftFunctor C a₁).obj X)

Tactic:
simpa using NatTrans.congr_app (congr_arg Iso.hom (shiftFunctorAdd_assoc C a₁ a₂ a₃)) X

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/GetElem.lean
theorem get!_eq_getElem! [Inhabited α] (a : Array α) (i : Nat) : a.get! i = a[i]!

Proof state:
α : Type u_1
inst✝ : Inhabited α
a : Array α
i : Nat
⊢ (if h : i < a.size then getElem a i ⋯ else default) =
    match getElem? a i with
    | some e => e
    | none => default

Tactic:
split <;> simp_all [getElem?_pos, getElem?_neg]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Inhabited α
a : Array α
i : Nat
⊢ a.get! i = getElem! a i

Tactic:
simp only [get!, getD, get_eq_getElem, getElem!_def]

Result:
α : Type u_1
inst✝ : Inhabited α
a : Array α
i : Nat
⊢ (if h : i < a.size then getElem a i ⋯ else default) =
    match getElem? a i with
    | some e => e
    | none => default
-- Mathlib/Data/Finset/PImage.lean
theorem pimage_congr (h₁ : s = t) (h₂ : ∀ x ∈ t, f x = g x) : s.pimage f = t.pimage g

Proof state:
α : Type u_1
β : Type u_2
inst✝² : DecidableEq β
f g : α →. β
inst✝¹ : (x : α) → Decidable (f x).Dom
inst✝ : (x : α) → Decidable (g x).Dom
s t : Finset α
h₁ : s = t
h₂ : ∀ x ∈ t, f x = g x
⊢ pimage f s = pimage g t

Tactic:
subst s

Result:
α : Type u_1
β : Type u_2
inst✝² : DecidableEq β
f g : α →. β
inst✝¹ : (x : α) → Decidable (f x).Dom
inst✝ : (x : α) → Decidable (g x).Dom
t : Finset α
h₂ : ∀ x ∈ t, f x = g x
⊢ pimage f t = pimage g t

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝² : DecidableEq β
f g : α →. β
inst✝¹ : (x : α) → Decidable (f x).Dom
inst✝ : (x : α) → Decidable (g x).Dom
t : Finset α
h₂ : ∀ x ∈ t, f x = g x
y : β
⊢ y ∈ pimage f t ↔ y ∈ pimage g t

Tactic:
simp +contextual only [mem_pimage, ← exists_prop, h₂]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : DecidableEq β
f g : α →. β
inst✝¹ : (x : α) → Decidable (f x).Dom
inst✝ : (x : α) → Decidable (g x).Dom
t : Finset α
h₂ : ∀ x ∈ t, f x = g x
⊢ pimage f t = pimage g t

Tactic:
ext y

Result:
case h
α : Type u_1
β : Type u_2
inst✝² : DecidableEq β
f g : α →. β
inst✝¹ : (x : α) → Decidable (f x).Dom
inst✝ : (x : α) → Decidable (g x).Dom
t : Finset α
h₂ : ∀ x ∈ t, f x = g x
y : β
⊢ y ∈ pimage f t ↔ y ∈ pimage g t
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedGatesLemmas.lean
theorem denote_mkImpCached {aig : AIG α} {input : BinaryInput aig} :
    ⟦aig.mkImpCached input, assign⟧
      =
    (
      !⟦aig, ⟨input.lhs.gate, input.lhs.hgate⟩, assign⟧
        ||
      ⟦aig, ⟨input.rhs.gate, input.rhs.hgate⟩, assign⟧
    )

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.BinaryInput
⊢ ⟦assign, aig.mkImpCached input⟧ =
    !(⟦assign, { aig := aig, ref := { gate := input.lhs.gate, hgate := ⋯ } }⟧ &&
        !⟦assign, { aig := aig, ref := { gate := input.rhs.gate, hgate := ⋯ } }⟧)

Tactic:
simp [mkImpCached, LawfulOperator.denote_input_entry (f := mkConstCached)]

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.BinaryInput
⊢ ⟦assign, aig.mkImpCached input⟧ =
    (!⟦assign, { aig := aig, ref := { gate := input.lhs.gate, hgate := ⋯ } }⟧ ||
      ⟦assign, { aig := aig, ref := { gate := input.rhs.gate, hgate := ⋯ } }⟧)

Tactic:
rw [← imp_as_aig]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.BinaryInput
⊢ ⟦assign, aig.mkImpCached input⟧ =
    !(⟦assign, { aig := aig, ref := { gate := input.lhs.gate, hgate := ⋯ } }⟧ &&
        !⟦assign, { aig := aig, ref := { gate := input.rhs.gate, hgate := ⋯ } }⟧)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem getKey?_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} :
    m.getKey? a = Raw₀.getKey? ⟨m, h.size_buckets_pos⟩ a

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α β
h : m.WF
a : α
⊢ m.getKey? a = Raw₀.getKey? ⟨m, ⋯⟩ a

Tactic:
simp [Raw.getKey?, h.size_buckets_pos]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma pow_self_mul_pow_self_le : m ^ m * n ^ n ≤ (m + n) ^ (m + n)

Proof state:
m n : ℕ
⊢ m ^ m * n ^ n ≤ (m + n) ^ m * (m + n) ^ n

Tactic:
exact Nat.mul_le_mul (Nat.pow_le_pow_left (le_add_right ..) _)
  (Nat.pow_le_pow_left (le_add_left ..) _)

Result:
no goals

Proof state:
m n : ℕ
⊢ m ^ m * n ^ n ≤ (m + n) ^ (m + n)

Tactic:
rw [Nat.pow_add]

Result:
m n : ℕ
⊢ m ^ m * n ^ n ≤ (m + n) ^ m * (m + n) ^ n
-- Mathlib/Topology/Maps/Basic.lean
theorem isQuotientMap_iff_isClosed :
    IsQuotientMap f ↔ Surjective f ∧ ∀ s : Set Y, IsClosed s ↔ IsClosed (f ⁻¹' s) :=
  isQuotientMap_iff.trans <| Iff.rfl.and <| compl_surjective.forall.trans <| by
    simp only [isOpen_compl_iff, preimage_compl]

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ (∀ (x : Set Y), IsOpen xᶜ ↔ IsOpen (f ⁻¹' xᶜ)) ↔ ∀ (s : Set Y), IsClosed s ↔ IsClosed (f ⁻¹' s)

Tactic:
simp only [isOpen_compl_iff, preimage_compl]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem minDegree_le_degree [DecidableRel G.Adj] (v : V) : G.minDegree ≤ G.degree v

Proof state:
case intro
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
t : ℕ
ht : (image (fun v => G.degree v) univ).min = ↑t
this : t ≤ G.degree v
⊢ G.minDegree ≤ G.degree v

Tactic:
rwa [minDegree, ht]

Result:
no goals

Proof state:
case intro
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
t : ℕ
ht : (image (fun v => G.degree v) univ).min = ↑t
⊢ G.minDegree ≤ G.degree v

Tactic:
have := Finset.min_le_of_eq (mem_image_of_mem _ (mem_univ v)) ht

Result:
case intro
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
t : ℕ
ht : (image (fun v => G.degree v) univ).min = ↑t
this : t ≤ G.degree v
⊢ G.minDegree ≤ G.degree v

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
⊢ G.minDegree ≤ G.degree v

Tactic:
obtain ⟨t, ht⟩ := Finset.min_of_mem (mem_image_of_mem (fun v => G.degree v) (mem_univ v))

Result:
case intro
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
t : ℕ
ht : (image (fun v => G.degree v) univ).min = ↑t
⊢ G.minDegree ≤ G.degree v
-- Mathlib/Topology/Order.lean
theorem continuous_sInf_rng {t₁ : TopologicalSpace α} {T : Set (TopologicalSpace β)} :
    Continuous[t₁, sInf T] f ↔ ∀ t ∈ T, Continuous[t₁, t] f

Proof state:
α : Type u
β : Type v
f : α → β
t₁ : TopologicalSpace α
T : Set (TopologicalSpace β)
⊢ Continuous f ↔ ∀ t ∈ T, Continuous f

Tactic:
simp only [continuous_iff_coinduced_le, le_sInf_iff]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma mul_inv (a b : EReal) : (a * b)⁻¹ = a⁻¹ * b⁻¹

Proof state:
case top_pos
x : ℝ
x_pos : 0 < x
⊢ (⊤ * ↑x)⁻¹ = ⊤⁻¹ * (↑x)⁻¹

Tactic:
rw [top_mul_of_pos (EReal.coe_pos.2 x_pos), inv_top, zero_mul]

Result:
no goals

Proof state:
case symm
a b : EReal
h : (a * b)⁻¹ = a⁻¹ * b⁻¹
⊢ (b * a)⁻¹ = b⁻¹ * a⁻¹

Tactic:
rw [mul_comm b a, mul_comm b⁻¹ a⁻¹]

Result:
case symm
a b : EReal
h : (a * b)⁻¹ = a⁻¹ * b⁻¹
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹

Proof state:
case top_neg
x : ℝ
x_neg : x < 0
⊢ (⊤ * ↑x)⁻¹ = ⊤⁻¹ * (↑x)⁻¹

Tactic:
rw [top_mul_of_neg (EReal.coe_neg'.2 x_neg), inv_bot, inv_top, zero_mul]

Result:
no goals

Proof state:
case coe_coe
x y : ℝ
⊢ (↑x * ↑y)⁻¹ = (↑x)⁻¹ * (↑y)⁻¹

Tactic:
rw [← coe_mul, ← coe_inv, _root_.mul_inv, coe_mul, coe_inv, coe_inv]

Result:
no goals

Proof state:
case pos_bot
x : ℝ
x_pos : 0 < x
⊢ (↑x * ⊥)⁻¹ = (↑x)⁻¹ * ⊥⁻¹

Tactic:
rw [mul_bot_of_pos (EReal.coe_pos.2 x_pos), inv_bot, mul_zero]

Result:
no goals

Proof state:
case neg_bot
x : ℝ
x_neg : x < 0
⊢ (↑x * ⊥)⁻¹ = (↑x)⁻¹ * ⊥⁻¹

Tactic:
rw [mul_bot_of_neg (EReal.coe_neg'.2 x_neg), inv_top, inv_bot, mul_zero]

Result:
no goals

Proof state:
case bot_bot

⊢ (⊥ * ⊥)⁻¹ = ⊥⁻¹ * ⊥⁻¹

Tactic:
simp

Result:
no goals

Proof state:
case symm
a b : EReal
h : (a * b)⁻¹ = a⁻¹ * b⁻¹
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹

Tactic:
exact h

Result:
no goals

Proof state:
a b : EReal
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹

Tactic:
induction a, b using EReal.induction₂_symm with
| top_top | top_zero | top_bot | zero_bot | bot_bot => simp
| @symm a b h => rw [mul_comm b a, mul_comm b⁻¹ a⁻¹]; exact h
| top_pos x x_pos => rw [top_mul_of_pos (EReal.coe_pos.2 x_pos), inv_top, zero_mul]
| top_neg x x_neg => rw [top_mul_of_neg (EReal.coe_neg'.2 x_neg), inv_bot, inv_top, zero_mul]
| pos_bot x x_pos => rw [mul_bot_of_pos (EReal.coe_pos.2 x_pos), inv_bot, mul_zero]
| coe_coe x y => rw [← coe_mul, ← coe_inv, _root_.mul_inv, coe_mul, coe_inv, coe_inv]
| neg_bot x x_neg => rw [mul_bot_of_neg (EReal.coe_neg'.2 x_neg), inv_top, inv_bot, mul_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filterMap_eq_filter (p : α → Bool) :
    filterMap (Option.guard (p ·)) = filter p

Proof state:
α : Type u_1
p : α → Bool
⊢ filterMap (Option.guard fun x => p x = true) = filter p

Tactic:
funext l

Result:
case h
α : Type u_1
p : α → Bool
l : List α
⊢ filterMap (Option.guard fun x => p x = true) l = filter p l

Proof state:
case h.nil
α : Type u_1
p : α → Bool
⊢ filterMap (Option.guard fun x => p x = true) [] = filter p []

Tactic:
rfl

Result:
no goals

Proof state:
case h.cons
α : Type u_1
p : α → Bool
a : α
l : List α
IH : filterMap (Option.guard fun x => p x = true) l = filter p l
⊢ filterMap (Option.guard fun x => p x = true) (a :: l) = filter p (a :: l)

Tactic:
by_cases pa : p a <;> simp [filterMap_cons, Option.guard, pa, ← IH]

Result:
no goals

Proof state:
case h
α : Type u_1
p : α → Bool
l : List α
⊢ filterMap (Option.guard fun x => p x = true) l = filter p l

Tactic:
induction l with
| nil => rfl
| cons a l IH => by_cases pa : p a <;> simp [filterMap_cons, Option.guard, pa, ← IH]

Result:
no goals
-- Mathlib/Analysis/Convex/StrictConvexSpace.lean
theorem lt_norm_sub_of_not_sameRay (h : ¬SameRay ℝ x y) : ‖x‖ - ‖y‖ < ‖x - y‖

Proof state:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y : E
h : ¬SameRay ℝ (x - y + y) y
⊢ ‖x - y + y‖ - ‖y‖ < ‖x - y‖

Tactic:
exact sub_lt_iff_lt_add.2 (norm_add_lt_of_not_sameRay fun H' => h <| H'.add_left SameRay.rfl)

Result:
no goals

Proof state:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y : E
h : ¬SameRay ℝ x y
⊢ ‖x‖ - ‖y‖ < ‖x - y‖

Tactic:
nth_rw 1 [← sub_add_cancel x y] at h ⊢

Result:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y : E
h : ¬SameRay ℝ (x - y + y) y
⊢ ‖x - y + y‖ - ‖y‖ < ‖x - y‖
-- Mathlib/Algebra/Order/Group/Abs.lean
theorem abs_sub_lt_iff : |a - b| < c ↔ a - b < c ∧ b - a < c

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c : α
⊢ |a - b| < c ↔ a - b < c ∧ b - a < c

Tactic:
rw [abs_lt, neg_lt_sub_iff_lt_add', sub_lt_iff_lt_add', and_comm, sub_lt_iff_lt_add']

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem inv_eq_of_aeval_divX_ne_zero {x : L} {p : K[X]} (aeval_ne : aeval x (divX p) ≠ 0) :
    x⁻¹ = aeval x (divX p) / (aeval x p - algebraMap _ _ (p.coeff 0))

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_ne : (aeval x) p.divX ≠ 0
⊢ (aeval x) p.divX ≠ 0

Tactic:
exact aeval_ne

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_ne : (aeval x) p.divX ≠ 0
⊢ x⁻¹ = (aeval x) p.divX / ((aeval x) p - (algebraMap K L) (p.coeff 0))

Tactic:
rw [inv_eq_iff_eq_inv, inv_div, eq_comm, div_eq_iff, sub_eq_iff_eq_add, mul_comm]

Result:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_ne : (aeval x) p.divX ≠ 0
⊢ (aeval x) p = (aeval x) p.divX * x + (algebraMap K L) (p.coeff 0)

K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_ne : (aeval x) p.divX ≠ 0
⊢ (aeval x) p.divX ≠ 0

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_ne : (aeval x) p.divX ≠ 0
⊢ (aeval x) p = (aeval x) p.divX * x + (algebraMap K L) (p.coeff 0)

K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_ne : (aeval x) p.divX ≠ 0
⊢ (aeval x) p.divX ≠ 0

Tactic:
conv_lhs => rw [← divX_mul_X_add p]

Result:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_ne : (aeval x) p.divX ≠ 0
⊢ (aeval x) (p.divX * X + C (p.coeff 0)) = (aeval x) p.divX * x + (algebraMap K L) (p.coeff 0)

K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_ne : (aeval x) p.divX ≠ 0
⊢ (aeval x) p.divX ≠ 0

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_ne : (aeval x) p.divX ≠ 0
⊢ (aeval x) (p.divX * X + C (p.coeff 0)) = (aeval x) p.divX * x + (algebraMap K L) (p.coeff 0)

Tactic:
rw [map_add, map_mul, aeval_X, aeval_C]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Chain.lean
lemma lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_right [LieRing.IsNilpotent H]
    (hq : genWeightSpace M (q • α + χ) = ⊥)
    {x : L} (hx : x ∈ rootSpace H α)
    {y : M} (hy : y ∈ genWeightSpaceChain M α χ p q) :
    ⁅x, y⁆ ∈ genWeightSpaceChain M α χ p q

Proof state:
case hN.mk.inl
R : Type u_1
L : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p : ℤ
inst✝ : LieRing.IsNilpotent ↥H
x : L
hx : x ∈ rootSpace H α
y z : M
k : ℤ
hq : genWeightSpace M ((k + 1) • α + χ) = ⊥
hk : k ∈ Ioo p (k + 1)
hz : z ∈ genWeightSpace M (↑⟨k, hk⟩ • α + χ)
⊢ genWeightSpace M ((k + 1) • α + χ) ≤ ⨆ k_1 ∈ Ioo p (k + 1), genWeightSpace M (k_1 • α + χ)

Tactic:
simp only [hq, bot_le]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem mul_sumInl_toMatrix_prod [Fintype n] [Fintype p] (M : Matrix n n R)
    (L : List (TransvectionStruct n R)) (N : Matrix p p R) :
    fromBlocks M 0 0 N * (L.map (toMatrix ∘ sumInl p)).prod =
      fromBlocks (M * (L.map toMatrix).prod) 0 0 N

Proof state:
case cons
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH :
  ∀ (M : Matrix n n R) (N : Matrix p p R),
    fromBlocks M 0 0 N * (List.map (toMatrix ∘ sumInl p) L).prod = fromBlocks (M * (List.map toMatrix L).prod) 0 0 N
M : Matrix n n R
N : Matrix p p R
⊢ fromBlocks M 0 0 N * (List.map (toMatrix ∘ sumInl p) (t :: L)).prod =
    fromBlocks (M * (List.map toMatrix (t :: L)).prod) 0 0 N

Tactic:
simp [IH, toMatrix_sumInl, fromBlocks_multiply]

Result:
no goals

Proof state:
case nil
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
M : Matrix n n R
N : Matrix p p R
⊢ fromBlocks M 0 0 N * (List.map (toMatrix ∘ sumInl p) []).prod = fromBlocks (M * (List.map toMatrix []).prod) 0 0 N

Tactic:
simp

Result:
no goals

Proof state:
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
M : Matrix n n R
L : List (TransvectionStruct n R)
N : Matrix p p R
⊢ fromBlocks M 0 0 N * (List.map (toMatrix ∘ sumInl p) L).prod = fromBlocks (M * (List.map toMatrix L).prod) 0 0 N

Tactic:
induction L generalizing M N with
| nil => simp
| cons t L IH => simp [IH, toMatrix_sumInl, fromBlocks_multiply]

Result:
no goals
-- Mathlib/Order/Category/FinBddDistLat.lean
lemma id_apply (X : FinBddDistLat) (x : X) :
    (𝟙 X : X ⟶ X) x = x

Proof state:
X : FinBddDistLat
x : ↑X.toDistLat
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean
theorem u_exists :
    ∃ u : E → ℝ,
      ContDiff ℝ ∞ u ∧ (∀ x, u x ∈ Icc (0 : ℝ) 1) ∧ support u = ball 0 1 ∧ ∀ x, u (-x) = u x

Proof state:
case intro.intro.intro.refine_3.refine_1.h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
A : IsOpen (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), f x ∈ Icc 0 1
x : E
hx : x ∈ ball 0 1
this : 0 < f x
⊢ 0 < (f x + f (-x)) / 2

Tactic:
linarith [(B (-x)).1]

Result:
no goals

Proof state:
case intro.intro.intro.refine_3.refine_1.h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
A : IsOpen (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), f x ∈ Icc 0 1
x : E
hx : x ∈ ball 0 1
⊢ 0 < (f x + f (-x)) / 2

Tactic:
have : 0 < f x := by
  apply lt_of_le_of_ne (B x).1 (Ne.symm _)
  rwa [← f_support] at hx

Result:
case intro.intro.intro.refine_3.refine_1.h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
A : IsOpen (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), f x ∈ Icc 0 1
x : E
hx : x ∈ ball 0 1
this : 0 < f x
⊢ 0 < (f x + f (-x)) / 2

Proof state:
case intro.intro.intro.refine_3.refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
A : IsOpen (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), f x ∈ Icc 0 1
x : E
hx : x ∉ ball 0 1
I1 : f x = 0
I2 : f (-x) = 0
⊢ (f x + f (-x)) / 2 = 0

Tactic:
simp only [I1, I2, add_zero, zero_div]

Result:
no goals
-- Mathlib/Data/Matrix/Block.lean
theorem fromBlocks_smul [SMul R α] (x : R) (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α)
    (D : Matrix o m α) : x • fromBlocks A B C D = fromBlocks (x • A) (x • B) (x • C) (x • D)

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
⊢ x • fromBlocks A B C D = fromBlocks (x • A) (x • B) (x • C) (x • D)

Tactic:
ext i j

Result:
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
i : n ⊕ o
j : l ⊕ m
⊢ (x • fromBlocks A B C D) i j = fromBlocks (x • A) (x • B) (x • C) (x • D) i j

Proof state:
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
α : Type u_12
inst✝ : SMul R α
x : R
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
i : n ⊕ o
j : l ⊕ m
⊢ (x • fromBlocks A B C D) i j = fromBlocks (x • A) (x • B) (x • C) (x • D) i j

Tactic:
rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> simp [fromBlocks]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ico_bot : Ico ⊥ a = Iio a

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderBot α
a : α
⊢ Ico ⊥ a = Iio a

Tactic:
simp [← Ici_inter_Iio]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Basic.lean
lemma zero_add_inv_app (h : ShiftMkCore C A) (n : A) (X : C) :
    (h.add 0 n).inv.app X = (h.F n).map (h.zero.hom.app X) ≫
      eqToHom (by dsimp; rw [zero_add])

Proof state:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ (h.add 0 n).inv.app X = (h.F n).map (h.zero.hom.app X) ≫ eqToHom ⋯

Tactic:
rw [← cancel_epi ((h.add 0 n).hom.app X), Iso.hom_inv_id_app, h.zero_add_hom_app,
  Category.assoc, ← Functor.map_comp_assoc, Iso.inv_hom_id_app, Functor.map_id,
  Category.id_comp, eqToHom_trans, eqToHom_refl]

Result:
no goals

Proof state:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ (h.F n).obj X = (h.F (0 + n)).obj X

Tactic:
rw [zero_add]

Result:
no goals

Proof state:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ (h.F n).obj ((𝟭 C).obj X) = (h.F (0 + n)).obj X

Tactic:
dsimp

Result:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ (h.F n).obj X = (h.F (0 + n)).obj X