harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Shift/Basic.lean
@[reassoc]
lemma shiftFunctorAdd'_assoc_inv_app (a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A)
    (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃) (h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) (X : C) :
    ((shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).inv.app X)⟦a₃⟧' ≫
      (shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ (by rw [← h₁₂, h₁₂₃])).inv.app X =
    (shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).inv.app (X⟦a₁⟧) ≫
      (shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ (by rw [← h₂₃, ← add_assoc, h₁₂₃])).inv.app X

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₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
X : C
⊢ a₁ + a₂₃ = a₁₂₃

Tactic:
rw [← h₂₃, ← add_assoc, h₁₂₃]

Result:
no goals

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₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
X : C
⊢ a₁₂ + a₃ = a₁₂₃

Tactic:
rw [← h₁₂, h₁₂₃]

Result:
no goals

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₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
X : C
⊢ (shiftFunctor C a₃).map ((shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).inv.app X) ≫
      (shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ ⋯).inv.app X =
    (shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).inv.app ((shiftFunctor C a₁).obj X) ≫
      (shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ⋯).inv.app X

Tactic:
simpa using NatTrans.congr_app (congr_arg Iso.inv
  (shiftFunctorAdd'_assoc C _ _ _ _ _ _ h₁₂ h₂₃ h₁₂₃)) X

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Limits/Products.lean
theorem prod_topology {X Y : TopCat.{u}} :
    (X ⨯ Y).str =
      induced (Limits.prod.fst : X ⨯ Y ⟶ _) X.str ⊓
        induced (Limits.prod.snd : X ⨯ Y ⟶ _) Y.str

Proof state:
X Y : TopCat
homeo : ↑(X ⨯ Y) ≃ₜ ↑(of (↑X × ↑Y)) := homeoOfIso (X.prodIsoProd Y)
⊢ induced (⇑homeo) (induced Prod.fst X.str ⊓ induced Prod.snd Y.str) =
    induced (⇑(ConcreteCategory.hom prod.fst)) X.str ⊓ induced (⇑(ConcreteCategory.hom prod.snd)) Y.str

Tactic:
simp [induced_compose]

Result:
X Y : TopCat
homeo : ↑(X ⨯ Y) ≃ₜ ↑(of (↑X × ↑Y)) := homeoOfIso (X.prodIsoProd Y)
⊢ induced (Prod.fst ∘ ⇑homeo) X.str ⊓ induced (Prod.snd ∘ ⇑homeo) Y.str =
    induced (⇑(ConcreteCategory.hom prod.fst)) X.str ⊓ induced (⇑(ConcreteCategory.hom prod.snd)) Y.str

Proof state:
X Y : TopCat
⊢ (X ⨯ Y).str = induced (⇑(ConcreteCategory.hom prod.fst)) X.str ⊓ induced (⇑(ConcreteCategory.hom prod.snd)) Y.str

Tactic:
let homeo := homeoOfIso (prodIsoProd X Y)

Result:
X Y : TopCat
homeo : ↑(X ⨯ Y) ≃ₜ ↑(of (↑X × ↑Y)) := homeoOfIso (X.prodIsoProd Y)
⊢ (X ⨯ Y).str = induced (⇑(ConcreteCategory.hom prod.fst)) X.str ⊓ induced (⇑(ConcreteCategory.hom prod.snd)) Y.str

Proof state:
X Y : TopCat
homeo : ↑(X ⨯ Y) ≃ₜ ↑(of (↑X × ↑Y)) := homeoOfIso (X.prodIsoProd Y)
⊢ induced (⇑homeo) (of (↑X × ↑Y)).str =
    induced (⇑(ConcreteCategory.hom prod.fst)) X.str ⊓ induced (⇑(ConcreteCategory.hom prod.snd)) Y.str

Tactic:
change induced homeo (_ ⊓ _) = _

Result:
X Y : TopCat
homeo : ↑(X ⨯ Y) ≃ₜ ↑(of (↑X × ↑Y)) := homeoOfIso (X.prodIsoProd Y)
⊢ induced (⇑homeo) (induced Prod.fst X.str ⊓ induced Prod.snd Y.str) =
    induced (⇑(ConcreteCategory.hom prod.fst)) X.str ⊓ induced (⇑(ConcreteCategory.hom prod.snd)) Y.str

Proof state:
X Y : TopCat
homeo : ↑(X ⨯ Y) ≃ₜ ↑(of (↑X × ↑Y)) := homeoOfIso (X.prodIsoProd Y)
⊢ induced (Prod.fst ∘ ⇑homeo) X.str ⊓ induced (Prod.snd ∘ ⇑homeo) Y.str =
    induced (⇑(ConcreteCategory.hom prod.fst)) X.str ⊓ induced (⇑(ConcreteCategory.hom prod.snd)) Y.str

Tactic:
rfl

Result:
no goals

Proof state:
X Y : TopCat
homeo : ↑(X ⨯ Y) ≃ₜ ↑(of (↑X × ↑Y)) := homeoOfIso (X.prodIsoProd Y)
⊢ (X ⨯ Y).str = induced (⇑(ConcreteCategory.hom prod.fst)) X.str ⊓ induced (⇑(ConcreteCategory.hom prod.snd)) Y.str

Tactic:
refine homeo.isInducing.eq_induced.trans ?_

Result:
X Y : TopCat
homeo : ↑(X ⨯ Y) ≃ₜ ↑(of (↑X × ↑Y)) := homeoOfIso (X.prodIsoProd Y)
⊢ induced (⇑homeo) (of (↑X × ↑Y)).str =
    induced (⇑(ConcreteCategory.hom prod.fst)) X.str ⊓ induced (⇑(ConcreteCategory.hom prod.snd)) Y.str
-- Mathlib/Algebra/Ring/Parity.lean
lemma iterate_odd (hf : Involutive f) (hn : Odd n) : f^[n] = f

Proof state:
case intro
α : Type u_4
f : α → α
hf : Involutive f
m : ℕ
⊢ f^[2 * m + 1] = f

Tactic:
rw [iterate_add, hf.iterate_two_mul, id_comp, iterate_one]

Result:
no goals

Proof state:
α : Type u_4
f : α → α
n : ℕ
hf : Involutive f
hn : Odd n
⊢ f^[n] = f

Tactic:
obtain ⟨m, rfl⟩ := hn

Result:
case intro
α : Type u_4
f : α → α
hf : Involutive f
m : ℕ
⊢ f^[2 * m + 1] = f
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Bootstrap.lean
theorem toList_appendList (arr : Array α) (l : List α) :
    (arr ++ l).toList = arr.toList ++ l

Proof state:
α : Type u_1
arr : Array α
l : List α
⊢ (arr.appendList l).toList = arr.toList ++ l

Tactic:
unfold Array.appendList

Result:
α : Type u_1
arr : Array α
l : List α
⊢ (List.foldl (fun r v => r.push v) arr l).toList = arr.toList ++ l

Proof state:
α : Type u_1
arr : Array α
l : List α
⊢ (List.foldl (fun r v => r.push v) arr l).toList = arr.toList ++ l

Tactic:
induction l generalizing arr <;> simp [*]

Result:
no goals

Proof state:
α : Type u_1
arr : Array α
l : List α
⊢ (arr ++ l).toList = arr.toList ++ l

Tactic:
rw [← appendList_eq_append]

Result:
α : Type u_1
arr : Array α
l : List α
⊢ (arr.appendList l).toList = arr.toList ++ l
-- Mathlib/Analysis/Convex/StrictConvexSpace.lean
theorem StrictConvexSpace.of_norm_add
    (h : ∀ x y : E, ‖x‖ = 1 → ‖y‖ = 1 → ‖x + y‖ = 2 → SameRay ℝ x y) : StrictConvexSpace ℝ E

Proof state:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → ‖x + y‖ = 2 → SameRay ℝ x y
⊢ StrictConvexSpace ℝ E

Tactic:
refine StrictConvexSpace.of_pairwise_sphere_norm_ne_two fun x hx y hy => mt fun h₂ => ?_

Result:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → ‖x + y‖ = 2 → SameRay ℝ x y
x : E
hx : x ∈ sphere 0 1
y : E
hy : y ∈ sphere 0 1
h₂ : ‖x + y‖ = 2
⊢ x = y

Proof state:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → ‖x + y‖ = 2 → SameRay ℝ x y
x : E
hx : ‖x‖ = 1
y : E
hy : ‖y‖ = 1
h₂ : ‖x + y‖ = 2
⊢ x = y

Tactic:
exact (sameRay_iff_of_norm_eq (hx.trans hy.symm)).1 (h x y hx hy h₂)

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → ‖x + y‖ = 2 → SameRay ℝ x y
x : E
hx : x ∈ sphere 0 1
y : E
hy : y ∈ sphere 0 1
h₂ : ‖x + y‖ = 2
⊢ x = y

Tactic:
rw [mem_sphere_zero_iff_norm] at hx hy

Result:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → ‖x + y‖ = 2 → SameRay ℝ x y
x : E
hx : ‖x‖ = 1
y : E
hy : ‖y‖ = 1
h₂ : ‖x + y‖ = 2
⊢ x = y
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem cos_oangle_add_left_mul_norm_of_oangle_eq_pi_div_two {x y : V}
    (h : o.oangle x y = ↑(π / 2)) : Real.Angle.cos (o.oangle (x + y) y) * ‖x + y‖ = ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ((-o).oangle y (x + y)).cos * ‖x + y‖ = ‖y‖

Tactic:
rw [add_comm]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ((-o).oangle y (y + x)).cos * ‖y + x‖ = ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle (x + y) y).cos * ‖x + y‖ = ‖y‖

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ((-o).oangle y (x + y)).cos * ‖x + y‖ = ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ((-o).oangle y (y + x)).cos * ‖y + x‖ = ‖y‖

Tactic:
exact (-o).cos_oangle_add_right_mul_norm_of_oangle_eq_pi_div_two h

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem abs_re_div_norm_le_one (z : K) : |re z / ‖z‖| ≤ 1

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ |re z| / ‖z‖ ≤ 1

Tactic:
exact div_le_one_of_le₀ (abs_re_le_norm _) (norm_nonneg _)

Result:
no goals

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ |re z / ‖z‖| ≤ 1

Tactic:
rw [abs_div, abs_norm]

Result:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ |re z| / ‖z‖ ≤ 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem mul_tmod_right (a b : Int) : (a * b).tmod a = 0

Proof state:
a b : Int
⊢ (a * b).tmod a = 0

Tactic:
rw [Int.mul_comm, mul_tmod_left]

Result:
no goals
-- Mathlib/Data/Set/Sigma.lean
theorem preimage_image_sigmaMk_of_ne (h : i ≠ j) (s : Set (α j)) :
    Sigma.mk i ⁻¹' (Sigma.mk j '' s) = ∅

Proof state:
ι : Type u_1
α : ι → Type u_3
i j : ι
h : i ≠ j
s : Set (α j)
⊢ Sigma.mk i ⁻¹' (Sigma.mk j '' s) = ∅

Tactic:
ext x

Result:
case h
ι : Type u_1
α : ι → Type u_3
i j : ι
h : i ≠ j
s : Set (α j)
x : α i
⊢ x ∈ Sigma.mk i ⁻¹' (Sigma.mk j '' s) ↔ x ∈ ∅

Proof state:
case h
ι : Type u_1
α : ι → Type u_3
i j : ι
h : i ≠ j
s : Set (α j)
x : α i
⊢ x ∈ Sigma.mk i ⁻¹' (Sigma.mk j '' s) ↔ x ∈ ∅

Tactic:
simp [h.symm]

Result:
no goals
-- Mathlib/Data/Nat/Multiplicity.lean
theorem emultiplicity_choose_prime_pow {p n k : ℕ} (hp : p.Prime) (hkn : k ≤ p ^ n) (hk0 : k ≠ 0) :
    emultiplicity p (choose (p ^ n) k) = ↑(n - multiplicity p k)

Proof state:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ emultiplicity p ((p ^ n).choose k) = ↑(n - multiplicity p k)

Tactic:
push_cast

Result:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ emultiplicity p ((p ^ n).choose k) = ↑n - ↑(multiplicity p k)

Proof state:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ emultiplicity p ((p ^ n).choose k) = ↑n - ↑(multiplicity p k)

Tactic:
rw [← emultiplicity_choose_prime_pow_add_emultiplicity hp hkn hk0,
  (finiteMultiplicity_iff.2 ⟨hp.ne_one, Nat.pos_of_ne_zero hk0⟩).emultiplicity_eq_multiplicity,
  (finiteMultiplicity_iff.2 ⟨hp.ne_one, choose_pos hkn⟩).emultiplicity_eq_multiplicity]

Result:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ ↑(multiplicity p ((p ^ n).choose k)) =
    ↑(multiplicity p ((p ^ n).choose k)) + ↑(multiplicity p k) - ↑(multiplicity p k)

Proof state:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ ↑(multiplicity p ((p ^ n).choose k)) =
    ↑(multiplicity p ((p ^ n).choose k)) + ↑(multiplicity p k) - ↑(multiplicity p k)

Tactic:
norm_cast

Result:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ multiplicity p ((p ^ n).choose k) = multiplicity p ((p ^ n).choose k) + multiplicity p k - multiplicity p k

Proof state:
p n k : ℕ
hp : Prime p
hkn : k ≤ p ^ n
hk0 : k ≠ 0
⊢ multiplicity p ((p ^ n).choose k) = multiplicity p ((p ^ n).choose k) + multiplicity p k - multiplicity p k

Tactic:
rw [Nat.add_sub_cancel_right]

Result:
no goals
-- Mathlib/LinearAlgebra/GeneralLinearGroup.lean
theorem generalLinearEquiv_to_linearMap (f : GeneralLinearGroup R M) :
    (generalLinearEquiv R M f : M →ₗ[R] M) = f

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : GeneralLinearGroup R M
x✝ : M
⊢ ↑((generalLinearEquiv R M) f) x✝ = ↑f x✝

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : GeneralLinearGroup R M
⊢ ↑((generalLinearEquiv R M) f) = ↑f

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : GeneralLinearGroup R M
x✝ : M
⊢ ↑((generalLinearEquiv R M) f) x✝ = ↑f x✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem succ_sub_succ_eq_sub (n m : Nat) : succ n - succ m = n - m

Proof state:
n m : Nat
⊢ n.succ - m.succ = n - m

Tactic:
induction m with
| zero      => exact rfl
| succ m ih => apply congrArg pred ih

Result:
no goals

Proof state:
case succ
n m : Nat
ih : n.succ - m.succ = n - m
⊢ n.succ - (m + 1).succ = n - (m + 1)

Tactic:
apply congrArg pred ih

Result:
no goals

Proof state:
case zero
n : Nat
⊢ n.succ - succ 0 = n - 0

Tactic:
exact rfl

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Valid'.dual_iff {t : Ordnode α} {o₁ o₂} : Valid' o₁ t o₂ ↔ @Valid' αᵒᵈ _ o₂ (.dual t) o₁ :=
  ⟨Valid'.dual, fun h => by
    have := Valid'.dual h; rwa [dual_dual, OrderDual.Preorder.dual_dual] at this⟩

Proof state:
α : Type u_1
inst✝ : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₂ t.dual o₁
this : Valid' o₁ t.dual.dual o₂
⊢ Valid' o₁ t o₂

Tactic:
rwa [dual_dual, OrderDual.Preorder.dual_dual] at this

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₂ t.dual o₁
⊢ Valid' o₁ t o₂

Tactic:
have := Valid'.dual h

Result:
α : Type u_1
inst✝ : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₂ t.dual o₁
this : Valid' o₁ t.dual.dual o₂
⊢ Valid' o₁ t o₂
-- Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean
lemma isIso₁_of_isIso₂₃ {T T' : Triangle C} (φ : T ⟶ T') (hT : T ∈ distTriang C)
    (hT' : T' ∈ distTriang C) (h₂ : IsIso φ.hom₂) (h₃ : IsIso φ.hom₃) : IsIso φ.hom₁ :=
  isIso₂_of_isIso₁₃ ((invRotate C).map φ) (inv_rot_of_distTriang _ hT)
    (inv_rot_of_distTriang _ hT') (by dsimp; infer_instance) (by dsimp; infer_instance)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T T' : Triangle C
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₂ : IsIso φ.hom₂
h₃ : IsIso φ.hom₃
⊢ IsIso φ.hom₂

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T T' : Triangle C
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₂ : IsIso φ.hom₂
h₃ : IsIso φ.hom₃
⊢ IsIso ((invRotate C).map φ).hom₁

Tactic:
dsimp

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T T' : Triangle C
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₂ : IsIso φ.hom₂
h₃ : IsIso φ.hom₃
⊢ IsIso ((shiftFunctor C (-1)).map φ.hom₃)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T T' : Triangle C
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₂ : IsIso φ.hom₂
h₃ : IsIso φ.hom₃
⊢ IsIso ((invRotate C).map φ).hom₃

Tactic:
dsimp

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T T' : Triangle C
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₂ : IsIso φ.hom₂
h₃ : IsIso φ.hom₃
⊢ IsIso φ.hom₂

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T T' : Triangle C
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₂ : IsIso φ.hom₂
h₃ : IsIso φ.hom₃
⊢ IsIso ((shiftFunctor C (-1)).map φ.hom₃)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/PairingHeap.lean
theorem Heap.WF.tail? (hwf : (s : Heap α).WF le) : s.tail? le = some tl →
  tl.WF le

Proof state:
α : Type u_1
s : Heap α
le : α → α → Bool
tl✝ : Heap α
hwf : WF le s
eq : Option.map (fun x => x.snd) (Heap.deleteMin le s) = some tl✝
a : α
tl : Heap α
eq₂ : Heap.deleteMin le s = some (a, tl)
⊢ WF le ((fun x => x.snd) (a, tl))

Tactic:
exact hwf.deleteMin eq₂

Result:
no goals

Proof state:
α : Type u_1
s : Heap α
le : α → α → Bool
tl : Heap α
hwf : WF le s
eq : Option.map (fun x => x.snd) (Heap.deleteMin le s) = some tl
⊢ WF le tl

Tactic:
match eq₂ : s.deleteMin le, eq with
| some (a, tl), rfl => exact hwf.deleteMin eq₂

Result:
no goals

Proof state:
α : Type u_1
s : Heap α
le : α → α → Bool
tl : Heap α
hwf : WF le s
⊢ Option.map (fun x => x.snd) (Heap.deleteMin le s) = some tl → WF le tl

Tactic:
intro eq

Result:
α : Type u_1
s : Heap α
le : α → α → Bool
tl : Heap α
hwf : WF le s
eq : Option.map (fun x => x.snd) (Heap.deleteMin le s) = some tl
⊢ WF le tl

Proof state:
α : Type u_1
s : Heap α
le : α → α → Bool
tl : Heap α
hwf : WF le s
⊢ Heap.tail? le s = some tl → WF le tl

Tactic:
simp only [Heap.tail?]

Result:
α : Type u_1
s : Heap α
le : α → α → Bool
tl : Heap α
hwf : WF le s
⊢ Option.map (fun x => x.snd) (Heap.deleteMin le s) = some tl → WF le tl
-- Mathlib/Topology/MetricSpace/Thickening.lean
/-- Any set is contained in the complement of the δ-thickening of the complement of its
δ-thickening. -/
lemma subset_compl_thickening_compl_thickening_self (δ : ℝ) (E : Set α) :
    E ⊆ (thickening δ (thickening δ E)ᶜ)ᶜ

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ E ⊆ (thickening δ (thickening δ E)ᶜ)ᶜ

Tactic:
intro x x_in_E

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_in_E : x ∈ E
⊢ x ∈ (thickening δ (thickening δ E)ᶜ)ᶜ

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_in_E : x ∈ E
y : α
hy : y ∈ {x | infEdist x E < ENNReal.ofReal δ}ᶜ
⊢ ENNReal.ofReal δ ≤ edist x y

Tactic:
simp only [mem_compl_iff, mem_setOf_eq, not_lt] at hy

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_in_E : x ∈ E
y : α
hy : ENNReal.ofReal δ ≤ infEdist y E
⊢ ENNReal.ofReal δ ≤ edist x y

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_in_E : x ∈ E
⊢ x ∈ (thickening δ (thickening δ E)ᶜ)ᶜ

Tactic:
simp only [thickening, mem_compl_iff, mem_setOf_eq, not_lt]

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_in_E : x ∈ E
⊢ ENNReal.ofReal δ ≤ infEdist x {x | infEdist x E < ENNReal.ofReal δ}ᶜ

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_in_E : x ∈ E
y : α
hy : ENNReal.ofReal δ ≤ infEdist y E
⊢ ENNReal.ofReal δ ≤ edist x y

Tactic:
simpa only [edist_comm] using le_trans hy <| EMetric.infEdist_le_edist_of_mem x_in_E

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_in_E : x ∈ E
⊢ ENNReal.ofReal δ ≤ infEdist x {x | infEdist x E < ENNReal.ofReal δ}ᶜ

Tactic:
apply EMetric.le_infEdist.mpr fun y hy ↦ ?_

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_in_E : x ∈ E
y : α
hy : y ∈ {x | infEdist x E < ENNReal.ofReal δ}ᶜ
⊢ ENNReal.ofReal δ ≤ edist x y
-- Mathlib/Algebra/Polynomial/Roots.lean
lemma eq_zero_of_forall_eval_zero_of_natDegree_lt_card
    (f : R[X]) (hf : ∀ r, f.eval r = 0) (hfR : f.natDegree < #R) : f = 0

Proof state:
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
hf : ∀ (r : R), eval r f = 0
hfR : ↑f.natDegree < #R
hR : Infinite R
⊢ f = 0

Tactic:
exact zero_of_eval_zero _ hf

Result:
no goals

Proof state:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
hf : ∀ (r : R), eval r f = 0
hfR : ↑f.natDegree < #R
hR : Finite R
⊢ f = 0

Tactic:
have := Fintype.ofFinite R

Result:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
hf : ∀ (r : R), eval r f = 0
hfR : ↑f.natDegree < #R
hR : Finite R
this : Fintype R
⊢ f = 0

Proof state:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
hf : ∀ (r : R), eval r f = 0
hfR : ↑f.natDegree < #R
hR : Finite R
this : Fintype R
⊢ f = 0

Tactic:
apply eq_zero_of_natDegree_lt_card_of_eval_eq_zero f Function.injective_id hf

Result:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
hf : ∀ (r : R), eval r f = 0
hfR : ↑f.natDegree < #R
hR : Finite R
this : Fintype R
⊢ f.natDegree < Fintype.card R

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
hf : ∀ (r : R), eval r f = 0
hfR : ↑f.natDegree < #R
⊢ f = 0

Tactic:
obtain hR|hR := finite_or_infinite R

Result:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
hf : ∀ (r : R), eval r f = 0
hfR : ↑f.natDegree < #R
hR : Finite R
⊢ f = 0

case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
hf : ∀ (r : R), eval r f = 0
hfR : ↑f.natDegree < #R
hR : Infinite R
⊢ f = 0

Proof state:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
hf : ∀ (r : R), eval r f = 0
hfR : ↑f.natDegree < #R
hR : Finite R
this : Fintype R
⊢ f.natDegree < Fintype.card R

Tactic:
simpa only [mk_fintype, Nat.cast_lt] using hfR

Result:
no goals
-- Mathlib/Data/ENNReal/Order.lean
theorem sub_mul (h : 0 < b → b < a → c ≠ ∞) : (a - b) * c = a * c - b * c

Proof state:
case inl
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ ⊤
hab : a ≤ b
⊢ (a - b) * c = a * c - b * c

Tactic:
simp [hab, mul_right_mono hab, tsub_eq_zero_of_le]

Result:
no goals

Proof state:
case inr.inr
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ ⊤
hab : b < a
hb : 0 < b
⊢ (a - b) * c = a * c - b * c

Tactic:
exact (cancel_of_ne <| mul_ne_top hab.ne_top (h hb hab)).tsub_mul

Result:
no goals

Proof state:
case inr
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ ⊤
hab : b < a
⊢ (a - b) * c = a * c - b * c

Tactic:
rcases eq_or_lt_of_le (zero_le b) with (rfl | hb)

Result:
case inr.inl
a c : ℝ≥0∞
h : 0 < 0 → 0 < a → c ≠ ⊤
hab : 0 < a
⊢ (a - 0) * c = a * c - 0 * c

case inr.inr
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ ⊤
hab : b < a
hb : 0 < b
⊢ (a - b) * c = a * c - b * c

Proof state:
case inr.inl
a c : ℝ≥0∞
h : 0 < 0 → 0 < a → c ≠ ⊤
hab : 0 < a
⊢ (a - 0) * c = a * c - 0 * c

Tactic:
simp

Result:
no goals

Proof state:
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ ⊤
⊢ (a - b) * c = a * c - b * c

Tactic:
rcases le_or_lt a b with hab | hab

Result:
case inl
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ ⊤
hab : a ≤ b
⊢ (a - b) * c = a * c - b * c

case inr
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ ⊤
hab : b < a
⊢ (a - b) * c = a * c - b * c
-- Mathlib/Algebra/Lie/Solvable.lean
theorem derivedSeries_eq_top (n : ℕ) (h : derivedSeries R L 1 = ⊤) :
    derivedSeries R L n = ⊤

Proof state:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : derivedSeries R L 1 = ⊤
n✝ : ℕ
⊢ derivedSeries R L (n✝ + 1) = ⊤

Tactic:
rwa [derivedSeries_succ_eq_top_iff]

Result:
no goals

Proof state:
case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : derivedSeries R L 1 = ⊤
⊢ derivedSeries R L 0 = ⊤

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
n : ℕ
h : derivedSeries R L 1 = ⊤
⊢ derivedSeries R L n = ⊤

Tactic:
cases n

Result:
case zero
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : derivedSeries R L 1 = ⊤
⊢ derivedSeries R L 0 = ⊤

case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : derivedSeries R L 1 = ⊤
n✝ : ℕ
⊢ derivedSeries R L (n✝ + 1) = ⊤
-- Mathlib/Algebra/Ring/Divisibility/Basic.lean
theorem dvd_iff_dvd_of_dvd_sub (h : a ∣ b - c) : a ∣ b ↔ a ∣ c

Proof state:
α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b - c
⊢ a ∣ b ↔ a ∣ c

Tactic:
rw [← sub_add_cancel b c, dvd_add_right h]

Result:
no goals