harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Monoidal/Hopf_.lean
theorem antipode_counit (A : Hopf_ C) : A.antipode ≫ A.X.counit.hom = A.X.counit.hom

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
this :
  A.X.comul.hom ≫
      A.X.X.X ◁ A.X.counit.hom ≫
        A.antipode ▷ (𝟙_ (Mon_ C)).X ≫ A.X.counit.hom ▷ (𝟙_ (Mon_ C)).X ≫ (λ_ (𝟙_ (Mon_ C)).X).hom =
    A.X.counit.hom ≫ A.X.X.one ≫ A.X.counit.hom
⊢ A.antipode ≫ A.X.counit.hom = A.X.counit.hom

Tactic:
simpa [unitors_equal]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
this : A.X.comul.hom ≫ A.antipode ▷ A.X.X.X ≫ A.X.X.mul ≫ A.X.counit.hom = A.X.counit.hom ≫ A.X.X.one ≫ A.X.counit.hom
⊢ A.antipode ≫ A.X.counit.hom = A.X.counit.hom

Tactic:
rw [A.X.mul_counit, tensorHom_def', Category.assoc, ← whisker_exchange_assoc] at this

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
this :
  A.X.comul.hom ≫
      A.X.X.X ◁ A.X.counit.hom ≫
        A.antipode ▷ (𝟙_ (Mon_ C)).X ≫ A.X.counit.hom ▷ (𝟙_ (Mon_ C)).X ≫ (λ_ (𝟙_ (Mon_ C)).X).hom =
    A.X.counit.hom ≫ A.X.X.one ≫ A.X.counit.hom
⊢ A.antipode ≫ A.X.counit.hom = A.X.counit.hom

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
⊢ A.antipode ≫ A.X.counit.hom = A.X.counit.hom

Tactic:
have := (rfl : A.X.comul.hom ≫ (A.antipode ▷ A.X.X.X) ≫ A.X.X.mul ≫ A.X.counit.hom = _)

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
this :
  A.X.comul.hom ≫ A.antipode ▷ A.X.X.X ≫ A.X.X.mul ≫ A.X.counit.hom =
    A.X.comul.hom ≫ A.antipode ▷ A.X.X.X ≫ A.X.X.mul ≫ A.X.counit.hom
⊢ A.antipode ≫ A.X.counit.hom = A.X.counit.hom

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
this :
  A.X.comul.hom ≫ A.antipode ▷ A.X.X.X ≫ A.X.X.mul ≫ A.X.counit.hom =
    A.X.comul.hom ≫ A.antipode ▷ A.X.X.X ≫ A.X.X.mul ≫ A.X.counit.hom
⊢ A.antipode ≫ A.X.counit.hom = A.X.counit.hom

Tactic:
conv at this =>
  rhs
  rw [A.antipode_left_assoc]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
A : Hopf_ C
this : A.X.comul.hom ≫ A.antipode ▷ A.X.X.X ≫ A.X.X.mul ≫ A.X.counit.hom = A.X.counit.hom ≫ A.X.X.one ≫ A.X.counit.hom
⊢ A.antipode ≫ A.X.counit.hom = A.X.counit.hom
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
lemma support_ofIdealTop (I : Ideal Γ(X, ⊤)) : (ofIdealTop I).support = X.zeroLocus (U := ⊤) I

Proof state:
case h
X : Scheme
I : Ideal ↑Γ(X, ⊤)
this : ∀ (U : ↑X.affineOpens), (ofIdealTop I).support ∩ ↑↑U = X.zeroLocus ↑I ∩ ↑↑U
x : ↑↑X.toPresheafedSpace
⊢ x ∈ (ofIdealTop I).support ↔ x ∈ X.zeroLocus ↑I

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
  (isBasis_affine_open X).exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ

Result:
case h.intro.intro.intro.intro.intro
X : Scheme
I : Ideal ↑Γ(X, ⊤)
this : ∀ (U : ↑X.affineOpens), (ofIdealTop I).support ∩ ↑↑U = X.zeroLocus ↑I ∩ ↑↑U
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
⊢ x ∈ (ofIdealTop I).support ↔ x ∈ X.zeroLocus ↑I

Proof state:
X : Scheme
I : Ideal ↑Γ(X, ⊤)
U : ↑X.affineOpens
⊢ (ofIdealTop I).support ∩ ↑↑U = X.zeroLocus ↑I ∩ ↑↑U

Tactic:
rw [support_inter, ofIdealTop_ideal, Ideal.map, zeroLocus_span, zeroLocus_map,
  Set.union_inter_distrib_right, Set.compl_inter_self, Set.union_empty]

Result:
no goals

Proof state:
X : Scheme
I : Ideal ↑Γ(X, ⊤)
⊢ (ofIdealTop I).support = X.zeroLocus ↑I

Tactic:
suffices ∀ U : X.affineOpens, (ofIdealTop I).support ∩ U = X.zeroLocus (U := ⊤) I ∩ U by
  ext x
  obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
    (isBasis_affine_open X).exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ
  simpa [hxU] using congr(x ∈ $(this ⟨U, hU⟩))

Result:
X : Scheme
I : Ideal ↑Γ(X, ⊤)
⊢ ∀ (U : ↑X.affineOpens), (ofIdealTop I).support ∩ ↑↑U = X.zeroLocus ↑I ∩ ↑↑U

Proof state:
X : Scheme
I : Ideal ↑Γ(X, ⊤)
⊢ ∀ (U : ↑X.affineOpens), (ofIdealTop I).support ∩ ↑↑U = X.zeroLocus ↑I ∩ ↑↑U

Tactic:
intro U

Result:
X : Scheme
I : Ideal ↑Γ(X, ⊤)
U : ↑X.affineOpens
⊢ (ofIdealTop I).support ∩ ↑↑U = X.zeroLocus ↑I ∩ ↑↑U

Proof state:
case h.intro.intro.intro.intro.intro
X : Scheme
I : Ideal ↑Γ(X, ⊤)
this : ∀ (U : ↑X.affineOpens), (ofIdealTop I).support ∩ ↑↑U = X.zeroLocus ↑I ∩ ↑↑U
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
⊢ x ∈ (ofIdealTop I).support ↔ x ∈ X.zeroLocus ↑I

Tactic:
simpa [hxU] using congr(x ∈ $(this ⟨U, hU⟩))

Result:
no goals

Proof state:
X : Scheme
I : Ideal ↑Γ(X, ⊤)
this : ∀ (U : ↑X.affineOpens), (ofIdealTop I).support ∩ ↑↑U = X.zeroLocus ↑I ∩ ↑↑U
⊢ (ofIdealTop I).support = X.zeroLocus ↑I

Tactic:
ext x

Result:
case h
X : Scheme
I : Ideal ↑Γ(X, ⊤)
this : ∀ (U : ↑X.affineOpens), (ofIdealTop I).support ∩ ↑↑U = X.zeroLocus ↑I ∩ ↑↑U
x : ↑↑X.toPresheafedSpace
⊢ x ∈ (ofIdealTop I).support ↔ x ∈ X.zeroLocus ↑I
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
@[simp, norm_cast]
lemma rpow_natCast (x : ℝ≥0) (n : ℕ) : x ^ (n : ℝ) = x ^ n :=
  NNReal.eq <| by simpa only [coe_rpow, coe_pow] using Real.rpow_natCast x n

Proof state:
x : ℝ≥0
n : ℕ
⊢ ↑(x ^ ↑n) = ↑(x ^ n)

Tactic:
simpa only [coe_rpow, coe_pow] using Real.rpow_natCast x n

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem dist_div_tan_oangle_left_of_oangle_eq_pi_div_two {p₁ p₂ p₃ : P}
    (h : ∡ p₁ p₂ p₃ = ↑(π / 2)) : dist p₃ p₂ / Real.Angle.tan (∡ p₃ p₁ p₂) = dist p₁ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ dist p₃ p₂ / (∡ p₃ p₁ p₂).tan = dist p₁ p₂

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.tan_coe,
  dist_div_tan_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
    (Or.inl (right_ne_of_oangle_eq_pi_div_two h))]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₃ p₁ p₂).sign = 1

Tactic:
rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ dist p₃ p₂ / (∡ p₃ p₁ p₂).tan = dist p₁ p₂

Tactic:
have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ dist p₃ p₂ / (∡ p₃ p₁ p₂).tan = dist p₁ p₂
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem xor_zero {x : BitVec w} : x ^^^ 0#w = x

Proof state:
w : Nat
x : BitVec w
⊢ x ^^^ 0#w = x

Tactic:
ext i

Result:
case pred
w : Nat
x : BitVec w
i : Nat
a✝ : i < w
⊢ (x ^^^ 0#w).getLsbD i = x.getLsbD i

Proof state:
case pred
w : Nat
x : BitVec w
i : Nat
a✝ : i < w
⊢ (x ^^^ 0#w).getLsbD i = x.getLsbD i

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem head?_filterMap (f : α → Option β) (l : List α) : (l.filterMap f).head? = l.findSome? f

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
x : α
xs : List α
ih : (filterMap f xs).head? = findSome? f xs
⊢ (filterMap f (x :: xs)).head? = findSome? f (x :: xs)

Tactic:
simp only [filterMap_cons, findSome?_cons]

Result:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
x : α
xs : List α
ih : (filterMap f xs).head? = findSome? f xs
⊢ (match f x with
      | none => filterMap f xs
      | some b => b :: filterMap f xs).head? =
    match f x with
    | some b => some b
    | none => findSome? f xs

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → Option β
⊢ (filterMap f []).head? = findSome? f []

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
x : α
xs : List α
ih : (filterMap f xs).head? = findSome? f xs
⊢ (match f x with
      | none => filterMap f xs
      | some b => b :: filterMap f xs).head? =
    match f x with
    | some b => some b
    | none => findSome? f xs

Tactic:
split <;> simp [*]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
⊢ (filterMap f l).head? = findSome? f l

Tactic:
induction l with
| nil => simp
| cons x xs ih =>
  simp only [filterMap_cons, findSome?_cons]
  split <;> simp [*]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKeyD_alter [EquivBEq α] [LawfulHashable α] {k k' fallback : α} {f : Option β → Option β}
    (h : m.WF) : (Const.alter m k f).getKeyD k' fallback =
      if k == k' then
        if (f (Const.get? m k)).isSome then k else fallback
      else
        m.getKeyD k' fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' fallback : α
f : Option β → Option β
h : m.WF
⊢ (alter m k f).getKeyD k' fallback =
    if (k == k') = true then if (f (get? m k)).isSome = true then k else fallback else m.getKeyD k' fallback

Tactic:
simp_to_raw using Raw₀.Const.getKeyD_alter

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem preimage_iInter {f : α → β} {s : ι → Set β} : (f ⁻¹' ⋂ i, s i) = ⋂ i, f ⁻¹' s i

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
s : ι → Set β
⊢ f ⁻¹' ⋂ i, s i = ⋂ i, f ⁻¹' s i

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
s : ι → Set β
x✝ : α
⊢ x✝ ∈ f ⁻¹' ⋂ i, s i ↔ x✝ ∈ ⋂ i, f ⁻¹' s i

Proof state:
case h
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
s : ι → Set β
x✝ : α
⊢ x✝ ∈ f ⁻¹' ⋂ i, s i ↔ x✝ ∈ ⋂ i, f ⁻¹' s i

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem zipIdx_succ (l : List α) (n : Nat) :
    l.zipIdx (n + 1) = (l.zipIdx n).map (fun ⟨a, i⟩ => (a, i + 1))

Proof state:
case nil
α : Type u_1
n : Nat
⊢ [].zipIdx (n + 1) =
    map
      (fun x =>
        match x with
        | (a, i) => (a, i + 1))
      ([].zipIdx n)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
l : List α
n : Nat
⊢ l.zipIdx (n + 1) =
    map
      (fun x =>
        match x with
        | (a, i) => (a, i + 1))
      (l.zipIdx n)

Tactic:
induction l generalizing n with
| nil => rfl
| cons _ _ ih => simp only [zipIdx_cons, ih (n + 1), map_cons]

Result:
no goals

Proof state:
case cons
α : Type u_1
head✝ : α
tail✝ : List α
ih :
  ∀ (n : Nat),
    tail✝.zipIdx (n + 1) =
      map
        (fun x =>
          match x with
          | (a, i) => (a, i + 1))
        (tail✝.zipIdx n)
n : Nat
⊢ (head✝ :: tail✝).zipIdx (n + 1) =
    map
      (fun x =>
        match x with
        | (a, i) => (a, i + 1))
      ((head✝ :: tail✝).zipIdx n)

Tactic:
simp only [zipIdx_cons, ih (n + 1), map_cons]

Result:
no goals
-- Mathlib/Algebra/Category/Ring/Basic.lean
lemma id_apply (R : RingCat) (r : R) :
    (𝟙 R : R ⟶ R) r = r

Proof state:
R : RingCat
r : ↑R
⊢ (ConcreteCategory.hom (𝟙 R)) r = r

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem le_findIdx_of_not {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs.length)
    (h2 : ∀ j (hji : j < i), p (xs[j]'(Nat.lt_trans hji h)) = false) : i ≤ xs.findIdx p

Proof state:
α : Type u_1
p : α → Bool
xs : List α
i : Nat
h : i < xs.length
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
⊢ i ≤ findIdx p xs

Tactic:
apply Decidable.byContradiction

Result:
case h
α : Type u_1
p : α → Bool
xs : List α
i : Nat
h : i < xs.length
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
⊢ ¬i ≤ findIdx p xs → False

Proof state:
α : Type u_1
p : α → Bool
xs : List α
i : Nat
h : i < xs.length
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
f : findIdx p xs < i
⊢ ¬p xs[findIdx p xs] = true

Tactic:
simpa using h2 (xs.findIdx p) f

Result:
no goals

Proof state:
case h
α : Type u_1
p : α → Bool
xs : List α
i : Nat
h : i < xs.length
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
⊢ ¬i ≤ findIdx p xs → False

Tactic:
intro f

Result:
case h
α : Type u_1
p : α → Bool
xs : List α
i : Nat
h : i < xs.length
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
f : ¬i ≤ findIdx p xs
⊢ False

Proof state:
case h
α : Type u_1
p : α → Bool
xs : List α
i : Nat
h : i < xs.length
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
f : ¬i ≤ findIdx p xs
⊢ False

Tactic:
simp only [Nat.not_le] at f

Result:
case h
α : Type u_1
p : α → Bool
xs : List α
i : Nat
h : i < xs.length
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
f : findIdx p xs < i
⊢ False

Proof state:
case h
α : Type u_1
p : α → Bool
xs : List α
i : Nat
h : i < xs.length
h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false
f : findIdx p xs < i
⊢ False

Tactic:
exact absurd (@findIdx_getElem _ p xs (Nat.lt_trans f h)) (by simpa using h2 (xs.findIdx p) f)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem cos_arcsin (x : ℝ) : cos (arcsin x) = √(1 - x ^ 2)

Proof state:
case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ cos (arcsin x) = √(1 - x ^ 2)

Tactic:
by_cases hx₂ : x ≤ 1

Result:
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ cos (arcsin x) = √(1 - x ^ 2)

case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ cos (arcsin x) = √(1 - x ^ 2)

Proof state:
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ cos (arcsin x) = √(1 - x ^ 2)

case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ cos (arcsin x) = √(1 - x ^ 2)

Tactic:
swap

Result:
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ cos (arcsin x) = √(1 - x ^ 2)

case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ cos (arcsin x) = √(1 - x ^ 2)

Proof state:
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ cos (arcsin x) = √(1 - x ^ 2)

Tactic:
rw [arcsin_of_one_le hx₂.le, cos_pi_div_two, sqrt_eq_zero_of_nonpos]

Result:
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ 1 - x ^ 2 ≤ 0

Proof state:
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ cos (arcsin x) = √(1 - x ^ 2)

Tactic:
rw [not_le] at hx₂

Result:
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ cos (arcsin x) = √(1 - x ^ 2)

Proof state:
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ cos (arcsin x) = √(1 - x ^ 2)

Tactic:
have : sin (arcsin x) ^ 2 + cos (arcsin x) ^ 2 = 1 := sin_sq_add_cos_sq (arcsin x)

Result:
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
this : sin (arcsin x) ^ 2 + cos (arcsin x) ^ 2 = 1
⊢ cos (arcsin x) = √(1 - x ^ 2)

Proof state:
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
this : cos (arcsin x) = √(1 - sin (arcsin x) ^ 2)
⊢ cos (arcsin x) = √(1 - x ^ 2)

Tactic:
rw [this, sin_arcsin hx₁ hx₂]

Result:
no goals

Proof state:
case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ cos (arcsin x) = √(1 - x ^ 2)

case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ cos (arcsin x) = √(1 - x ^ 2)

Tactic:
swap

Result:
case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ cos (arcsin x) = √(1 - x ^ 2)

case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ cos (arcsin x) = √(1 - x ^ 2)

Proof state:
case neg
x : ℝ
hx₁ : x < -1
⊢ 1 - x ^ 2 ≤ 0

Tactic:
nlinarith

Result:
no goals

Proof state:
case neg
x : ℝ
hx₁ : x < -1
⊢ cos (arcsin x) = √(1 - x ^ 2)

Tactic:
rw [arcsin_of_le_neg_one hx₁.le, cos_neg, cos_pi_div_two, sqrt_eq_zero_of_nonpos]

Result:
case neg
x : ℝ
hx₁ : x < -1
⊢ 1 - x ^ 2 ≤ 0

Proof state:
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
this : sin (arcsin x) ^ 2 + cos (arcsin x) ^ 2 = 1
⊢ cos (arcsin x) = √(1 - x ^ 2)

Tactic:
rw [← eq_sub_iff_add_eq', ← sqrt_inj (sq_nonneg _) (sub_nonneg.2 (sin_sq_le_one (arcsin x))), sq,
  sqrt_mul_self (cos_arcsin_nonneg _)] at this

Result:
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
this : cos (arcsin x) = √(1 - sin (arcsin x) ^ 2)
⊢ cos (arcsin x) = √(1 - x ^ 2)

Proof state:
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ 1 - x ^ 2 ≤ 0

Tactic:
nlinarith

Result:
no goals

Proof state:
x : ℝ
⊢ cos (arcsin x) = √(1 - x ^ 2)

Tactic:
by_cases hx₁ : -1 ≤ x

Result:
case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ cos (arcsin x) = √(1 - x ^ 2)

case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ cos (arcsin x) = √(1 - x ^ 2)

Proof state:
case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ cos (arcsin x) = √(1 - x ^ 2)

Tactic:
rw [not_le] at hx₁

Result:
case neg
x : ℝ
hx₁ : x < -1
⊢ cos (arcsin x) = √(1 - x ^ 2)
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiffOn_all_iff_nat :
    (∀ (n : ℕ∞), ContDiffOn 𝕜 n f s) ↔ ∀ n : ℕ, ContDiffOn 𝕜 n f s

Proof state:
case none
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
H : ∀ (n : ℕ), ContDiffOn 𝕜 (↑n) f s
⊢ ContDiffOn 𝕜 (↑none) f s

case some
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
H : ∀ (n : ℕ), ContDiffOn 𝕜 (↑n) f s
n : ℕ
⊢ ContDiffOn 𝕜 (↑(some n)) f s

Tactic:
exacts [contDiffOn_infty.2 H, H n]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
⊢ (∀ (n : ℕ), ContDiffOn 𝕜 (↑n) f s) → ∀ (n : ℕ∞), ContDiffOn 𝕜 (↑n) f s

Tactic:
rintro H (_ | n)

Result:
case none
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
H : ∀ (n : ℕ), ContDiffOn 𝕜 (↑n) f s
⊢ ContDiffOn 𝕜 (↑none) f s

case some
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
H : ∀ (n : ℕ), ContDiffOn 𝕜 (↑n) f s
n : ℕ
⊢ ContDiffOn 𝕜 (↑(some n)) f s

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
⊢ (∀ (n : ℕ∞), ContDiffOn 𝕜 (↑n) f s) ↔ ∀ (n : ℕ), ContDiffOn 𝕜 (↑n) f s

Tactic:
refine ⟨fun H n => H n, ?_⟩

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
⊢ (∀ (n : ℕ), ContDiffOn 𝕜 (↑n) f s) → ∀ (n : ℕ∞), ContDiffOn 𝕜 (↑n) f s
-- Mathlib/SetTheory/Game/PGame.lean
theorem moveLeft_neg_symm {x : PGame} (i) :
    x.moveLeft (toRightMovesNeg.symm i) = -(-x).moveRight i

Proof state:
x : PGame
i : (-x).RightMoves
⊢ x.moveLeft (toRightMovesNeg.symm i) = -(-x).moveRight i

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/AxGrothendieck.lean
theorem realize_genericPolyMapSurjOnOfInjOn
    [Finite ι] (φ : ring.Formula (α ⊕ ι)) (mons : ι → Finset (ι →₀ ℕ)) :
    (K ⊨ genericPolyMapSurjOnOfInjOn φ mons) ↔
      ∀ (v : α → K) (p : { p : ι → MvPolynomial ι K // (∀ i, (p i).support ⊆ mons i) }),
        let f : (ι → K) → (ι → K) := fun v i => eval v (p.1 i)
        let S : Set (ι → K) := fun x => φ.Realize (Sum.elim v x)
        S.MapsTo f S → S.InjOn f → S.SurjOn f S

Proof state:
ι : Type u_1
α : Type u_2
inst✝³ : Finite α
K : Type u_3
inst✝² : Field K
inst✝¹ : CompatibleRing K
inst✝ : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K), Set.InjOn f S ↔ ∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y

Tactic:
simp [Set.InjOn]

Result:
ι : Type u_1
α : Type u_2
inst✝³ : Finite α
K : Type u_3
inst✝² : Field K
inst✝¹ : CompatibleRing K
inst✝ : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ ∀ {S : Set (ι → K)} (f : (ι → K) → ι → K),
    (∀ ⦃x₁ : ι → K⦄, x₁ ∈ S → ∀ ⦃x₂ : ι → K⦄, x₂ ∈ S → f x₁ = f x₂ → x₁ = x₂) ↔
      ∀ (x y : ι → K), x ∈ S → y ∈ S → f x = f y → x = y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem Sublist.reverse : l₁ <+ l₂ → l₁.reverse <+ l₂.reverse
  | .slnil => Sublist.refl _
  | .cons _ h => by rw [reverse_cons]; exact sublist_append_of_sublist_left h.reverse
  | .cons₂ _ h => by rw [reverse_cons, reverse_cons]; exact h.reverse.append_right _

Proof state:
α✝ : Type u_1
l₁✝ l₂ l₁ l₂✝ : List α✝
a✝ : α✝
h : l₁ <+ l₂✝
⊢ l₁.reverse <+ l₂✝.reverse ++ [a✝]

Tactic:
exact sublist_append_of_sublist_left h.reverse

Result:
no goals

Proof state:
α✝ : Type u_1
l₁ l₂ l₁✝ l₂✝ : List α✝
a✝ : α✝
h : l₁✝ <+ l₂✝
⊢ (a✝ :: l₁✝).reverse <+ (a✝ :: l₂✝).reverse

Tactic:
rw [reverse_cons, reverse_cons]

Result:
α✝ : Type u_1
l₁ l₂ l₁✝ l₂✝ : List α✝
a✝ : α✝
h : l₁✝ <+ l₂✝
⊢ l₁✝.reverse ++ [a✝] <+ l₂✝.reverse ++ [a✝]

Proof state:
α✝ : Type u_1
l₁✝ l₂ l₁ l₂✝ : List α✝
a✝ : α✝
h : l₁ <+ l₂✝
⊢ l₁.reverse <+ (a✝ :: l₂✝).reverse

Tactic:
rw [reverse_cons]

Result:
α✝ : Type u_1
l₁✝ l₂ l₁ l₂✝ : List α✝
a✝ : α✝
h : l₁ <+ l₂✝
⊢ l₁.reverse <+ l₂✝.reverse ++ [a✝]

Proof state:
α✝ : Type u_1
l₁ l₂ l₁✝ l₂✝ : List α✝
a✝ : α✝
h : l₁✝ <+ l₂✝
⊢ l₁✝.reverse ++ [a✝] <+ l₂✝.reverse ++ [a✝]

Tactic:
exact h.reverse.append_right _

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem add_eq_max_of_ne {q r : ℚ_[p]} (h : ‖q‖ ≠ ‖r‖) : ‖q + r‖ = max ‖q‖ ‖r‖

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
h : ¬↑(padicNormE q) = ↑(padicNormE r)
⊢ ↑(padicNormE (q + r)) = ↑(padicNormE q) ⊔ ↑(padicNormE r)

Tactic:
have : padicNormE q ≠ padicNormE r := mod_cast h

Result:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
h : ¬↑(padicNormE q) = ↑(padicNormE r)
this : padicNormE q ≠ padicNormE r
⊢ ↑(padicNormE (q + r)) = ↑(padicNormE q) ⊔ ↑(padicNormE r)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
h : ‖q‖ ≠ ‖r‖
⊢ ‖q + r‖ = ‖q‖ ⊔ ‖r‖

Tactic:
dsimp [norm] at h ⊢

Result:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
h : ¬↑(padicNormE q) = ↑(padicNormE r)
⊢ ↑(padicNormE (q + r)) = ↑(padicNormE q) ⊔ ↑(padicNormE r)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
h : ¬↑(padicNormE q) = ↑(padicNormE r)
this : padicNormE q ≠ padicNormE r
⊢ ↑(padicNormE (q + r)) = ↑(padicNormE q) ⊔ ↑(padicNormE r)

Tactic:
exact mod_cast add_eq_max_of_ne' this

Result:
no goals