harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Matrix/ConjTranspose.lean
theorem conjTranspose_eq_zero [AddMonoid α] [StarAddMonoid α] {M : Matrix m n α} :
    Mᴴ = 0 ↔ M = 0

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M : Matrix m n α
⊢ Mᴴ = 0 ↔ M = 0

Tactic:
rw [← conjTranspose_inj (A := M), conjTranspose_zero]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem chain_cons {a b : α} {l : List α} : Chain R a (b :: l) ↔ R a b ∧ Chain R b l :=
  ⟨fun p => by cases p with | cons n p => exact ⟨n, p⟩,
   fun ⟨n, p⟩ => p.cons n⟩

Proof state:
α : Type u_1
R : α → α → Prop
a b : α
l : List α
p : Chain R a (b :: l)
⊢ R a b ∧ Chain R b l

Tactic:
cases p with | cons n p => exact ⟨n, p⟩

Result:
no goals

Proof state:
case cons
α : Type u_1
R : α → α → Prop
a b : α
l : List α
n : R a b
p : Chain R b l
⊢ R a b ∧ Chain R b l

Tactic:
exact ⟨n, p⟩

Result:
no goals
-- Mathlib/Topology/Maps/Proper/Basic.lean
theorem isProperMap_iff_isClosedMap_filter {X : Type u} {Y : Type v} [TopologicalSpace X]
    [TopologicalSpace Y] {f : X → Y} :
    IsProperMap f ↔ Continuous f ∧ IsClosedMap
      (Prod.map f id : X × Filter X → Y × Filter X)

Proof state:
case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
⊢ IsProperMap f

Tactic:
rw [isProperMap_iff_ultrafilter]

Result:
case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
⊢ Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
/-- The **spectral mapping theorem** for the continuous functional calculus. -/
lemma cfc_map_spectrum (ha : p a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f : R → R
a : A
ha : autoParam (p a) _auto✝
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
⊢ spectrum R (cfc f a) = f '' spectrum R a

Tactic:
simp [cfc_apply f a, cfcHom_map_spectrum (p := p)]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem exists_circumcenter_eq_of_cospherical {ps : Set P} {n : ℕ} [FiniteDimensional ℝ V]
    (hd : finrank ℝ V = n) (hc : Cospherical ps) :
    ∃ c : P, ∀ sx : Simplex ℝ P n, Set.range sx.points ⊆ ps → sx.circumcenter = c

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ps : Set P
n : ℕ
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ ↥⊤.direction = n
hc : Cospherical ps
this : Nonempty ↥⊤
⊢ ∃ c, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c

Tactic:
refine exists_circumcenter_eq_of_cospherical_subset ?_ hd hc

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ps : Set P
n : ℕ
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ ↥⊤.direction = n
hc : Cospherical ps
this : Nonempty ↥⊤
⊢ ps ⊆ ↑⊤

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ps : Set P
n : ℕ
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
this : Nonempty ↥⊤
⊢ ∃ c, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c

Tactic:
rw [← finrank_top, ← direction_top ℝ V P] at hd

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ps : Set P
n : ℕ
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ ↥⊤.direction = n
hc : Cospherical ps
this : Nonempty ↥⊤
⊢ ∃ c, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ps : Set P
n : ℕ
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
⊢ ∃ c, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c

Tactic:
haveI : Nonempty (⊤ : AffineSubspace ℝ P) := Set.univ.nonempty

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ps : Set P
n : ℕ
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
this : Nonempty ↥⊤
⊢ ∃ c, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ps : Set P
n : ℕ
inst✝ : FiniteDimensional ℝ V
hd : finrank ℝ ↥⊤.direction = n
hc : Cospherical ps
this : Nonempty ↥⊤
⊢ ps ⊆ ↑⊤

Tactic:
exact Set.subset_univ _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem getElem?_drop (L : List α) (i j : Nat) : (L.drop i)[j]? = L[i + j]?

Proof state:
case a
α : Type u_1
L : List α
i j : Nat
a✝ : α
⊢ a✝ ∈ (drop i L)[j]? ↔ a✝ ∈ L[i + j]?

Tactic:
simp only [getElem?_eq_some_iff, getElem_drop, Option.mem_def]

Result:
case a
α : Type u_1
L : List α
i j : Nat
a✝ : α
⊢ (∃ h, L[i + j] = a✝) ↔ ∃ h, L[i + j] = a✝

Proof state:
α : Type u_1
L : List α
i j : Nat
⊢ (drop i L)[j]? = L[i + j]?

Tactic:
ext

Result:
case a
α : Type u_1
L : List α
i j : Nat
a✝ : α
⊢ a✝ ∈ (drop i L)[j]? ↔ a✝ ∈ L[i + j]?

Proof state:
case a.mp
α : Type u_1
L : List α
i j : Nat
a✝ : α
h : j < (drop i L).length
ha : L[i + j] = a✝
⊢ ∃ h, L[i + j] = a✝

Tactic:
exact ⟨_, ha⟩

Result:
no goals

Proof state:
case a.mpr
α : Type u_1
L : List α
i j : Nat
a✝ : α
h : i + j < L.length
ha : L[i + j] = a✝
⊢ j < (drop i L).length

Tactic:
rw [length_drop]

Result:
case a.mpr
α : Type u_1
L : List α
i j : Nat
a✝ : α
h : i + j < L.length
ha : L[i + j] = a✝
⊢ j < L.length - i

Proof state:
case a
α : Type u_1
L : List α
i j : Nat
a✝ : α
⊢ (∃ h, L[i + j] = a✝) ↔ ∃ h, L[i + j] = a✝

Tactic:
constructor <;> intro ⟨h, ha⟩

Result:
case a.mp
α : Type u_1
L : List α
i j : Nat
a✝ : α
h : j < (drop i L).length
ha : L[i + j] = a✝
⊢ ∃ h, L[i + j] = a✝

case a.mpr
α : Type u_1
L : List α
i j : Nat
a✝ : α
h : i + j < L.length
ha : L[i + j] = a✝
⊢ ∃ h, L[i + j] = a✝

Proof state:
case a.mpr
α : Type u_1
L : List α
i j : Nat
a✝ : α
h✝ : i + j < L.length
h : j + i < L.length
ha : L[i + j] = a✝
⊢ j < L.length - i

Tactic:
apply Nat.lt_sub_of_add_lt h

Result:
no goals

Proof state:
case a.mpr
α : Type u_1
L : List α
i j : Nat
a✝ : α
h : i + j < L.length
ha : L[i + j] = a✝
⊢ ∃ h, L[i + j] = a✝

Tactic:
refine ⟨?_, ha⟩

Result:
case a.mpr
α : Type u_1
L : List α
i j : Nat
a✝ : α
h : i + j < L.length
ha : L[i + j] = a✝
⊢ j < (drop i L).length

Proof state:
case a.mpr
α : Type u_1
L : List α
i j : Nat
a✝ : α
h : i + j < L.length
ha : L[i + j] = a✝
⊢ j < L.length - i

Tactic:
rw [Nat.add_comm] at h

Result:
case a.mpr
α : Type u_1
L : List α
i j : Nat
a✝ : α
h✝ : i + j < L.length
h : j + i < L.length
ha : L[i + j] = a✝
⊢ j < L.length - i
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem reverse_inv_prod_mul_prod (L : List (TransvectionStruct n R)) :
    (L.reverse.map (toMatrix ∘ TransvectionStruct.inv)).prod * (L.map toMatrix).prod = 1

Proof state:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (List.map toMatrix L).prod = 1
this :
  (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (t.inv.toMatrix * t.toMatrix) *
      (List.map toMatrix L).prod =
    1
⊢ (List.map (toMatrix ∘ TransvectionStruct.inv) (t :: L).reverse).prod * (List.map toMatrix (t :: L)).prod = 1

Tactic:
simpa [Matrix.mul_assoc]

Result:
no goals

Proof state:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
L : List (TransvectionStruct n R)
⊢ (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (List.map toMatrix L).prod = 1

Tactic:
induction L with
| nil => simp
| cons t L IH =>
  suffices
    (L.reverse.map (toMatrix ∘ TransvectionStruct.inv)).prod * (t.inv.toMatrix * t.toMatrix) *
        (L.map toMatrix).prod = 1
    by simpa [Matrix.mul_assoc]
  simpa [inv_mul] using IH

Result:
no goals

Proof state:
case cons
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (List.map toMatrix L).prod = 1
⊢ (List.map (toMatrix ∘ TransvectionStruct.inv) (t :: L).reverse).prod * (List.map toMatrix (t :: L)).prod = 1

Tactic:
suffices
  (L.reverse.map (toMatrix ∘ TransvectionStruct.inv)).prod * (t.inv.toMatrix * t.toMatrix) *
      (L.map toMatrix).prod = 1
  by simpa [Matrix.mul_assoc]

Result:
case cons
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (List.map toMatrix L).prod = 1
⊢ (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (t.inv.toMatrix * t.toMatrix) *
      (List.map toMatrix L).prod =
    1

Proof state:
case cons
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (List.map toMatrix L).prod = 1
⊢ (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod * (t.inv.toMatrix * t.toMatrix) *
      (List.map toMatrix L).prod =
    1

Tactic:
simpa [inv_mul] using IH

Result:
no goals

Proof state:
case nil
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
⊢ (List.map (toMatrix ∘ TransvectionStruct.inv) [].reverse).prod * (List.map toMatrix []).prod = 1

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean
theorem formula_performRatCheck {n : Nat} (f : DefaultFormula n)
    (hf : f.ratUnits = #[] ∧ f.assignments.size = n) (p : Literal (PosFin n))
    (ratHint : Nat × Array Nat) :
    (performRatCheck f p ratHint).1 = f

Proof state:
case h_2
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHint : Nat × Array Nat
x✝ : Option (DefaultClause n)
heq✝ : f.clauses[ratHint.fst]! = none
⊢ ({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }, false).fst =
    f

Tactic:
rfl

Result:
no goals

Proof state:
case isTrue
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHint : Nat × Array Nat
x✝ : Option (DefaultClause n)
c : DefaultClause n
heq✝ : f.clauses[ratHint.fst]! = some c
h✝ :
  ({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }.insertRatUnits
        (c.delete p).negate).snd =
    true
⊢ (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                  assignments := f.assignments }.insertRatUnits
              (c.delete p).negate).fst.clearRatUnits,
        true).fst =
    f

Tactic:
rw [clear_insertRat f hf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean
theorem formula_performRatCheck {n : Nat} (f : DefaultFormula n)
    (hf : f.ratUnits = #[] ∧ f.assignments.size = n) (p : Literal (PosFin n))
    (ratHint : Nat × Array Nat) :
    (performRatCheck f p ratHint).1 = f

Proof state:
case isFalse
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHint : Nat × Array Nat
x✝ : Option (DefaultClause n)
c : DefaultClause n
heq✝ : f.clauses[ratHint.fst]! = some c
h✝ :
  ¬({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
              assignments := f.assignments }.insertRatUnits
          (c.delete p).negate).snd =
      true
fc : DefaultFormula n := (f.insertRatUnits (c.delete p).negate).fst
fc_assignments_size : fc.assignments.size = n
insertRatUnits_rw :
  (f.insertRatUnits (c.delete p).negate).fst =
    { clauses := (f.insertRatUnits (c.delete p).negate).fst.clauses,
      rupUnits := (f.insertRatUnits (c.delete p).negate).fst.rupUnits,
      ratUnits := (f.insertRatUnits (c.delete p).negate).fst.ratUnits,
      assignments := (f.insertRatUnits (c.delete p).negate).fst.assignments }
⊢ (if
          (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                assignments := f.assignments }.insertRatUnits
                            (c.delete p).negate).fst.performRupCheck
                      ratHint.snd).2.2.snd =
              true ∨
            (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                assignments := f.assignments }.insertRatUnits
                            (c.delete p).negate).fst.performRupCheck
                      ratHint.snd).2.2.fst =
              false then
        (f, false)
      else (f, true)).fst =
    f

Tactic:
split <;> rfl

Result:
no goals
-- Mathlib/Algebra/Tropical/BigOperators.lean
theorem untrop_sum_eq_sInf_image [ConditionallyCompleteLinearOrder R] (s : Finset S)
    (f : S → Tropical (WithTop R)) : untrop (∑ i ∈ s, f i) = sInf (untrop ∘ f '' s)

Proof state:
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
⊢ untrop (∑ i ∈ s, f i) = sInf (untrop ∘ f '' ↑s)

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | h)

Result:
case inl
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
f : S → Tropical (WithTop R)
⊢ untrop (∑ i ∈ ∅, f i) = sInf (untrop ∘ f '' ↑∅)

case inr
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
h : s.Nonempty
⊢ untrop (∑ i ∈ s, f i) = sInf (untrop ∘ f '' ↑s)

Proof state:
case inl
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
f : S → Tropical (WithTop R)
⊢ untrop (∑ i ∈ ∅, f i) = sInf (untrop ∘ f '' ↑∅)

Tactic:
simp only [Set.image_empty, coe_empty, sum_empty, WithTop.sInf_empty, untrop_zero]

Result:
no goals

Proof state:
case inr
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
h : s.Nonempty
⊢ untrop (∑ i ∈ s, f i) = sInf (untrop ∘ f '' ↑s)

Tactic:
rw [← inf'_eq_csInf_image _ h, inf'_eq_inf, Finset.untrop_sum']

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
lemma domDomRestrict_aux {ι} [DecidableEq ι] (P : ι → Prop) [DecidablePred P] {M₁ : ι → Type*}
    [DecidableEq {a // P a}]
    (x : (i : {a // P a}) → M₁ i) (z : (i : {a // ¬ P a}) → M₁ i) (i : {a : ι // P a})
    (c : M₁ i) : (fun j ↦ if h : P j then Function.update x i c ⟨j, h⟩ else z ⟨j, h⟩) =
    Function.update (fun j => if h : P j then x ⟨j, h⟩ else z ⟨j, h⟩) i c

Proof state:
ι : Sort u_2
inst✝² : DecidableEq ι
P : ι → Prop
inst✝¹ : DecidablePred P
M₁ : ι → Type u_1
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
z : (i : { a // ¬P a }) → M₁ ↑i
i : { a // P a }
c : M₁ ↑i
j : ι
h : ¬j = ↑i
h' : P j
he : ⟨j, h'⟩ = i
⊢ False

Tactic:
apply_fun (fun x => x.1) at he

Result:
ι : Sort u_2
inst✝² : DecidableEq ι
P : ι → Prop
inst✝¹ : DecidablePred P
M₁ : ι → Type u_1
inst✝ : DecidableEq { a // P a }
x : (i : { a // P a }) → M₁ ↑i
z : (i : { a // ¬P a }) → M₁ ↑i
i : { a // P a }
c : M₁ ↑i
j : ι
h : ¬j = ↑i
h' : P j
he : ↑⟨j, h'⟩ = ↑i
⊢ False
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem sin_oangle_add_left_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    Real.Angle.sin (o.oangle (x + y) y) = ‖x‖ / ‖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 y x = ↑(π / 2)
⊢ ((-o).oangle y (x + y)).sin = ‖x‖ / ‖x + 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)).sin = ‖x‖ / ‖y + x‖

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)).sin = ‖x‖ / ‖y + x‖

Tactic:
exact (-o).sin_oangle_add_right_of_oangle_eq_pi_div_two h

Result:
no goals

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).sin = ‖x‖ / ‖x + 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)).sin = ‖x‖ / ‖x + y‖
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem iota_val (A : Class) (x : ZFSet) (H : ∀ y, A y ↔ y = x) : iota A = ↑x :=
  ext fun y =>
    ⟨fun ⟨_, ⟨x', rfl, h⟩, yx'⟩ => by rwa [← (H x').1 <| (h x').2 rfl], fun yx =>
      ⟨_, ⟨x, rfl, H⟩, yx⟩⟩

Proof state:
A : Class.{u_1}
x : ZFSet.{u_1}
H : ∀ (y : ZFSet.{u_1}), A y ↔ y = x
y : ZFSet.{u_1}
x✝ : A.iota y
x' : ZFSet.{u_1}
h : {x | ∀ (y : ZFSet.{u_1}), A y ↔ y = x} x'
yx' : y ∈ ↑x'
⊢ ↑x y

Tactic:
rwa [← (H x').1 <| (h x').2 rfl]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma map_polynomialX : (W'.map f).toAffine.polynomialX = W'.polynomialX.map (mapRingHom f)

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
⊢ C (C (map W' f).toAffine.a₁) * Y - C (C 3 * X ^ 2 + C (2 * (map W' f).toAffine.a₂) * X + C (map W' f).toAffine.a₄) =
    Polynomial.map (mapRingHom f) (C (C W'.a₁) * Y - C (C 3 * X ^ 2 + C (2 * W'.a₂) * X + C W'.a₄))

Tactic:
map_simp

Result:
no goals

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
⊢ (map W' f).toAffine.polynomialX = Polynomial.map (mapRingHom f) W'.polynomialX

Tactic:
simp only [polynomialX]

Result:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
⊢ C (C (map W' f).toAffine.a₁) * Y - C (C 3 * X ^ 2 + C (2 * (map W' f).toAffine.a₂) * X + C (map W' f).toAffine.a₄) =
    Polynomial.map (mapRingHom f) (C (C W'.a₁) * Y - C (C 3 * X ^ 2 + C (2 * W'.a₂) * X + C W'.a₄))
-- Mathlib/Algebra/Group/End.lean
theorem subtypePerm_pow (f : Perm α) (n : ℕ) (hf) :
    (f.subtypePerm hf : Perm { x // p x }) ^ n = (f ^ n).subtypePerm (pow_aux hf)

Proof state:
case zero
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p x ↔ p (f x)
⊢ f.subtypePerm hf ^ 0 = (f ^ 0).subtypePerm ⋯

Tactic:
simp

Result:
no goals

Proof state:
case succ
α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p x ↔ p (f x)
n : ℕ
ih : f.subtypePerm hf ^ n = (f ^ n).subtypePerm ⋯
⊢ f.subtypePerm hf ^ (n + 1) = (f ^ (n + 1)).subtypePerm ⋯

Tactic:
simp_rw [pow_succ', ih, subtypePerm_mul]

Result:
no goals

Proof state:
α : Type u_4
p : α → Prop
f : Perm α
n : ℕ
hf : ∀ (x : α), p x ↔ p (f x)
⊢ f.subtypePerm hf ^ n = (f ^ n).subtypePerm ⋯

Tactic:
induction n with
| zero => simp
| succ n ih => simp_rw [pow_succ', ih, subtypePerm_mul]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Polynomial.lean
theorem polynomialFunctions.le_equalizer {A : Type*} [Semiring A] [Algebra R A] (s : Set R)
    (φ ψ : C(s, R) →ₐ[R] A)
    (h : φ (toContinuousMapOnAlgHom s X) = ψ (toContinuousMapOnAlgHom s X)) :
    polynomialFunctions s ≤ AlgHom.equalizer φ ψ

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : TopologicalSpace R
inst✝² : IsTopologicalSemiring R
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set R
φ ψ : C(↑s, R) →ₐ[R] A
h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)
⊢ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X} ≤ AlgHom.equalizer φ ψ

Tactic:
exact φ.adjoin_le_equalizer ψ fun x hx => (Set.mem_singleton_iff.1 hx).symm ▸ h

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : TopologicalSpace R
inst✝² : IsTopologicalSemiring R
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set R
φ ψ : C(↑s, R) →ₐ[R] A
h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)
⊢ polynomialFunctions s ≤ AlgHom.equalizer φ ψ

Tactic:
rw [polynomialFunctions.eq_adjoin_X s]

Result:
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : TopologicalSpace R
inst✝² : IsTopologicalSemiring R
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set R
φ ψ : C(↑s, R) →ₐ[R] A
h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)
⊢ Algebra.adjoin R {(toContinuousMapOnAlgHom s) X} ≤ AlgHom.equalizer φ ψ
-- Mathlib/Algebra/Homology/TotalComplexSymmetry.lean
@[reassoc]
lemma totalFlipIsoX_hom_D₂ (j j' : J) :
    (K.totalFlipIsoX c j).hom ≫ K.D₂ c j j' =
      K.flip.D₁ c j j' ≫ (K.totalFlipIsoX c j').hom

Proof state:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{u_5, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : c₂.Rel i₂ (c₂.next i₂)
⊢ c₂.π c₁ c (c₂.next i₂, i₁) = j'

Tactic:
rw [← ComplexShape.next_π₁ c₁ c h₂ i₁, h₁, c.next_eq' h₀]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem pentagon_inv :
    W ◁ (α_ X Y Z).inv ≫ (α_ W (X ⊗ Y) Z).inv ≫ (α_ W X Y).inv ▷ Z =
      (α_ W X (Y ⊗ Z)).inv ≫ (α_ (W ⊗ X) Y Z).inv :=
  eq_of_inv_eq_inv (by simp)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ inv (W ◁ (α_ X Y Z).inv ≫ (α_ W (X ⊗ Y) Z).inv ≫ (α_ W X Y).inv ▷ Z) =
    inv ((α_ W X (Y ⊗ Z)).inv ≫ (α_ (W ⊗ X) Y Z).inv)

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Coset/Basic.lean
theorem mem_rightCoset_iff (a : α) : x ∈ op a • s ↔ x * a⁻¹ ∈ s :=
  Iff.intro (fun ⟨b, hb, Eq⟩ => by simp [Eq.symm, hb]) fun h => ⟨x * a⁻¹, h, by simp⟩

Proof state:
α : Type u_1
inst✝ : Group α
s : Set α
x a : α
h : x * a⁻¹ ∈ s
⊢ (fun x => op a • x) (x * a⁻¹) = x

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Group α
s : Set α
x a : α
x✝ : x ∈ op a • s
b : α
hb : b ∈ s
Eq : (fun x => op a • x) b = x
⊢ x * a⁻¹ ∈ s

Tactic:
simp [Eq.symm, hb]

Result:
no goals