harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/GradedObject/Braiding.lean
@[reassoc (attr := simp)]
lemma symmetry [SymmetricCategory C] [HasTensor X Y] [HasTensor Y X] :
    (braiding X Y).hom ≫ (braiding Y X).hom = 𝟙 _

Proof state:
I : Type u_1
inst✝⁵ : AddCommMonoid I
C : Type u_2
inst✝⁴ : Category.{u_3, u_2} C
inst✝³ : MonoidalCategory C
X Y : GradedObject I C
inst✝² : SymmetricCategory C
inst✝¹ : X.HasTensor Y
inst✝ : Y.HasTensor X
⊢ (braiding X Y).hom ≫ (braiding Y X).hom = 𝟙 (tensorObj X Y)

Tactic:
dsimp [braiding]

Result:
I : Type u_1
inst✝⁵ : AddCommMonoid I
C : Type u_2
inst✝⁴ : Category.{u_3, u_2} C
inst✝³ : MonoidalCategory C
X Y : GradedObject I C
inst✝² : SymmetricCategory C
inst✝¹ : X.HasTensor Y
inst✝ : Y.HasTensor X
⊢ ((fun k => tensorObjDesc fun i j hij => (β_ (X i) (Y j)).hom ≫ ιTensorObj Y X j i k ⋯) ≫ fun k =>
      tensorObjDesc fun i j hij => (β_ (Y i) (X j)).hom ≫ ιTensorObj X Y j i k ⋯) =
    𝟙 (tensorObj X Y)

Proof state:
I : Type u_1
inst✝⁵ : AddCommMonoid I
C : Type u_2
inst✝⁴ : Category.{u_3, u_2} C
inst✝³ : MonoidalCategory C
X Y : GradedObject I C
inst✝² : SymmetricCategory C
inst✝¹ : X.HasTensor Y
inst✝ : Y.HasTensor X
⊢ ((fun k => tensorObjDesc fun i j hij => (β_ (X i) (Y j)).hom ≫ ιTensorObj Y X j i k ⋯) ≫ fun k =>
      tensorObjDesc fun i j hij => (β_ (Y i) (X j)).hom ≫ ιTensorObj X Y j i k ⋯) =
    𝟙 (tensorObj X Y)

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma rightShift_neg (a n' : ℤ) (hn' : n' + a = n) :
    (-γ).rightShift a n' hn' = -γ.rightShift a n' hn'

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
⊢ (-γ).rightShift a n' hn' = -γ.rightShift a n' hn'

Tactic:
change rightShiftAddEquiv K L n a n' hn' (-γ) = _

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
⊢ (rightShiftAddEquiv K L n a n' hn') (-γ) = -γ.rightShift a n' hn'

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
⊢ (rightShiftAddEquiv K L n a n' hn') (-γ) = -γ.rightShift a n' hn'

Tactic:
apply _root_.map_neg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem reverse_range' (s n : Nat) : reverse (range' s n) = map (s + n - 1 - ·) (range n)

Proof state:
s n : Nat
⊢ (range' s n).reverse = map (fun x => s + n - 1 - x) (range n)

Tactic:
simp [← toList_inj, List.reverse_range']

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/QuasiIso.lean
lemma quasiIso_of_comp_right (φ : S₁ ⟶ S₂) (φ' : S₂ ⟶ S₃)
    [hφ' : QuasiIso φ'] [hφφ' : QuasiIso (φ ≫ φ')] :
    QuasiIso φ

Proof state:
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ' : QuasiIso φ'
hφφ' : QuasiIso (φ ≫ φ')
⊢ QuasiIso φ

Tactic:
rw [quasiIso_iff] at hφ' hφφ' ⊢

Result:
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ' : IsIso (homologyMap φ')
hφφ' : IsIso (homologyMap (φ ≫ φ'))
⊢ IsIso (homologyMap φ)

Proof state:
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ' : IsIso (homologyMap φ')
hφφ' : IsIso (homologyMap φ ≫ homologyMap φ')
⊢ IsIso (homologyMap φ)

Tactic:
exact IsIso.of_isIso_comp_right (homologyMap φ) (homologyMap φ')

Result:
no goals

Proof state:
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ' : IsIso (homologyMap φ')
hφφ' : IsIso (homologyMap (φ ≫ φ'))
⊢ IsIso (homologyMap φ)

Tactic:
rw [homologyMap_comp] at hφφ'

Result:
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ' : IsIso (homologyMap φ')
hφφ' : IsIso (homologyMap φ ≫ homologyMap φ')
⊢ IsIso (homologyMap φ)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem anyM_toArray [Monad m] (p : α → m Bool) (v : Vector α n) :
    v.toArray.anyM p = v.anyM p

Proof state:
case mk
m : Type → Type u_1
α : Type u_2
n : Nat
inst✝ : Monad m
p : α → m Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ Array.anyM p { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray =
    anyM p { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals

Proof state:
m : Type → Type u_1
α : Type u_2
n : Nat
inst✝ : Monad m
p : α → m Bool
v : Vector α n
⊢ Array.anyM p v.toArray = anyM p v

Tactic:
cases v

Result:
case mk
m : Type → Type u_1
α : Type u_2
n : Nat
inst✝ : Monad m
p : α → m Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ Array.anyM p { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray =
    anyM p { toArray := toArray✝, size_toArray := size_toArray✝ }
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem eq_liftOfRightInverse (hf : Function.RightInverse f_inv f) (g : G₁ →* G₃)
    (hg : f.ker ≤ g.ker) (h : G₂ →* G₃) (hh : h.comp f = g) :
    h = f.liftOfRightInverse f_inv hf ⟨g, hg⟩

Proof state:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
h : G₂ →* G₃
hh : h.comp f = g
⊢ h = (f.liftOfRightInverse f_inv hf) ⟨h.comp f, ⋯⟩

Tactic:
exact ((f.liftOfRightInverse f_inv hf).apply_symm_apply _).symm

Result:
no goals

Proof state:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
h : G₂ →* G₃
hh : h.comp f = g
⊢ h = (f.liftOfRightInverse f_inv hf) ⟨g, hg⟩

Tactic:
simp_rw [← hh]

Result:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
h : G₂ →* G₃
hh : h.comp f = g
⊢ h = (f.liftOfRightInverse f_inv hf) ⟨h.comp f, ⋯⟩
-- Mathlib/Topology/Order/UpperLowerSetTopology.lean
protected lemma monotone_iff_continuous [TopologicalSpace α] [TopologicalSpace β]
    [Topology.IsLowerSet α] [Topology.IsLowerSet β] {f : α → β} : Monotone f ↔ Continuous f

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Topology.IsLowerSet α
inst✝ : Topology.IsLowerSet β
f : α → β
⊢ Monotone f ↔ Continuous f

Tactic:
rw [← monotone_dual_iff]

Result:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Topology.IsLowerSet α
inst✝ : Topology.IsLowerSet β
f : α → β
⊢ Monotone (⇑toDual ∘ f ∘ ⇑ofDual) ↔ Continuous f

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Topology.IsLowerSet α
inst✝ : Topology.IsLowerSet β
f : α → β
⊢ Monotone (⇑toDual ∘ f ∘ ⇑ofDual) ↔ Continuous f

Tactic:
exact IsUpperSet.monotone_iff_continuous (α := αᵒᵈ) (β := βᵒᵈ)
  (f := (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ))

Result:
no goals
-- Mathlib/Geometry/Manifold/Algebra/LeftInvariantDerivation.lean
theorem map_zero : X 0 = 0

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
X : LeftInvariantDerivation I G
⊢ X 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
lemma mem_coe_supp_of_adj {v w : V} {H : Subgraph G} {c : ConnectedComponent H.coe}
    (hv : v ∈ (↑) '' (c : Set H.verts)) (hw : w ∈ H.verts)
    (hadj : H.Adj v w) : w ∈ (↑) '' (c : Set H.verts)

Proof state:
case h
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
c : H.coe.ConnectedComponent
hw : w ∈ H.verts
hadj : H.Adj v w
w✝ : ↑H.verts
h : w✝ ∈ ↑c ∧ ↑w✝ = v
⊢ ⟨w, hw⟩ ∈ ↑(H.coe.connectedComponentMk w✝) ∧ ↑⟨w, hw⟩ = w

Tactic:
exact ⟨connectedComponentMk_eq_of_adj <| Subgraph.Adj.coe <| h.2 ▸ hadj.symm, rfl⟩

Result:
no goals

Proof state:
case intro
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
c : H.coe.ConnectedComponent
hw : w ∈ H.verts
hadj : H.Adj v w
w✝ : ↑H.verts
h : w✝ ∈ ↑c ∧ ↑w✝ = v
⊢ w ∈ Subtype.val '' ↑c

Tactic:
use ⟨w, hw⟩

Result:
case h
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
c : H.coe.ConnectedComponent
hw : w ∈ H.verts
hadj : H.Adj v w
w✝ : ↑H.verts
h : w✝ ∈ ↑c ∧ ↑w✝ = v
⊢ ⟨w, hw⟩ ∈ ↑c ∧ ↑⟨w, hw⟩ = w

Proof state:
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
c : H.coe.ConnectedComponent
hv : v ∈ Subtype.val '' ↑c
hw : w ∈ H.verts
hadj : H.Adj v w
⊢ w ∈ Subtype.val '' ↑c

Tactic:
obtain ⟨_, h⟩ := hv

Result:
case intro
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
c : H.coe.ConnectedComponent
hw : w ∈ H.verts
hadj : H.Adj v w
w✝ : ↑H.verts
h : w✝ ∈ ↑c ∧ ↑w✝ = v
⊢ w ∈ Subtype.val '' ↑c

Proof state:
case h
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
c : H.coe.ConnectedComponent
hw : w ∈ H.verts
hadj : H.Adj v w
w✝ : ↑H.verts
h : w✝ ∈ ↑c ∧ ↑w✝ = v
⊢ ⟨w, hw⟩ ∈ ↑c ∧ ↑⟨w, hw⟩ = w

Tactic:
rw [← (mem_supp_iff _ _).mp h.1]

Result:
case h
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
c : H.coe.ConnectedComponent
hw : w ∈ H.verts
hadj : H.Adj v w
w✝ : ↑H.verts
h : w✝ ∈ ↑c ∧ ↑w✝ = v
⊢ ⟨w, hw⟩ ∈ ↑(H.coe.connectedComponentMk w✝) ∧ ↑⟨w, hw⟩ = w
-- Mathlib/Topology/Algebra/ConstMulAction.lean
theorem IsOpen.smul_left {s : Set G} {t : Set α} (ht : IsOpen t) : IsOpen (s • t)

Proof state:
α : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : ContinuousConstSMul G α
s : Set G
t : Set α
ht : IsOpen t
⊢ IsOpen (⋃ a ∈ s, a • t)

Tactic:
exact isOpen_biUnion fun a _ => ht.smul _

Result:
no goals

Proof state:
α : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : ContinuousConstSMul G α
s : Set G
t : Set α
ht : IsOpen t
⊢ IsOpen (s • t)

Tactic:
rw [← iUnion_smul_set]

Result:
α : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : ContinuousConstSMul G α
s : Set G
t : Set α
ht : IsOpen t
⊢ IsOpen (⋃ a ∈ s, a • t)
-- Mathlib/Algebra/Ring/Equiv.lean
theorem map_eq_neg_one_iff {x : R} : f x = -1 ↔ x = -1

Proof state:
R : Type u_4
S : Type u_5
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R ≃+* S
x : R
⊢ f x = -1 ↔ x = -1

Tactic:
rw [← neg_eq_iff_eq_neg, ← neg_eq_iff_eq_neg, ← map_neg, RingEquiv.map_eq_one_iff]

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem Wbtw.trans_right {w x y z : P} (h₁ : Wbtw R w x z) (h₂ : Wbtw R x y z) : Wbtw R w y z

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w x y z : P
h₁ : Wbtw R w x z
h₂ : Wbtw R x y z
⊢ Wbtw R w y z

Tactic:
rw [wbtw_comm] at *

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w x y z : P
h₁ : Wbtw R z x w
h₂ : Wbtw R z y x
⊢ Wbtw R z y w

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w x y z : P
h₁ : Wbtw R z x w
h₂ : Wbtw R z y x
⊢ Wbtw R z y w

Tactic:
exact h₁.trans_left h₂

Result:
no goals
-- Mathlib/Algebra/Group/Semiconj/Defs.lean
theorem semiconjBy_iff_eq [CancelCommMonoid M] {a x y : M} : SemiconjBy a x y ↔ x = y :=
  ⟨fun h => mul_left_cancel (h.trans (mul_comm _ _)), fun h => by rw [h, SemiconjBy, mul_comm]⟩

Proof state:
M : Type u_2
inst✝ : CancelCommMonoid M
a x y : M
h : x = y
⊢ SemiconjBy a x y

Tactic:
rw [h, SemiconjBy, mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem sub_le (n m : Nat) : n - m ≤ n

Proof state:
case zero
n : Nat
⊢ n - 0 ≤ n

Tactic:
exact Nat.le_refl (n - 0)

Result:
no goals

Proof state:
n m : Nat
⊢ n - m ≤ n

Tactic:
induction m with
| zero      => exact Nat.le_refl (n - 0)
| succ m ih => apply Nat.le_trans (pred_le (n - m)) ih

Result:
no goals

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

Tactic:
apply Nat.le_trans (pred_le (n - m)) ih

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
/-- Functional equation for the even Hurwitz zeta function with poles removed. -/
lemma completedHurwitzZetaEven₀_one_sub (a : UnitAddCircle) (s : ℂ) :
    completedHurwitzZetaEven₀ a (1 - s) = completedCosZeta₀ a s

Proof state:
a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaEven₀ a (1 - s) = completedCosZeta₀ a s

Tactic:
rw [completedHurwitzZetaEven₀, completedCosZeta₀, sub_div,
  (by norm_num : (1 / 2 : ℂ) = ↑(1 / 2 : ℝ)),
  (by rfl : (1 / 2 : ℝ) = (hurwitzEvenFEPair a).k),
  (hurwitzEvenFEPair a).functional_equation₀ (s / 2),
  (by rfl : (hurwitzEvenFEPair a).ε = 1),
  one_smul]

Result:
no goals

Proof state:
a : UnitAddCircle
s : ℂ
⊢ 1 / 2 = ↑(1 / 2)

Tactic:
norm_num

Result:
no goals

Proof state:
a : UnitAddCircle
s : ℂ
⊢ (hurwitzEvenFEPair a).ε = 1

Tactic:
rfl

Result:
no goals

Proof state:
a : UnitAddCircle
s : ℂ
⊢ 1 / 2 = (hurwitzEvenFEPair a).k

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma closure_union_congr_right {Y' : Set α} (h : M.closure Y = M.closure Y') :
    M.closure (X ∪ Y) = M.closure (X ∪ Y')

Proof state:
α : Type u_2
M : Matroid α
X Y Y' : Set α
h : M.closure Y = M.closure Y'
⊢ M.closure (X ∪ Y) = M.closure (X ∪ Y')

Tactic:
rw [← M.closure_union_closure_right_eq, h, M.closure_union_closure_right_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem sub_eq_iff_eq_add' {c : Nat} (h : b ≤ a) : a - b = c ↔ a = b + c

Proof state:
b a c : Nat
h : b ≤ a
⊢ a - b = c ↔ a = b + c

Tactic:
rw [Nat.add_comm, Nat.sub_eq_iff_eq_add h]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean
theorem quadraticChar_ne_one (hF : ringChar F ≠ 2) : quadraticChar F ≠ 1

Proof state:
case intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : Fˣ
ha : (quadraticChar F) ↑a = -1
hχ : quadraticChar F = 1
⊢ False

Tactic:
simp only [hχ, one_apply a.isUnit, one_ne_zero, reduceCtorEq] at ha

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
⊢ quadraticChar F ≠ 1

Tactic:
rcases quadraticChar_exists_neg_one' hF with ⟨a, ha⟩

Result:
case intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : Fˣ
ha : (quadraticChar F) ↑a = -1
⊢ quadraticChar F ≠ 1

Proof state:
case intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : Fˣ
ha : (quadraticChar F) ↑a = -1
⊢ quadraticChar F ≠ 1

Tactic:
intro hχ

Result:
case intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : Fˣ
ha : (quadraticChar F) ↑a = -1
hχ : quadraticChar F = 1
⊢ False
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean
lemma toNNReal_add_add_neg_add_neg_eq (f g : C(X, ℝ)₀) :
    ((f + g).toNNReal + (-f).toNNReal + (-g).toNNReal) =
      ((-(f + g)).toNNReal + f.toNNReal + g.toNNReal)

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
f g : C(X, ℝ)₀
⊢ (f + g).toNNReal + (-f).toNNReal + (-g).toNNReal = (-(f + g)).toNNReal + f.toNNReal + g.toNNReal

Tactic:
apply toContinuousMap_injective

Result:
case a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
f g : C(X, ℝ)₀
⊢ ↑((f + g).toNNReal + (-f).toNNReal + (-g).toNNReal) = ↑((-(f + g)).toNNReal + f.toNNReal + g.toNNReal)

Proof state:
case a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Zero X
f g : C(X, ℝ)₀
⊢ ↑((f + g).toNNReal + (-f).toNNReal + (-g).toNNReal) = ↑((-(f + g)).toNNReal + f.toNNReal + g.toNNReal)

Tactic:
simpa only [← toContinuousMapHom_apply, map_add, map_mul, map_neg, toContinuousMapHom_toNNReal]
  using (f : C(X, ℝ)).toNNReal_add_add_neg_add_neg_eq g

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem sign_of_cycleType' (σ : Perm α) :
    sign σ = (σ.cycleType.map fun n => -(-1 : ℤˣ) ^ n).prod

Proof state:
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
⊢ sign σ = (Multiset.map (fun n => -(-1) ^ n) σ.cycleType).prod

Tactic:
simp [hσ.cycleType, hσ.sign]

Result:
no goals

Proof state:
case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : sign σ = (Multiset.map (fun n => -(-1) ^ n) σ.cycleType).prod
hτ : sign τ = (Multiset.map (fun n => -(-1) ^ n) τ.cycleType).prod
⊢ sign (σ * τ) = (Multiset.map (fun n => -(-1) ^ n) (σ * τ).cycleType).prod

Tactic:
simp [hσ, hτ, hd.cycleType]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ sign σ = (Multiset.map (fun n => -(-1) ^ n) σ.cycleType).prod

Tactic:
induction σ using cycle_induction_on with
| base_one => simp
| base_cycles σ hσ => simp [hσ.cycleType, hσ.sign]
| induction_disjoint σ τ hd _ hσ hτ => simp [hσ, hτ, hd.cycleType]

Result:
no goals

Proof state:
case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ sign 1 = (Multiset.map (fun n => -(-1) ^ n) (cycleType 1)).prod

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem le_of_mul_le_mul_left {a b c : Int} (w : a * b ≤ a * c) (h : 0 < a) : b ≤ c

Proof state:
a b c : Int
w✝¹ : a * b ≤ a * c
h : 0 < a
w✝ : 0 ≤ a * (c - b)
w : 0 ≤ a * (c - b) / a
⊢ b ≤ c

Tactic:
rw [Int.mul_ediv_cancel_left _ (Int.ne_of_gt h)] at w

Result:
a b c : Int
w✝¹ : a * b ≤ a * c
h : 0 < a
w✝ : 0 ≤ a * (c - b)
w : 0 ≤ c - b
⊢ b ≤ c

Proof state:
a b c : Int
w : a * b ≤ a * c
h : 0 < a
⊢ b ≤ c

Tactic:
have w := Int.sub_nonneg_of_le w

Result:
a b c : Int
w✝ : a * b ≤ a * c
h : 0 < a
w : 0 ≤ a * c - a * b
⊢ b ≤ c

Proof state:
a b c : Int
w✝ : a * b ≤ a * c
h : 0 < a
w : 0 ≤ a * (c - b)
⊢ b ≤ c

Tactic:
have w := Int.ediv_nonneg w (Int.le_of_lt h)

Result:
a b c : Int
w✝¹ : a * b ≤ a * c
h : 0 < a
w✝ : 0 ≤ a * (c - b)
w : 0 ≤ a * (c - b) / a
⊢ b ≤ c

Proof state:
a b c : Int
w✝ : a * b ≤ a * c
h : 0 < a
w : 0 ≤ a * c - a * b
⊢ b ≤ c

Tactic:
rw [← Int.mul_sub] at w

Result:
a b c : Int
w✝ : a * b ≤ a * c
h : 0 < a
w : 0 ≤ a * (c - b)
⊢ b ≤ c

Proof state:
a b c : Int
w✝¹ : a * b ≤ a * c
h : 0 < a
w✝ : 0 ≤ a * (c - b)
w : 0 ≤ c - b
⊢ b ≤ c

Tactic:
exact Int.le_of_sub_nonneg w

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem inner_smul_rotation_pi_div_two_smul_right (x : V) (r₁ r₂ : ℝ) :
    ⟪r₂ • x, r₁ • o.rotation (π / 2 : ℝ) x⟫ = 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r₁ r₂ : ℝ
⊢ inner (r₂ • x) (r₁ • (o.rotation ↑(π / 2)) x) = 0

Tactic:
rw [real_inner_comm, inner_smul_rotation_pi_div_two_smul_left]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem zpow_neg_mul_zpow_self (n : ℤ) {A : M} (h : IsUnit A.det) : A ^ (-n) * A ^ n = 1

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
n : ℤ
A : M
h : IsUnit A.det
⊢ A ^ (-n) * A ^ n = 1

Tactic:
rw [zpow_neg h, nonsing_inv_mul _ (h.det_zpow _)]

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem LinearMap.associated_det_comp_equiv {N : Type*} [AddCommGroup N] [Module R N]
    (f : N →ₗ[R] M) (e e' : M ≃ₗ[R] N) :
    Associated (LinearMap.det (f ∘ₗ ↑e)) (LinearMap.det (f ∘ₗ ↑e'))

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : N →ₗ[R] M
e e' : M ≃ₗ[R] N
x : M
⊢ (f ∘ₗ ↑e) x = (f ∘ₗ ↑e') ((e ≪≫ₗ e'.symm) x)

Tactic:
simp only [LinearMap.comp_apply, LinearEquiv.coe_coe, LinearEquiv.trans_apply,
  LinearEquiv.apply_symm_apply]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : N →ₗ[R] M
e e' : M ≃ₗ[R] N
⊢ ∀ (x : M), (f ∘ₗ ↑e) x = (f ∘ₗ ↑e') ((e ≪≫ₗ e'.symm) x)

Tactic:
intro x

Result:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : N →ₗ[R] M
e e' : M ≃ₗ[R] N
x : M
⊢ (f ∘ₗ ↑e) x = (f ∘ₗ ↑e') ((e ≪≫ₗ e'.symm) x)

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : N →ₗ[R] M
e e' : M ≃ₗ[R] N
⊢ Associated (LinearMap.det (f ∘ₗ ↑e)) (LinearMap.det (f ∘ₗ ↑e'))

Tactic:
refine LinearMap.associated_det_of_eq_comp (e.trans e'.symm) _ _ ?_

Result:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : N →ₗ[R] M
e e' : M ≃ₗ[R] N
⊢ ∀ (x : M), (f ∘ₗ ↑e) x = (f ∘ₗ ↑e') ((e ≪≫ₗ e'.symm) x)
-- Mathlib/Analysis/RCLike/Basic.lean
theorem div_re (z w : K) : re (z / w) = re z * re w / normSq w + im z * im w / normSq w

Proof state:
K : Type u_1
inst✝ : RCLike K
z w : K
⊢ re (z / w) = re z * re w / normSq w + im z * im w / normSq w

Tactic:
simp only [div_eq_mul_inv, mul_assoc, sub_eq_add_neg, neg_mul, mul_neg, neg_neg, map_neg,
  rclike_simps]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapFinIdx_eq_cons_iff' {l : List α} {b : β} {f : (i : Nat) → α → (h : i < l.length) → β} :
    l.mapFinIdx f = b :: l₂ ↔
      l.head?.pbind (fun x m => (f 0 x (by cases l <;> simp_all))) = some b ∧
        l.tail?.attach.map (fun ⟨t, m⟩ => t.mapFinIdx fun i a h => f (i + 1) a (by cases l <;> simp_all)) = some l₂

Proof state:
α : Type u_1
β : Type u_2
l₂ : List β
l : List α
b : β
f : (i : Nat) → α → i < l.length → β
⊢ l.mapFinIdx f = b :: l₂ ↔
    (l.head?.pbind fun x m => some (f 0 x ⋯)) = some b ∧
      Option.map
          (fun x =>
            match x with
            | ⟨t, m⟩ => t.mapFinIdx fun i a h => f (i + 1) a ⋯)
          l.tail?.attach =
        some l₂

Tactic:
cases l <;> simp

Result:
no goals

Proof state:
α : Type ?u.43795
β : Type ?u.43819
l₂ : List β
l : List α
b : β
f : (i : Nat) → α → i < l.length → β
x✝ : { x // x ∈ l.tail? }
t : List α
m : t ∈ l.tail?
i : Nat
a : α
h : i < t.length
⊢ i + 1 < l.length

Tactic:
cases l <;> simp_all

Result:
no goals

Proof state:
α : Type ?u.43795
β : Type ?u.43819
l₂ : List β
l : List α
b : β
f : (i : Nat) → α → i < l.length → β
x : α
m : x ∈ l.head?
⊢ 0 < l.length

Tactic:
cases l <;> simp_all

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem sum_smul_vsub_eq_weightedVSubOfPoint_sub (w : ι → k) (p₁ p₂ : ι → P) (b : P) :
    (∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i)) =
      s.weightedVSubOfPoint p₁ b w - s.weightedVSubOfPoint p₂ b w

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p₁ p₂ : ι → P
b : P
⊢ ∑ i ∈ s, w i • (p₁ i -ᵥ p₂ i) = (s.weightedVSubOfPoint p₁ b) w - (s.weightedVSubOfPoint p₂ b) w

Tactic:
simp_rw [weightedVSubOfPoint_apply, ← sum_sub_distrib, ← smul_sub, vsub_sub_vsub_cancel_right]

Result:
no goals