harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem toListModel_containsThenInsert [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
    {m : Raw₀ α β} (h : Raw.WFImp m.1) {a : α} {b : β a} :
    Perm (toListModel (m.containsThenInsert a b).2.1.2) (insertEntry a b (toListModel m.1.2))

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ toListModel (m.containsThenInsert a b).snd.val.buckets ~ insertEntry a b (toListModel m.val.buckets)

Tactic:
rw [containsThenInsert_eq_insertₘ]

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ toListModel (m.insertₘ a b).val.buckets ~ insertEntry a b (toListModel m.val.buckets)

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ toListModel (m.insertₘ a b).val.buckets ~ insertEntry a b (toListModel m.val.buckets)

Tactic:
exact toListModel_insertₘ h

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem norm_mkPiAlgebra [NormOneClass A] : ‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ = 1

Proof state:
case inl
𝕜 : Type u
ι : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Fintype ι
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : NormOneClass A
h✝ : IsEmpty ι
⊢ ‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ = 1

Tactic:
simp [norm_mkPiAlgebra_of_empty]

Result:
no goals

Proof state:
𝕜 : Type u
ι : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Fintype ι
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : NormOneClass A
⊢ ‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ = 1

Tactic:
cases isEmpty_or_nonempty ι

Result:
case inl
𝕜 : Type u
ι : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Fintype ι
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : NormOneClass A
h✝ : IsEmpty ι
⊢ ‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ = 1

case inr
𝕜 : Type u
ι : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Fintype ι
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : NormOneClass A
h✝ : Nonempty ι
⊢ ‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ = 1

Proof state:
case inr
𝕜 : Type u
ι : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Fintype ι
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : NormOneClass A
h✝ : Nonempty ι
⊢ ‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ = 1

Tactic:
refine le_antisymm norm_mkPiAlgebra_le ?_

Result:
case inr
𝕜 : Type u
ι : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Fintype ι
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : NormOneClass A
h✝ : Nonempty ι
⊢ 1 ≤ ‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖

Proof state:
case h.e'_3
𝕜 : Type u
ι : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Fintype ι
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : NormOneClass A
h✝ : Nonempty ι
⊢ 1 = ‖(ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) fun x => 1‖ / ∏ i : ι, ‖1‖

Tactic:
simp

Result:
no goals

Proof state:
case inr
𝕜 : Type u
ι : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Fintype ι
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : NormOneClass A
h✝ : Nonempty ι
⊢ 1 ≤ ‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖

Tactic:
convert ratio_le_opNorm (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) fun _ => 1

Result:
case h.e'_3
𝕜 : Type u
ι : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Fintype ι
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : NormOneClass A
h✝ : Nonempty ι
⊢ 1 = ‖(ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) fun x => 1‖ / ∏ i : ι, ‖1‖
-- Mathlib/RingTheory/Ideal/Over.lean
theorem mem_of_liesOver [P.LiesOver p] (x : A) : x ∈ p ↔ algebraMap A B x ∈ P

Proof state:
A : Type u_2
inst✝³ : CommSemiring A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra A B
P : Ideal B
p : Ideal A
inst✝ : P.LiesOver p
x : A
⊢ x ∈ under A P ↔ (algebraMap A B) x ∈ P

Tactic:
rfl

Result:
no goals

Proof state:
A : Type u_2
inst✝³ : CommSemiring A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra A B
P : Ideal B
p : Ideal A
inst✝ : P.LiesOver p
x : A
⊢ x ∈ p ↔ (algebraMap A B) x ∈ P

Tactic:
rw [P.over_def p]

Result:
A : Type u_2
inst✝³ : CommSemiring A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra A B
P : Ideal B
p : Ideal A
inst✝ : P.LiesOver p
x : A
⊢ x ∈ under A P ↔ (algebraMap A B) x ∈ P
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem algEquivOfEq_toAlgHom {p q : K[X]} (hp : p ≠ 0) (h_eq : p = q) :
    (algEquivOfEq hp h_eq).toAlgHom = liftHom p (root q) (by rw [h_eq, aeval_eq, mk_self]) :=
  rfl

Proof state:
K : Type ?u.367425
L : Type ?u.367428
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p q : K[X]
hp : p ≠ 0
h_eq : p = q
⊢ (aeval (root q)) p = 0

Tactic:
rw [h_eq, aeval_eq, mk_self]

Result:
no goals
-- Mathlib/GroupTheory/FixedPointFree.lean
theorem odd_card_of_involutive (hφ : FixedPointFree φ) (h2 : Function.Involutive φ) :
    Odd (Nat.card G)

Proof state:
case intro
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
this : Fintype G
h : 2 ∣ Fintype.card G
g : G
hg : orderOf g = 2
⊢ False

Tactic:
exact hφ.orderOf_ne_two_of_involutive h2 g hg

Result:
no goals

Proof state:
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
this : Fintype G
h : 2 ∣ Fintype.card G
⊢ False

Tactic:
obtain ⟨g, hg⟩ := exists_prime_orderOf_dvd_card 2 h

Result:
case intro
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
this : Fintype G
h : 2 ∣ Fintype.card G
g : G
hg : orderOf g = 2
⊢ False

Proof state:
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
this : Fintype G
h : ¬Odd (Nat.card G)
⊢ False

Tactic:
rw [Nat.not_odd_iff_even, even_iff_two_dvd, Nat.card_eq_fintype_card] at h

Result:
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
this : Fintype G
h : 2 ∣ Fintype.card G
⊢ False

Proof state:
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
this : Fintype G
⊢ Odd (Nat.card G)

Tactic:
by_contra h

Result:
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
this : Fintype G
h : ¬Odd (Nat.card G)
⊢ False

Proof state:
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
⊢ Odd (Nat.card G)

Tactic:
have := Fintype.ofFinite G

Result:
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
h2 : Function.Involutive ⇑φ
this : Fintype G
⊢ Odd (Nat.card G)
-- Mathlib/NumberTheory/GaussSum.lean
/-- If `χ` is a multiplicative character of order `n` on a finite field `F`,
then `g(χ) * g(χ^(n-1)) = χ(-1)*#F` -/
lemma gaussSum_mul_gaussSum_pow_orderOf_sub_one {χ : MulChar R R'} {ψ : AddChar R R'}
    (hχ : χ ≠ 1) (hψ : ψ.IsPrimitive) :
    gaussSum χ ψ * gaussSum (χ ^ (orderOf χ - 1)) ψ = χ (-1) * Fintype.card R

Proof state:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
ψ : AddChar R R'
hχ : χ ≠ 1
hψ : ψ.IsPrimitive
⊢ χ * χ ^ (orderOf χ - 1) = 1

Tactic:
rw [← pow_succ', Nat.sub_one_add_one_eq_of_pos χ.orderOf_pos, pow_orderOf_eq_one]

Result:
no goals

Proof state:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
ψ : AddChar R R'
hχ : χ ≠ 1
hψ : ψ.IsPrimitive
⊢ χ ^ (orderOf χ - 1) = χ⁻¹

Tactic:
refine (inv_eq_of_mul_eq_one_right ?_).symm

Result:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
ψ : AddChar R R'
hχ : χ ≠ 1
hψ : ψ.IsPrimitive
⊢ χ * χ ^ (orderOf χ - 1) = 1

Proof state:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
ψ : AddChar R R'
hχ : χ ≠ 1
hψ : ψ.IsPrimitive
⊢ gaussSum χ ψ * gaussSum (χ ^ (orderOf χ - 1)) ψ = χ (-1) * ↑(Fintype.card R)

Tactic:
have h : χ ^ (orderOf χ - 1) = χ⁻¹ := by
  refine (inv_eq_of_mul_eq_one_right ?_).symm
  rw [← pow_succ', Nat.sub_one_add_one_eq_of_pos χ.orderOf_pos, pow_orderOf_eq_one]

Result:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
ψ : AddChar R R'
hχ : χ ≠ 1
hψ : ψ.IsPrimitive
h : χ ^ (orderOf χ - 1) = χ⁻¹
⊢ gaussSum χ ψ * gaussSum (χ ^ (orderOf χ - 1)) ψ = χ (-1) * ↑(Fintype.card R)

Proof state:
R : Type u
inst✝³ : Field R
inst✝² : Fintype R
R' : Type v
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
χ : MulChar R R'
ψ : AddChar R R'
hχ : χ ≠ 1
hψ : ψ.IsPrimitive
h : χ ^ (orderOf χ - 1) = χ⁻¹
⊢ gaussSum χ ψ * gaussSum (χ ^ (orderOf χ - 1)) ψ = χ (-1) * ↑(Fintype.card R)

Tactic:
rw [h, ← mul_gaussSum_inv_eq_gaussSum χ⁻¹, mul_left_comm, gaussSum_mul_gaussSum_eq_card hχ hψ,
  MulChar.inv_apply', inv_neg_one]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem card_biUnion_lt_iff_forall_of_isRegular {α β : Type u} {s : Set α} {t : ∀ a ∈ s, Set β}
    {c : Cardinal} (hc : c.IsRegular) (hs : #s < c) :
    #(⋃ a ∈ s, t a ‹_›) < c ↔ ∀ a (ha : a ∈ s), # (t a ha) < c

Proof state:
α β : Type u
s : Set α
t : (a : α) → a ∈ s → Set β
c : Cardinal.{u}
hc : c.IsRegular
hs : #↑s < c
⊢ #↑(⋃ a, ⋃ (h : a ∈ s), t a h) < c ↔ ∀ (a : α) (ha : a ∈ s), #↑(t a ha) < c

Tactic:
rw [biUnion_eq_iUnion, card_iUnion_lt_iff_forall_of_isRegular hc hs, SetCoe.forall']

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem gcd_add_mul_left_right (m n k : ℕ) : gcd m (n + m * k) = gcd m n

Proof state:
m n k : ℕ
⊢ m.gcd (n + m * k) = m.gcd n

Tactic:
simp [gcd_rec m (n + m * k), gcd_rec m n]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/List.lean
theorem foldrM_toList [Monad m] [LawfulMonad m] (o : Option β) (a : α) (f : β → α → m α) :
    o.toList.foldrM f a = o.elim (pure a) (fun b => f b a)

Proof state:
m : Type u_1 → Type u_2
β : Type u_3
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
o : Option β
a : α
f : β → α → m α
⊢ List.foldrM f a o.toList = o.elim (pure a) fun b => f b a

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
theorem inseparable_iff_forall_isClosed : (x ~ᵢ y) ↔ ∀ s : Set X, IsClosed s → (x ∈ s ↔ y ∈ s)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ (x ~ᵢ y) ↔ ∀ (s : Set X), IsClosed s → (x ∈ s ↔ y ∈ s)

Tactic:
simp only [inseparable_iff_specializes_and, specializes_iff_forall_closed, ← forall_and, ←
  iff_def]

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem translationNumber_one : τ 1 = 0 :=
  translationNumber_eq_of_tendsto₀ _ <| by simp [tendsto_const_nhds]

Proof state:
⊢ Tendsto (fun n => (⇑1)^[n] 0 / ↑n) atTop (𝓝 0)

Tactic:
simp [tendsto_const_nhds]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem isUpperSet_compl : IsUpperSet sᶜ ↔ IsLowerSet s :=
  ⟨fun h => by
    convert h.compl
    rw [compl_compl], IsLowerSet.compl⟩

Proof state:
α : Type u_1
inst✝ : LE α
s : Set α
h : IsUpperSet sᶜ
⊢ IsLowerSet s

Tactic:
convert h.compl

Result:
case h.e'_3
α : Type u_1
inst✝ : LE α
s : Set α
h : IsUpperSet sᶜ
⊢ s = sᶜᶜ

Proof state:
case h.e'_3
α : Type u_1
inst✝ : LE α
s : Set α
h : IsUpperSet sᶜ
⊢ s = sᶜᶜ

Tactic:
rw [compl_compl]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
theorem map_add {F} [Add β] [FunLike F α β] [AddHomClass F α β]
    (f : F) (a b : WithTop α) :
    (a + b).map f = a.map f + b.map f

Proof state:
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a b : WithTop α
⊢ map (⇑f) (a + b) = map (⇑f) a + map (⇑f) b

Tactic:
induction a

Result:
case top
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
b : WithTop α
⊢ map (⇑f) (⊤ + b) = map ⇑f ⊤ + map (⇑f) b

case coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
b : WithTop α
a✝ : α
⊢ map (⇑f) (↑a✝ + b) = map ⇑f ↑a✝ + map (⇑f) b

Proof state:
case top
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
b : WithTop α
⊢ map (⇑f) (⊤ + b) = map ⇑f ⊤ + map (⇑f) b

Tactic:
exact (top_add _).symm

Result:
no goals

Proof state:
case coe.top
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a✝ : α
⊢ map (⇑f) (↑a✝ + ⊤) = map ⇑f ↑a✝ + map ⇑f ⊤

Tactic:
exact (add_top _).symm

Result:
no goals

Proof state:
case coe.coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a✝¹ a✝ : α
⊢ map (⇑f) (↑a✝¹ + ↑a✝) = map ⇑f ↑a✝¹ + map ⇑f ↑a✝

Tactic:
rw [map_coe, map_coe, ← coe_add, ← coe_add, ← map_add]

Result:
case coe.coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a✝¹ a✝ : α
⊢ map ⇑f ↑(a✝¹ + a✝) = ↑(f (a✝¹ + a✝))

Proof state:
case coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
b : WithTop α
a✝ : α
⊢ map (⇑f) (↑a✝ + b) = map ⇑f ↑a✝ + map (⇑f) b

Tactic:
induction b

Result:
case coe.top
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a✝ : α
⊢ map (⇑f) (↑a✝ + ⊤) = map ⇑f ↑a✝ + map ⇑f ⊤

case coe.coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a✝¹ a✝ : α
⊢ map (⇑f) (↑a✝¹ + ↑a✝) = map ⇑f ↑a✝¹ + map ⇑f ↑a✝

Proof state:
case coe.coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a✝¹ a✝ : α
⊢ map ⇑f ↑(a✝¹ + a✝) = ↑(f (a✝¹ + a✝))

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/CommSq.lean
theorem vert_inv {g : W ≅ Y} {h : X ≅ Z} (p : CommSq f g.hom h.hom i) :
    CommSq i g.inv h.inv f :=
  ⟨by rw [Iso.comp_inv_eq, Category.assoc, Iso.eq_inv_comp, p.w]⟩

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
W X Y Z : C
f : W ⟶ X
i : Y ⟶ Z
g : W ≅ Y
h : X ≅ Z
p : CommSq f g.hom h.hom i
⊢ i ≫ h.inv = g.inv ≫ f

Tactic:
rw [Iso.comp_inv_eq, Category.assoc, Iso.eq_inv_comp, p.w]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem adjoint_conj {T : E →L[𝕜] E} (hT : IsSelfAdjoint T) (S : F →L[𝕜] E) :
    IsSelfAdjoint (ContinuousLinearMap.adjoint S ∘L T ∘L S)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : adjoint T = T
S : F →L[𝕜] E
⊢ ((adjoint S).comp T).comp S = (adjoint S).comp (T.comp S)

Tactic:
exact ContinuousLinearMap.comp_assoc _ _ _

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : adjoint T = T
S : F →L[𝕜] E
⊢ adjoint ((adjoint S).comp (T.comp S)) = (adjoint S).comp (T.comp S)

Tactic:
simp only [hT, adjoint_comp, adjoint_adjoint]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : adjoint T = T
S : F →L[𝕜] E
⊢ ((adjoint S).comp T).comp S = (adjoint S).comp (T.comp S)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : IsSelfAdjoint T
S : F →L[𝕜] E
⊢ IsSelfAdjoint ((adjoint S).comp (T.comp S))

Tactic:
rw [isSelfAdjoint_iff'] at hT ⊢

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : adjoint T = T
S : F →L[𝕜] E
⊢ adjoint ((adjoint S).comp (T.comp S)) = (adjoint S).comp (T.comp S)
-- Mathlib/ModelTheory/Substructures.lean
theorem coe_iInf {ι : Sort*} {S : ι → L.Substructure M} :
    ((⨅ i, S i : L.Substructure M) : Set M) = ⋂ i, (S i : Set M)

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
ι : Sort u_3
S : ι → L.Substructure M
⊢ ↑(⨅ i, S i) = ⋂ i, ↑(S i)

Tactic:
simp only [iInf, coe_sInf, Set.biInter_range]

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem isCompact_iff_ultrafilter_le_nhds' :
    IsCompact s ↔ ∀ f : Ultrafilter X, s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsCompact s ↔ ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x

Tactic:
simp only [isCompact_iff_ultrafilter_le_nhds, le_principal_iff, Ultrafilter.mem_coe]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_pi_div_eight : cos (π / 8) = √(2 + √2) / 2

Proof state:
⊢ cos (π / 2 ^ 3) = √(2 + √2) / 2

Tactic:
simp

Result:
no goals

Proof state:
⊢ cos (π / 8) = cos (π / 2 ^ 3)

Tactic:
congr

Result:
case e_x.e_a

⊢ 8 = 2 ^ 3

Proof state:
⊢ cos (π / 8) = √(2 + √2) / 2

Tactic:
trans cos (π / 2 ^ 3)

Result:
⊢ cos (π / 8) = cos (π / 2 ^ 3)


⊢ cos (π / 2 ^ 3) = √(2 + √2) / 2

Proof state:
case e_x.e_a

⊢ 8 = 2 ^ 3

Tactic:
norm_num

Result:
no goals
-- Mathlib/Data/Finite/Card.lean
theorem card_le_of_injective [Finite β] (f : α → β) (hf : Function.Injective f) :
    Nat.card α ≤ Nat.card β

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
hf : Function.Injective f
⊢ Nat.card α ≤ Nat.card β

Tactic:
haveI := Fintype.ofFinite β

Result:
α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
hf : Function.Injective f
this : Fintype β
⊢ Nat.card α ≤ Nat.card β

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
hf : Function.Injective f
this✝ : Fintype β
this : Fintype α
⊢ Nat.card α ≤ Nat.card β

Tactic:
simpa only [Nat.card_eq_fintype_card] using Fintype.card_le_of_injective f hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
hf : Function.Injective f
this : Fintype β
⊢ Nat.card α ≤ Nat.card β

Tactic:
haveI := Fintype.ofInjective f hf

Result:
α : Type u_1
β : Type u_2
inst✝ : Finite β
f : α → β
hf : Function.Injective f
this✝ : Fintype β
this : Fintype α
⊢ Nat.card α ≤ Nat.card β
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem num_eq_zero_iff {x : RatFunc K} : num x = 0 ↔ x = 0 :=
  ⟨fun h => by rw [← num_div_denom x, h, RingHom.map_zero, zero_div], fun h => h.symm ▸ num_zero⟩

Proof state:
K : Type u
inst✝ : Field K
x : RatFunc K
h : x.num = 0
⊢ x = 0

Tactic:
rw [← num_div_denom x, h, RingHom.map_zero, zero_div]

Result:
no goals
-- Mathlib/Analysis/Convex/Strict.lean
theorem StrictConvex.add_left (hs : StrictConvex 𝕜 s) (z : E) :
    StrictConvex 𝕜 ((fun x => z + x) '' s)

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousAdd E
s : Set E
hs : StrictConvex 𝕜 s
z : E
⊢ StrictConvex 𝕜 ((fun x => z + x) '' s)

Tactic:
simpa only [singleton_add] using (strictConvex_singleton z).add hs

Result:
no goals
-- Mathlib/FieldTheory/SplittingField/IsSplittingField.lean
theorem IntermediateField.isSplittingField_iff :
    p.IsSplittingField K F ↔ p.Splits (algebraMap K F) ∧ F = adjoin K (p.rootSet L)

Proof state:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
this : ?m.53096 → (Algebra.adjoin K (p.rootSet ↥F) = ⊤ ↔ F = adjoin K (p.rootSet L))
⊢ IsSplittingField K (↥F) p ↔ Splits (algebraMap K ↥F) p ∧ F = adjoin K (p.rootSet L)

Tactic:
exact ⟨fun h ↦ ⟨h.1, (this h.1).mp h.2⟩, fun h ↦ ⟨h.1, (this h.1).mpr h.2⟩⟩

Result:
no goals

Proof state:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
⊢ Splits (algebraMap K ↥F) p → (Algebra.adjoin K (p.rootSet ↥F) = ⊤ ↔ F.toSubalgebra = Algebra.adjoin K (p.rootSet L))

Tactic:
refine fun hp ↦ (adjoin_rootSet_eq_range hp F.val).symm.trans ?_

Result:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
hp : Splits (algebraMap K ↥F) p
⊢ Algebra.adjoin K (p.rootSet L) = F.val.range ↔ F.toSubalgebra = Algebra.adjoin K (p.rootSet L)

Proof state:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
⊢ IsSplittingField K (↥F) p ↔ Splits (algebraMap K ↥F) p ∧ F = adjoin K (p.rootSet L)

Tactic:
suffices _ → (Algebra.adjoin K (p.rootSet F) = ⊤ ↔ F = adjoin K (p.rootSet L)) by
  exact ⟨fun h ↦ ⟨h.1, (this h.1).mp h.2⟩, fun h ↦ ⟨h.1, (this h.1).mpr h.2⟩⟩

Result:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
⊢ Splits (algebraMap K ↥F) p → (Algebra.adjoin K (p.rootSet ↥F) = ⊤ ↔ F = adjoin K (p.rootSet L))

Proof state:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
hp : Splits (algebraMap K ↥F) p
⊢ Algebra.adjoin K (p.rootSet L) = F.val.range ↔ F.toSubalgebra = Algebra.adjoin K (p.rootSet L)

Tactic:
rw [← F.range_val, eq_comm]

Result:
no goals

Proof state:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
⊢ Splits (algebraMap K ↥F) p → (Algebra.adjoin K (p.rootSet ↥F) = ⊤ ↔ F = adjoin K (p.rootSet L))

Tactic:
rw [← toSubalgebra_injective.eq_iff,
    adjoin_algebraic_toSubalgebra fun x ↦ isAlgebraic_of_mem_rootSet]

Result:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
⊢ Splits (algebraMap K ↥F) p → (Algebra.adjoin K (p.rootSet ↥F) = ⊤ ↔ F.toSubalgebra = Algebra.adjoin K (p.rootSet L))