harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/NumberField/House.lean
theorem house_le_bound : ∀ l, house (ξ K x l).1 ≤ (c₁ K) *
    ((c₁ K * q * A)^((p : ℝ) / (q - p)))

Proof state:
case calc_3.h
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
p q : ℕ
hpq : p < q
x : β × (K →+* ℂ) → ℤ
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))
h : ℕ := finrank ℚ K
l : β
r : K →+* ℂ
a✝ : r ∈ univ
⊢ ‖x (l, r)‖ * house ((algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) r)) ≤
    ‖x (l, r)‖ * univ.sup' ⋯ fun r => house ((algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) r))

Tactic:
apply mul_le_mul_of_nonneg_left ?_ (norm_nonneg (x (l,r)))

Result:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
p q : ℕ
hpq : p < q
x : β × (K →+* ℂ) → ℤ
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))
h : ℕ := finrank ℚ K
l : β
r : K →+* ℂ
a✝ : r ∈ univ
⊢ house ((algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) r)) ≤
    univ.sup' ⋯ fun r => house ((algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) r))

Proof state:
case calc_5
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
p q : ℕ
hpq : p < q
x : β × (K →+* ℂ) → ℤ
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))
h : ℕ := finrank ℚ K
l : β
⊢ ↑(Fintype.card (K →+* ℂ)) *
      ((↑q * ↑h * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p)) * NumberField.house.supOfBasis K) ≤
    ↑h * NumberField.house.c₂ K * (↑q * NumberField.house.c₁ K * A) ^ (↑p / (↑q - ↑p))

Tactic:
rw [Embeddings.card, mul_comm _ (supOfBasis K), c₂, c₁, ← mul_assoc]

Result:
case calc_5
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
p q : ℕ
hpq : p < q
x : β × (K →+* ℂ) → ℤ
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))
h : ℕ := finrank ℚ K
l : β
⊢ ↑(finrank ℚ K) * NumberField.house.supOfBasis K * (↑q * ↑h * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p)) ≤
    ↑h * ((1 ⊔ NumberField.house.c K) * NumberField.house.supOfBasis K) *
      (↑q * (↑(finrank ℚ K) * NumberField.house.c₂ K) * A) ^ (↑p / (↑q - ↑p))
-- Mathlib/Topology/DiscreteSubset.lean
lemma mem_codiscreteWithin_accPt {S T : Set X} :
    S ∈ codiscreteWithin T ↔ ∀ x ∈ T, ¬AccPt x (𝓟 (T \ S))

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
S T : Set X
⊢ S ∈ codiscreteWithin T ↔ ∀ x ∈ T, ¬AccPt x (𝓟 (T \ S))

Tactic:
simp only [mem_codiscreteWithin, disjoint_iff, AccPt, not_neBot]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
theorem half_mul_log_add_log_abs {r : ℝ} : 2⁻¹ * (log r + |log r|) = log⁺ r

Proof state:
case pos
r : ℝ
hr : 0 ≤ log r
⊢ 2⁻¹ * (log r + |log r|) = log⁺ r

Tactic:
simp [posLog, hr, abs_of_nonneg]

Result:
case pos
r : ℝ
hr : 0 ≤ log r
⊢ 2⁻¹ * (log r + log r) = log r

Proof state:
case pos
r : ℝ
hr : 0 ≤ log r
⊢ 2⁻¹ * (log r + log r) = log r

Tactic:
ring

Result:
no goals

Proof state:
case neg
r : ℝ
hr : ¬0 ≤ log r
⊢ 2⁻¹ * (log r + |log r|) = log⁺ r

Tactic:
simp [posLog, le_of_not_ge hr, abs_of_nonpos]

Result:
no goals

Proof state:
r : ℝ
⊢ 2⁻¹ * (log r + |log r|) = log⁺ r

Tactic:
by_cases hr : 0 ≤ log r

Result:
case pos
r : ℝ
hr : 0 ≤ log r
⊢ 2⁻¹ * (log r + |log r|) = log⁺ r

case neg
r : ℝ
hr : ¬0 ≤ log r
⊢ 2⁻¹ * (log r + |log r|) = log⁺ r
-- Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean
theorem quadraticChar_card_sqrts (hF : ringChar F ≠ 2) (a : F) :
    #{x : F | x ^ 2 = a}.toFinset = quadraticChar F a + 1

Proof state:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := {x | x ^ 2 = a}.toFinset
h : IsSquare a
⊢ ↑(#s) = (quadraticChar F) a + 1

Tactic:
rw [(quadraticChar_one_iff_isSquare h₀).mpr h]

Result:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := {x | x ^ 2 = a}.toFinset
h : IsSquare a
⊢ ↑(#s) = 1 + 1

Proof state:
case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := {x | x ^ 2 = a}.toFinset
h : ¬IsSquare a
⊢ s = ∅

Tactic:
ext1

Result:
case neg.h
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := {x | x ^ 2 = a}.toFinset
h : ¬IsSquare a
a✝ : F
⊢ a✝ ∈ s ↔ a✝ ∈ ∅

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
⊢ ↑(#{x | x ^ 2 = a}.toFinset) = (quadraticChar F) a + 1

Tactic:
by_cases h₀ : a = 0

Result:
case pos
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : a = 0
⊢ ↑(#{x | x ^ 2 = a}.toFinset) = (quadraticChar F) a + 1

case neg
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
⊢ ↑(#{x | x ^ 2 = a}.toFinset) = (quadraticChar F) a + 1

Proof state:
case pos.intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
h₀ : ¬a = 0
s : Finset F := {x | x ^ 2 = a}.toFinset
b : F
h : a = b * b
⊢ ↑(#s) = 1 + 1

Tactic:
rw [h, mul_self_eq_zero] at h₀

Result:
case pos.intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := {x | x ^ 2 = a}.toFinset
b : F
h₀ : ¬b = 0
h : a = b * b
⊢ ↑(#s) = 1 + 1

Proof state:
case h
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := {x | x ^ 2 = a}.toFinset
b : F
h₀ : ¬b = 0
h : a = b ^ 2
a✝ : F
⊢ a✝ ∈ s ↔ a✝ ∈ [b, -b].toFinset

Tactic:
simp only [Set.toFinset_setOf, h, mem_filter, mem_univ, true_and, List.toFinset_cons,
  List.toFinset_nil, insert_emptyc_eq, mem_insert, mem_singleton, s]

Result:
case h
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
s : Finset F := {x | x ^ 2 = a}.toFinset
b : F
h₀ : ¬b = 0
h : a = b ^ 2
a✝ : F
⊢ a✝ ^ 2 = b ^ 2 ↔ a✝ = b ∨ a✝ = -b
-- Mathlib/CategoryTheory/Monoidal/Bimod.lean
theorem pentagon_bimod {V W X Y Z : Mon_ C} (M : Bimod V W) (N : Bimod W X) (P : Bimod X Y)
    (Q : Bimod Y Z) :
    whiskerRight (associatorBimod M N P).hom Q ≫
      (associatorBimod M (N.tensorBimod P) Q).hom ≫
        whiskerLeft M (associatorBimod N P Q).hom =
      (associatorBimod (M.tensorBimod N) P Q).hom ≫
        (associatorBimod M N (P.tensorBimod Q)).hom

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
V W X Y Z : Mon_ C
M : Bimod V W
N : Bimod W X
P : Bimod X Y
Q : Bimod Y Z
⊢ whiskerRight
        (isoOfIso
            { hom := AssociatorBimod.hom M N P, inv := AssociatorBimod.inv M N P, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
            ⋯).hom
        Q ≫
      (isoOfIso
            { hom := AssociatorBimod.hom M (N.tensorBimod P) Q, inv := AssociatorBimod.inv M (N.tensorBimod P) Q,
              hom_inv_id := ⋯, inv_hom_id := ⋯ }
            ⋯ ⋯).hom ≫
        M.whiskerLeft
          (isoOfIso
              { hom := AssociatorBimod.hom N P Q, inv := AssociatorBimod.inv N P Q, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
              ⋯).hom =
    (isoOfIso
          { hom := AssociatorBimod.hom (M.tensorBimod N) P Q, inv := AssociatorBimod.inv (M.tensorBimod N) P Q,
            hom_inv_id := ⋯, inv_hom_id := ⋯ }
          ⋯ ⋯).hom ≫
      (isoOfIso
          { hom := AssociatorBimod.hom M N (P.tensorBimod Q), inv := AssociatorBimod.inv M N (P.tensorBimod Q),
            hom_inv_id := ⋯, inv_hom_id := ⋯ }
          ⋯ ⋯).hom

Tactic:
ext

Result:
case h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
V W X Y Z : Mon_ C
M : Bimod V W
N : Bimod W X
P : Bimod X Y
Q : Bimod Y Z
⊢ (whiskerRight
          (isoOfIso
              { hom := AssociatorBimod.hom M N P, inv := AssociatorBimod.inv M N P, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
              ⋯).hom
          Q ≫
        (isoOfIso
              { hom := AssociatorBimod.hom M (N.tensorBimod P) Q, inv := AssociatorBimod.inv M (N.tensorBimod P) Q,
                hom_inv_id := ⋯, inv_hom_id := ⋯ }
              ⋯ ⋯).hom ≫
          M.whiskerLeft
            (isoOfIso
                { hom := AssociatorBimod.hom N P Q, inv := AssociatorBimod.inv N P Q, hom_inv_id := ⋯, inv_hom_id := ⋯ }
                ⋯ ⋯).hom).hom =
    ((isoOfIso
            { hom := AssociatorBimod.hom (M.tensorBimod N) P Q, inv := AssociatorBimod.inv (M.tensorBimod N) P Q,
              hom_inv_id := ⋯, inv_hom_id := ⋯ }
            ⋯ ⋯).hom ≫
        (isoOfIso
            { hom := AssociatorBimod.hom M N (P.tensorBimod Q), inv := AssociatorBimod.inv M N (P.tensorBimod Q),
              hom_inv_id := ⋯, inv_hom_id := ⋯ }
            ⋯ ⋯).hom).hom
-- Mathlib/CategoryTheory/Monoidal/Bimod.lean
theorem pentagon_bimod {V W X Y Z : Mon_ C} (M : Bimod V W) (N : Bimod W X) (P : Bimod X Y)
    (Q : Bimod Y Z) :
    whiskerRight (associatorBimod M N P).hom Q ≫
      (associatorBimod M (N.tensorBimod P) Q).hom ≫
        whiskerLeft M (associatorBimod N P Q).hom =
      (associatorBimod (M.tensorBimod N) P Q).hom ≫
        (associatorBimod M N (P.tensorBimod Q)).hom

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
V W X Y Z : Mon_ C
M : Bimod V W
N : Bimod W X
P : Bimod X Y
Q : Bimod Y Z
⊢ whiskerRight (M.associatorBimod N P).hom Q ≫
      (M.associatorBimod (N.tensorBimod P) Q).hom ≫ M.whiskerLeft (N.associatorBimod P Q).hom =
    ((M.tensorBimod N).associatorBimod P Q).hom ≫ (M.associatorBimod N (P.tensorBimod Q)).hom

Tactic:
dsimp [associatorBimod]

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
V W X Y Z : Mon_ C
M : Bimod V W
N : Bimod W X
P : Bimod X Y
Q : Bimod Y Z
⊢ whiskerRight
        (isoOfIso
            { hom := AssociatorBimod.hom M N P, inv := AssociatorBimod.inv M N P, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
            ⋯).hom
        Q ≫
      (isoOfIso
            { hom := AssociatorBimod.hom M (N.tensorBimod P) Q, inv := AssociatorBimod.inv M (N.tensorBimod P) Q,
              hom_inv_id := ⋯, inv_hom_id := ⋯ }
            ⋯ ⋯).hom ≫
        M.whiskerLeft
          (isoOfIso
              { hom := AssociatorBimod.hom N P Q, inv := AssociatorBimod.inv N P Q, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
              ⋯).hom =
    (isoOfIso
          { hom := AssociatorBimod.hom (M.tensorBimod N) P Q, inv := AssociatorBimod.inv (M.tensorBimod N) P Q,
            hom_inv_id := ⋯, inv_hom_id := ⋯ }
          ⋯ ⋯).hom ≫
      (isoOfIso
          { hom := AssociatorBimod.hom M N (P.tensorBimod Q), inv := AssociatorBimod.inv M N (P.tensorBimod Q),
            hom_inv_id := ⋯, inv_hom_id := ⋯ }
          ⋯ ⋯).hom
-- Mathlib/Algebra/Polynomial/Derivation.lean
theorem compAEval_eq (d : Derivation R A M) (f : R[X]) :
    d.compAEval a f = derivative f • (AEval.of R M a (d a))

Proof state:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
a : A
d : Derivation R A M
f : R[X]
⊢ (d.compAEval a) f = ((mkDerivation R) ((AEval.of R M a) (d a))) f

Tactic:
congr

Result:
case e_a
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
a : A
d : Derivation R A M
f : R[X]
⊢ d.compAEval a = (mkDerivation R) ((AEval.of R M a) (d a))

Proof state:
case e_a.h
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
a : A
d : Derivation R A M
f : R[X]
⊢ (d.compAEval a) X = ((mkDerivation R) ((AEval.of R M a) (d a))) X

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
a : A
d : Derivation R A M
f : R[X]
⊢ (d.compAEval a) f = derivative f • (AEval.of R M a) (d a)

Tactic:
rw [← mkDerivation_apply]

Result:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
a : A
d : Derivation R A M
f : R[X]
⊢ (d.compAEval a) f = ((mkDerivation R) ((AEval.of R M a) (d a))) f

Proof state:
case e_a
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
a : A
d : Derivation R A M
f : R[X]
⊢ d.compAEval a = (mkDerivation R) ((AEval.of R M a) (d a))

Tactic:
apply derivation_ext

Result:
case e_a.h
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
a : A
d : Derivation R A M
f : R[X]
⊢ (d.compAEval a) X = ((mkDerivation R) ((AEval.of R M a) (d a))) X
-- Mathlib/CategoryTheory/Sites/Sieves.lean
theorem functorPushforward_top (F : C ⥤ D) (X : C) : (⊤ : Sieve X).functorPushforward F = ⊤

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
⊢ generate (functorPushforward F ⊤).arrows = ⊤

Tactic:
apply generate_of_contains_isSplitEpi (𝟙 (F.obj X))

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
⊢ (functorPushforward F ⊤).arrows (𝟙 (F.obj X))

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
⊢ functorPushforward F ⊤ = ⊤

Tactic:
refine (generate_sieve _).symm.trans ?_

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
⊢ generate (functorPushforward F ⊤).arrows = ⊤

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
⊢ 𝟙 (F.obj X) = 𝟙 (F.obj X) ≫ F.map (𝟙 X)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
⊢ (functorPushforward F ⊤).arrows (𝟙 (F.obj X))

Tactic:
exact ⟨X, 𝟙 _, 𝟙 _, trivial, by simp⟩

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem eq_adjoint_iff (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E) :
    A = LinearMap.adjoint B ↔ ∀ x y, ⟪A x, y⟫ = ⟪x, B y⟫

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✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
⊢ A = adjoint B ↔ ∀ (x : E) (y : F), ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜

Tactic:
refine ⟨fun h x y => by rw [h, adjoint_inner_left], fun h => ?_⟩

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✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : ∀ (x : E) (y : F), ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜
⊢ A = adjoint B

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✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : A = adjoint B
x : E
y : F
⊢ ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜

Tactic:
rw [h, adjoint_inner_left]

Result:
no goals

Proof state:
case h
𝕜 : 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✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : ∀ (x : E) (y : F), ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜
x : E
⊢ A x = (adjoint B) x

Tactic:
exact ext_inner_right 𝕜 fun y => by simp only [adjoint_inner_left, h x y]

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✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : ∀ (x : E) (y : F), ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜
x : E
y : F
⊢ ⟪A x, y⟫_𝕜 = ⟪(adjoint B) x, y⟫_𝕜

Tactic:
simp only [adjoint_inner_left, h x y]

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✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : ∀ (x : E) (y : F), ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜
⊢ A = adjoint B

Tactic:
ext x

Result:
case h
𝕜 : 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✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : ∀ (x : E) (y : F), ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜
x : E
⊢ A x = (adjoint B) x
-- Mathlib/Analysis/RCLike/Basic.lean
theorem smul_re (r : ℝ) (z : K) : re (r • z) = r * re z

Proof state:
K : Type u_1
inst✝ : RCLike K
r : ℝ
z : K
⊢ re (r • z) = r * re z

Tactic:
rw [real_smul_eq_coe_mul, re_ofReal_mul]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
@[simp]
lemma map_b₂ : (W.map φ).b₂ = φ W.b₂

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ (W.map φ).b₂ = φ W.b₂

Tactic:
simp only [b₂, map_a₁, map_a₂]

Result:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ φ W.a₁ ^ 2 + 4 * φ W.a₂ = φ (W.a₁ ^ 2 + 4 * W.a₂)

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ φ W.a₁ ^ 2 + 4 * φ W.a₂ = φ (W.a₁ ^ 2 + 4 * W.a₂)

Tactic:
map_simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem and_self_right : (a ∧ b) ∧ b ↔ a ∧ b

Proof state:
a b : Prop
⊢ (a ∧ b) ∧ b ↔ a ∧ b

Tactic:
rw [ propext and_assoc, and_self]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioc_union_Ioc_right : Ioc a b ∪ Ioc a c = Ioc a (max b c)

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ Ioc a b ∪ Ioc a c = Ioc a (b ⊔ c)

Tactic:
rw [Ioc_union_Ioc, min_self] <;> exact (min_le_left _ _).trans (le_max_left _ _)

Result:
no goals
-- Mathlib/GroupTheory/PGroup.lean
theorem to_sup_of_normal_right {H K : Subgroup G} (hH : IsPGroup p H) (hK : IsPGroup p K)
    [K.Normal] : IsPGroup p (H ⊔ K : Subgroup G)

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
hH : IsPGroup p ↥H
hK : IsPGroup p ↥K
inst✝ : K.Normal
⊢ IsPGroup p ↥(H ⊔ K)

Tactic:
rw [← QuotientGroup.ker_mk' K, ← Subgroup.comap_map_eq]

Result:
p : ℕ
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
hH : IsPGroup p ↥H
hK : IsPGroup p ↥K
inst✝ : K.Normal
⊢ IsPGroup p ↥(Subgroup.comap (QuotientGroup.mk' K) (Subgroup.map (QuotientGroup.mk' K) H))

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
hH : IsPGroup p ↥H
hK : IsPGroup p ↥K
inst✝ : K.Normal
⊢ IsPGroup p ↥(Subgroup.comap (QuotientGroup.mk' K) (Subgroup.map (QuotientGroup.mk' K) H))

Tactic:
apply (hH.map (QuotientGroup.mk' K)).comap_of_ker_isPGroup

Result:
case hϕ
p : ℕ
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
hH : IsPGroup p ↥H
hK : IsPGroup p ↥K
inst✝ : K.Normal
⊢ IsPGroup p ↥(QuotientGroup.mk' K).ker

Proof state:
case hϕ
p : ℕ
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
hH : IsPGroup p ↥H
hK : IsPGroup p ↥K
inst✝ : K.Normal
⊢ IsPGroup p ↥(QuotientGroup.mk' K).ker

Tactic:
rwa [QuotientGroup.ker_mk']

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean
theorem parallelPair_pullback_initial {X B : C} (π : X ⟶ B)
    (c : PullbackCone π π) (hc : IsLimit c) :
    (parallelPair (C := (Sieve.ofArrows (fun (_ : Unit) => X) (fun _ => π)).arrows.categoryᵒᵖ)
    (Y := op ((Presieve.categoryMk _ (c.fst ≫ π) ⟨_, c.fst, π, ofArrows.mk (), rfl⟩)))
    (X := op ((Presieve.categoryMk _ π (Sieve.ofArrows_mk _ _ Unit.unit))))
    (Quiver.Hom.op (Over.homMk c.fst))
    (Quiver.Hom.op (Over.homMk c.snd c.condition.symm))).Initial

Proof state:
case h₁.intro.intro.intro.intro.mk
C : Type u_1
inst✝ : Category.{u_4, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z : (Sieve.ofArrows (fun x => X) fun x => π).arrows.category
Y : C
i✝ : Unit
f : (𝟭 C).obj Z.obj.left ⟶ X
hh : f ≫ π = Z.obj.hom
⊢ Nonempty (op ((Sieve.ofArrows (fun x => X) fun x => π).arrows.categoryMk π ⋯) ⟶ op Z)

Tactic:
let X' : (Presieve.ofArrows (fun () ↦ X) (fun () ↦ π)).category :=
  Presieve.categoryMk _ π (ofArrows.mk ())

Result:
case h₁.intro.intro.intro.intro.mk
C : Type u_1
inst✝ : Category.{u_4, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z : (Sieve.ofArrows (fun x => X) fun x => π).arrows.category
Y : C
i✝ : Unit
f : (𝟭 C).obj Z.obj.left ⟶ X
hh : f ≫ π = Z.obj.hom
X' : (ofArrows (fun x => X) fun x =>
    match x with
    | PUnit.unit => π).category :=
  (ofArrows (fun x => X) fun x =>
        match x with
        | PUnit.unit => π).categoryMk
    π ⋯
⊢ Nonempty (op ((Sieve.ofArrows (fun x => X) fun x => π).arrows.categoryMk π ⋯) ⟶ op Z)

Proof state:
case h₁.intro.intro.intro.intro.mk
C : Type u_1
inst✝ : Category.{u_4, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z : (Sieve.ofArrows (fun x => X) fun x => π).arrows.category
Y : C
i✝ : Unit
f : (𝟭 C).obj Z.obj.left ⟶ X
hh : f ≫ π = Z.obj.hom
X' : (ofArrows (fun x => X) fun x =>
    match x with
    | PUnit.unit => π).category :=
  (ofArrows (fun x => X) fun x =>
        match x with
        | PUnit.unit => π).categoryMk
    π ⋯
⊢ Nonempty (op ((Sieve.ofArrows (fun x => X) fun x => π).arrows.categoryMk π ⋯) ⟶ op Z)

Tactic:
let f' : Z.obj.left ⟶ X'.obj.left := f

Result:
case h₁.intro.intro.intro.intro.mk
C : Type u_1
inst✝ : Category.{u_4, u_1} C
X B : C
π : X ⟶ B
c : PullbackCone π π
hc : IsLimit c
Z : (Sieve.ofArrows (fun x => X) fun x => π).arrows.category
Y : C
i✝ : Unit
f : (𝟭 C).obj Z.obj.left ⟶ X
hh : f ≫ π = Z.obj.hom
X' : (ofArrows (fun x => X) fun x =>
    match x with
    | PUnit.unit => π).category :=
  (ofArrows (fun x => X) fun x =>
        match x with
        | PUnit.unit => π).categoryMk
    π ⋯
f' : Z.obj.left ⟶ X'.obj.left := f
⊢ Nonempty (op ((Sieve.ofArrows (fun x => X) fun x => π).arrows.categoryMk π ⋯) ⟶ op Z)