harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
theorem tensorLeftHomEquiv_whiskerLeft_comp_evaluation {Y Z : C} [HasLeftDual Z] (f : Y ⟶ ᘁZ) :
    (tensorLeftHomEquiv _ _ _ _) (Z ◁ f ≫ ε_ _ _) = f ≫ (ρ_ _).inv :=
  calc
    _ = 𝟙 _ ⊗≫ (η_ (ᘁZ : C) Z ▷ Y ≫ ((ᘁZ) ⊗ Z) ◁ f) ⊗≫ (ᘁZ) ◁ ε_ (ᘁZ) Z

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Z : C
inst✝ : HasLeftDual Z
f : Y ⟶ ᘁZ
⊢ f ⊗≫ ⊗𝟙.hom = f ≫ (ρ_ ᘁZ).inv

Tactic:
monoidal

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Z : C
inst✝ : HasLeftDual Z
f : Y ⟶ ᘁZ
⊢ 𝟙 Y ⊗≫ (𝟙_ C ◁ f ≫ η_ (ᘁZ) Z ▷ ᘁZ) ⊗≫ ᘁZ ◁ ε_ (ᘁZ) Z = f ⊗≫ η_ (ᘁZ) Z ▷ ᘁZ ⊗≫ ᘁZ ◁ ε_ (ᘁZ) Z

Tactic:
monoidal

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Z : C
inst✝ : HasLeftDual Z
f : Y ⟶ ᘁZ
⊢ 𝟙 Y ⊗≫ (η_ (ᘁZ) Z ▷ Y ≫ (ᘁZ ⊗ Z) ◁ f) ⊗≫ ᘁZ ◁ ε_ (ᘁZ) Z = f ⊗≫ η_ (ᘁZ) Z ▷ ᘁZ ⊗≫ ᘁZ ◁ ε_ (ᘁZ) Z

Tactic:
rw [← whisker_exchange]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Z : C
inst✝ : HasLeftDual Z
f : Y ⟶ ᘁZ
⊢ 𝟙 Y ⊗≫ (𝟙_ C ◁ f ≫ η_ (ᘁZ) Z ▷ ᘁZ) ⊗≫ ᘁZ ◁ ε_ (ᘁZ) Z = f ⊗≫ η_ (ᘁZ) Z ▷ ᘁZ ⊗≫ ᘁZ ◁ ε_ (ᘁZ) Z

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Z : C
inst✝ : HasLeftDual Z
f : Y ⟶ ᘁZ
⊢ (tensorLeftHomEquiv Y (ᘁZ) Z (𝟙_ C)) (Z ◁ f ≫ ε_ (ᘁZ) Z) = 𝟙 Y ⊗≫ (η_ (ᘁZ) Z ▷ Y ≫ (ᘁZ ⊗ Z) ◁ f) ⊗≫ ᘁZ ◁ ε_ (ᘁZ) Z

Tactic:
dsimp [tensorLeftHomEquiv]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Z : C
inst✝ : HasLeftDual Z
f : Y ⟶ ᘁZ
⊢ (λ_ Y).inv ≫ η_ (ᘁZ) Z ▷ Y ≫ (α_ (ᘁZ) Z Y).hom ≫ ᘁZ ◁ (Z ◁ f ≫ ε_ (ᘁZ) Z) =
    𝟙 Y ⊗≫ (η_ (ᘁZ) Z ▷ Y ≫ (ᘁZ ⊗ Z) ◁ f) ⊗≫ ᘁZ ◁ ε_ (ᘁZ) Z

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Z : C
inst✝ : HasLeftDual Z
f : Y ⟶ ᘁZ
⊢ f ⊗≫ η_ (ᘁZ) Z ▷ ᘁZ ⊗≫ ᘁZ ◁ ε_ (ᘁZ) Z = f ≫ (ρ_ ᘁZ).inv

Tactic:
rw [evaluation_coevaluation'']

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Z : C
inst✝ : HasLeftDual Z
f : Y ⟶ ᘁZ
⊢ f ⊗≫ ⊗𝟙.hom = f ≫ (ρ_ ᘁZ).inv

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Z : C
inst✝ : HasLeftDual Z
f : Y ⟶ ᘁZ
⊢ (λ_ Y).inv ≫ η_ (ᘁZ) Z ▷ Y ≫ (α_ (ᘁZ) Z Y).hom ≫ ᘁZ ◁ (Z ◁ f ≫ ε_ (ᘁZ) Z) =
    𝟙 Y ⊗≫ (η_ (ᘁZ) Z ▷ Y ≫ (ᘁZ ⊗ Z) ◁ f) ⊗≫ ᘁZ ◁ ε_ (ᘁZ) Z

Tactic:
monoidal

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_alter (h : m.1.WF) {k k' : α} {f : Option β → Option β} :
    Const.get? (Const.alter m k f) k' =
      if k == k' then
        f (Const.get? m k)
      else
        Const.get? m k'

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

Tactic:
simp_to_model [Const.alter] using List.Const.getValue?_alterKey

Result:
no goals
-- Mathlib/Algebra/Polynomial/Cardinal.lean
theorem cardinalMk_le_max {R : Type u} [Semiring R] : #(R[X]) ≤ max #R ℵ₀

Proof state:
case inr
R : Type u
inst✝ : Semiring R
h✝ : Nontrivial R
⊢ #R[X] ≤ #R ⊔ ℵ₀

Tactic:
exact cardinalMk_eq_max.le

Result:
no goals

Proof state:
case inl
R : Type u
inst✝ : Semiring R
h✝ : Subsingleton R
⊢ #R[X] ≤ #R ⊔ ℵ₀

Tactic:
exact (mk_eq_one _).trans_le (le_max_of_le_right one_le_aleph0)

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
⊢ #R[X] ≤ #R ⊔ ℵ₀

Tactic:
cases subsingleton_or_nontrivial R

Result:
case inl
R : Type u
inst✝ : Semiring R
h✝ : Subsingleton R
⊢ #R[X] ≤ #R ⊔ ℵ₀

case inr
R : Type u
inst✝ : Semiring R
h✝ : Nontrivial R
⊢ #R[X] ≤ #R ⊔ ℵ₀
-- Mathlib/Algebra/Order/Chebyshev.lean
theorem AntivaryOn.card_mul_sum_le_sum_mul_sum (hfg : AntivaryOn f g s) :
    (#s : α) * ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : ExistsAddOfLE α
s : Finset ι
f g : ι → α
hfg : AntivaryOn f g ↑s
⊢ #s • ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i

Tactic:
exact hfg.card_smul_sum_le_sum_smul_sum

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : ExistsAddOfLE α
s : Finset ι
f g : ι → α
hfg : AntivaryOn f g ↑s
⊢ ↑(#s) * ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i

Tactic:
rw [← nsmul_eq_mul]

Result:
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : ExistsAddOfLE α
s : Finset ι
f g : ι → α
hfg : AntivaryOn f g ↑s
⊢ #s • ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i
-- Mathlib/MeasureTheory/Measure/MutuallySingular.lean
lemma _root_.MeasurableEmbedding.mutuallySingular_map {β : Type*} {_ : MeasurableSpace β}
    {f : α → β} (hf : MeasurableEmbedding f) (hμν : μ ⟂ₘ ν) :
    μ.map f ⟂ₘ ν.map f

Proof state:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
β : Type u_2
x✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ⟂ₘ ν
⊢ (map f μ) (f '' hμν.nullSet) = 0

Tactic:
rw [hf.map_apply, hf.injective.preimage_image, hμν.measure_nullSet]

Result:
no goals

Proof state:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
β : Type u_2
x✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ⟂ₘ ν
⊢ (map f ν) (f '' hμν.nullSet)ᶜ = 0

Tactic:
rw [hf.map_apply, Set.preimage_compl, hf.injective.preimage_image, hμν.measure_compl_nullSet]

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
β : Type u_2
x✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ⟂ₘ ν
⊢ map f μ ⟂ₘ map f ν

Tactic:
refine ⟨f '' hμν.nullSet, hf.measurableSet_image' hμν.measurableSet_nullSet, ?_, ?_⟩

Result:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
β : Type u_2
x✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ⟂ₘ ν
⊢ (map f μ) (f '' hμν.nullSet) = 0

case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
β : Type u_2
x✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ⟂ₘ ν
⊢ (map f ν) (f '' hμν.nullSet)ᶜ = 0
-- Mathlib/LinearAlgebra/StdBasis.lean
theorem basis_repr_single [DecidableEq η] (s : ∀ j, Basis (ιs j) R (Ms j)) (j i) :
    (Pi.basis s).repr (Pi.single j (s j i)) = Finsupp.single ⟨j, i⟩ 1

Proof state:
case pos
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i i' : ιs j
⊢ ((Pi.basis s).repr (single j ((s j) i))) ⟨j, i'⟩ = (Finsupp.single ⟨j, i⟩ 1) ⟨j, i'⟩

Tactic:
simp only [Pi.basis, LinearEquiv.trans_apply, Basis.repr_self, Pi.single_eq_same,
  LinearEquiv.piCongrRight, Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply,
  Basis.repr_symm_apply, LinearEquiv.coe_mk, ne_eq, Sigma.mk.inj_iff, heq_eq_eq, true_and]

Result:
case pos
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i i' : ιs j
⊢ (Finsupp.single i 1) i' = (Finsupp.single ⟨j, i⟩ 1) ⟨j, i'⟩
-- Mathlib/Topology/Order/LeftRightLim.lean
theorem leftLim_le (h : x ≤ y) : leftLim f x ≤ f y

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this : TopologicalSpace α := Preorder.topology α
⊢ leftLim f x ≤ f y

Tactic:
haveI : OrderTopology α := ⟨rfl⟩

Result:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ leftLim f x ≤ f y
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem algebraMap_eval_T [Algebra R R'] (x : R) (n : ℤ) :
    algebraMap R R' ((T R n).eval x) = (T R' n).eval (algebraMap R R' x)

Proof state:
R : Type u_1
R' : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing R'
inst✝ : Algebra R R'
x : R
n : ℤ
⊢ (algebraMap R R') (eval x (T R n)) = eval ((algebraMap R R') x) (T R' n)

Tactic:
rw [← aeval_algebraMap_apply_eq_algebraMap_eval, aeval_T]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem?_eq_none_iff {a : Vector α n} : a[i]? = none ↔ n ≤ i

Proof state:
α : Type u_1
n i : Nat
a : Vector α n
⊢ a[i]? = none ↔ n ≤ i

Tactic:
by_cases h : i < n

Result:
case pos
α : Type u_1
n i : Nat
a : Vector α n
h : i < n
⊢ a[i]? = none ↔ n ≤ i

case neg
α : Type u_1
n i : Nat
a : Vector α n
h : ¬i < n
⊢ a[i]? = none ↔ n ≤ i

Proof state:
case pos
α : Type u_1
n i : Nat
a : Vector α n
h : i < n
⊢ a[i]? = none ↔ n ≤ i

Tactic:
simp [getElem?_pos, h]

Result:
no goals

Proof state:
case neg
α : Type u_1
n i : Nat
a : Vector α n
h : ¬i < n
⊢ a[i]? = none ↔ n ≤ i

Tactic:
rw [getElem?_neg a i h]

Result:
case neg
α : Type u_1
n i : Nat
a : Vector α n
h : ¬i < n
⊢ none = none ↔ n ≤ i

Proof state:
case neg
α : Type u_1
n i : Nat
a : Vector α n
h : ¬i < n
⊢ none = none ↔ n ≤ i

Tactic:
simp_all

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem angle_add_angle_eq_pi_of_angle_eq_pi {x y : V} (z : V) (h : angle x y = π) :
    angle x z + angle y z = π

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
h : angle x y = π
⊢ angle x z + angle y z = π

Tactic:
rcases angle_eq_pi_iff.1 h with ⟨_, ⟨r, ⟨hr, rfl⟩⟩⟩

Result:
case intro.intro.intro
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x z : V
left✝ : x ≠ 0
r : ℝ
hr : r < 0
h : angle x (r • x) = π
⊢ angle x z + angle (r • x) z = π

Proof state:
case intro.intro.intro
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x z : V
left✝ : x ≠ 0
r : ℝ
hr : r < 0
h : angle x (r • x) = π
⊢ angle x z + angle (r • x) z = π

Tactic:
rw [angle_smul_left_of_neg x z hr, angle_neg_left, add_sub_cancel]

Result:
no goals
-- Mathlib/GroupTheory/CosetCover.lean
theorem Subspace.exists_eq_top_of_iUnion_eq_univ {ι} [Finite ι] {p : ι → Subspace k E}
    (hcovers : ⋃ i, (p i : Set E) = Set.univ) : ∃ i, p i = ⊤

Proof state:
k : Type u_1
E : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : Infinite k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
ι : Sort u_3
inst✝ : Finite ι
p : ι → Subspace k E
hcovers : ⋃ i, ↑(p i) = Set.univ
⊢ ∃ i, p i = ⊤

Tactic:
have := Fintype.ofFinite (Set.range p)

Result:
k : Type u_1
E : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : Infinite k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
ι : Sort u_3
inst✝ : Finite ι
p : ι → Subspace k E
hcovers : ⋃ i, ↑(p i) = Set.univ
this : Fintype ↑(Set.range p)
⊢ ∃ i, p i = ⊤

Proof state:
k : Type u_1
E : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : Infinite k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
ι : Sort u_3
inst✝ : Finite ι
p : ι → Subspace k E
this : Fintype ↑(Set.range p)
hcovers : ⋃ x ∈ (Set.range p).toFinset, ↑x = Set.univ
⊢ ∃ i, p i = ⊤

Tactic:
apply Set.mem_toFinset.mp (Subspace.top_mem_of_biUnion_eq_univ hcovers)

Result:
no goals

Proof state:
k : Type u_1
E : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : Infinite k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
ι : Sort u_3
inst✝ : Finite ι
p : ι → Subspace k E
hcovers : ⋃ i, ↑(p i) = Set.univ
this : Fintype ↑(Set.range p)
⊢ ∃ i, p i = ⊤

Tactic:
simp_rw [← Set.biUnion_range (f := p), ← Set.mem_toFinset] at hcovers

Result:
k : Type u_1
E : Type u_2
inst✝⁴ : DivisionRing k
inst✝³ : Infinite k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
ι : Sort u_3
inst✝ : Finite ι
p : ι → Subspace k E
this : Fintype ↑(Set.range p)
hcovers : ⋃ x ∈ (Set.range p).toFinset, ↑x = Set.univ
⊢ ∃ i, p i = ⊤
-- Mathlib/Algebra/MonoidAlgebra/Basic.lean
@[simp]
lemma mapDomainAlgHom_comp (k A) {G₁ G₂ G₃} [CommSemiring k] [Semiring A] [Algebra k A]
    [AddMonoid G₁] [AddMonoid G₂] [AddMonoid G₃] (f : G₁ →+ G₂) (g : G₂ →+ G₃) :
    mapDomainAlgHom k A (g.comp f) = (mapDomainAlgHom k A g).comp (mapDomainAlgHom k A f)

Proof state:
k : Type u_3
A : Type u_4
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝⁵ : CommSemiring k
inst✝⁴ : Semiring A
inst✝³ : Algebra k A
inst✝² : AddMonoid G₁
inst✝¹ : AddMonoid G₂
inst✝ : AddMonoid G₃
f : G₁ →+ G₂
g : G₂ →+ G₃
⊢ mapDomainAlgHom k A (g.comp f) = (mapDomainAlgHom k A g).comp (mapDomainAlgHom k A f)

Tactic:
ext

Result:
case H.H
k : Type u_3
A : Type u_4
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝⁵ : CommSemiring k
inst✝⁴ : Semiring A
inst✝³ : Algebra k A
inst✝² : AddMonoid G₁
inst✝¹ : AddMonoid G₂
inst✝ : AddMonoid G₃
f : G₁ →+ G₂
g : G₂ →+ G₃
x✝¹ : A[G₁]
x✝ : G₃
⊢ ((mapDomainAlgHom k A (g.comp f)) x✝¹) x✝ = (((mapDomainAlgHom k A g).comp (mapDomainAlgHom k A f)) x✝¹) x✝

Proof state:
case H.H
k : Type u_3
A : Type u_4
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝⁵ : CommSemiring k
inst✝⁴ : Semiring A
inst✝³ : Algebra k A
inst✝² : AddMonoid G₁
inst✝¹ : AddMonoid G₂
inst✝ : AddMonoid G₃
f : G₁ →+ G₂
g : G₂ →+ G₃
x✝¹ : A[G₁]
x✝ : G₃
⊢ ((mapDomainAlgHom k A (g.comp f)) x✝¹) x✝ = (((mapDomainAlgHom k A g).comp (mapDomainAlgHom k A f)) x✝¹) x✝

Tactic:
simp [mapDomain_comp]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Kan/Adjunction.lean
theorem isLeftAdjoint_TFAE (f : a ⟶ b) :
    List.TFAE [
      IsLeftAdjoint f,
      HasAbsLeftKanExtension f (𝟙 a),
      ∃ _ : HasLeftKanExtension f (𝟙 a), Lan.CommuteWith f (𝟙 a) f]

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f : a ⟶ b
⊢ [IsLeftAdjoint f, HasAbsLeftKanExtension f (𝟙 a), ∃ (x : HasLeftKanExtension f (𝟙 a)), Lan.CommuteWith f (𝟙 a) f].TFAE

Tactic:
tfae_have 1 → 2
| h => IsAbsKan.hasAbsLeftKanExtension (Adjunction.ofIsLeftAdjoint f).isAbsoluteLeftKan

Result:
B : Type u
inst✝ : Bicategory B
a b : B
f : a ⟶ b
tfae_1_to_2 : IsLeftAdjoint f → HasAbsLeftKanExtension f (𝟙 a)
⊢ [IsLeftAdjoint f, HasAbsLeftKanExtension f (𝟙 a), ∃ (x : HasLeftKanExtension f (𝟙 a)), Lan.CommuteWith f (𝟙 a) f].TFAE

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f : a ⟶ b
tfae_1_to_2 : IsLeftAdjoint f → HasAbsLeftKanExtension f (𝟙 a)
tfae_2_to_3 : HasAbsLeftKanExtension f (𝟙 a) → ∃ (x : HasLeftKanExtension f (𝟙 a)), Lan.CommuteWith f (𝟙 a) f
tfae_3_to_1 : (∃ (x : HasLeftKanExtension f (𝟙 a)), Lan.CommuteWith f (𝟙 a) f) → IsLeftAdjoint f
⊢ [IsLeftAdjoint f, HasAbsLeftKanExtension f (𝟙 a), ∃ (x : HasLeftKanExtension f (𝟙 a)), Lan.CommuteWith f (𝟙 a) f].TFAE

Tactic:
tfae_finish

Result:
no goals

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f : a ⟶ b
tfae_1_to_2 : IsLeftAdjoint f → HasAbsLeftKanExtension f (𝟙 a)
⊢ [IsLeftAdjoint f, HasAbsLeftKanExtension f (𝟙 a), ∃ (x : HasLeftKanExtension f (𝟙 a)), Lan.CommuteWith f (𝟙 a) f].TFAE

Tactic:
tfae_have 2 → 3
| h => ⟨inferInstance, inferInstance⟩

Result:
B : Type u
inst✝ : Bicategory B
a b : B
f : a ⟶ b
tfae_1_to_2 : IsLeftAdjoint f → HasAbsLeftKanExtension f (𝟙 a)
tfae_2_to_3 : HasAbsLeftKanExtension f (𝟙 a) → ∃ (x : HasLeftKanExtension f (𝟙 a)), Lan.CommuteWith f (𝟙 a) f
⊢ [IsLeftAdjoint f, HasAbsLeftKanExtension f (𝟙 a), ∃ (x : HasLeftKanExtension f (𝟙 a)), Lan.CommuteWith f (𝟙 a) f].TFAE

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f : a ⟶ b
tfae_1_to_2 : IsLeftAdjoint f → HasAbsLeftKanExtension f (𝟙 a)
tfae_2_to_3 : HasAbsLeftKanExtension f (𝟙 a) → ∃ (x : HasLeftKanExtension f (𝟙 a)), Lan.CommuteWith f (𝟙 a) f
⊢ [IsLeftAdjoint f, HasAbsLeftKanExtension f (𝟙 a), ∃ (x : HasLeftKanExtension f (𝟙 a)), Lan.CommuteWith f (𝟙 a) f].TFAE

Tactic:
tfae_have 3 → 1
| ⟨h, h'⟩ => .mk <| (lanIsKan f (𝟙 a)).adjunction <| Lan.CommuteWith.isKan f (𝟙 a) f

Result:
B : Type u
inst✝ : Bicategory B
a b : B
f : a ⟶ b
tfae_1_to_2 : IsLeftAdjoint f → HasAbsLeftKanExtension f (𝟙 a)
tfae_2_to_3 : HasAbsLeftKanExtension f (𝟙 a) → ∃ (x : HasLeftKanExtension f (𝟙 a)), Lan.CommuteWith f (𝟙 a) f
tfae_3_to_1 : (∃ (x : HasLeftKanExtension f (𝟙 a)), Lan.CommuteWith f (𝟙 a) f) → IsLeftAdjoint f
⊢ [IsLeftAdjoint f, HasAbsLeftKanExtension f (𝟙 a), ∃ (x : HasLeftKanExtension f (𝟙 a)), Lan.CommuteWith f (𝟙 a) f].TFAE
-- Mathlib/Data/Finset/Pairwise.lean
theorem pairwise_of_coe_toFinset_pairwise (hl : (l.toFinset : Set α).Pairwise r) (hn : l.Nodup) :
    l.Pairwise r

Proof state:
α : Type u_1
inst✝ : DecidableEq α
r : α → α → Prop
l : List α
hl : (↑l.toFinset).Pairwise r
hn : l.Nodup
⊢ Pairwise r l

Tactic:
rw [coe_toFinset] at hl

Result:
α : Type u_1
inst✝ : DecidableEq α
r : α → α → Prop
l : List α
hl : {a | a ∈ l}.Pairwise r
hn : l.Nodup
⊢ Pairwise r l

Proof state:
α : Type u_1
inst✝ : DecidableEq α
r : α → α → Prop
l : List α
hl : {a | a ∈ l}.Pairwise r
hn : l.Nodup
⊢ Pairwise r l

Tactic:
exact hn.pairwise_of_set_pairwise hl

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/Free.lean
@[simp]
lemma toMatrix_baseChange (f : M₁ →ₗ[R] M₂) (b₁ : Basis ι R M₁) (b₂ : Basis ι₂ R M₂) :
    toMatrix (basis A b₁) (basis A b₂) (f.baseChange A) =
    (toMatrix b₁ b₂ f).map (algebraMap R A)

Proof state:
case a
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι : Type u_4
ι₂ : Type u_5
A : Type u_6
inst✝⁹ : Fintype ι
inst✝⁸ : Finite ι₂
inst✝⁷ : DecidableEq ι
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
b₁ : Basis ι R M₁
b₂ : Basis ι₂ R M₂
i✝ : ι₂
j✝ : ι
⊢ (toMatrix (basis A b₁) (basis A b₂)) (baseChange A f) i✝ j✝ = ((toMatrix b₁ b₂) f).map (⇑(algebraMap R A)) i✝ j✝

Tactic:
simp [toMatrix_apply]

Result:
no goals

Proof state:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι : Type u_4
ι₂ : Type u_5
A : Type u_6
inst✝⁹ : Fintype ι
inst✝⁸ : Finite ι₂
inst✝⁷ : DecidableEq ι
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
b₁ : Basis ι R M₁
b₂ : Basis ι₂ R M₂
⊢ (toMatrix (basis A b₁) (basis A b₂)) (baseChange A f) = ((toMatrix b₁ b₂) f).map ⇑(algebraMap R A)

Tactic:
ext

Result:
case a
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι : Type u_4
ι₂ : Type u_5
A : Type u_6
inst✝⁹ : Fintype ι
inst✝⁸ : Finite ι₂
inst✝⁷ : DecidableEq ι
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
b₁ : Basis ι R M₁
b₂ : Basis ι₂ R M₂
i✝ : ι₂
j✝ : ι
⊢ (toMatrix (basis A b₁) (basis A b₂)) (baseChange A f) i✝ j✝ = ((toMatrix b₁ b₂) f).map (⇑(algebraMap R A)) i✝ j✝
-- Mathlib/Algebra/Exact.lean
lemma surjective_range_liftQ (h : range f ≤ ker g) (hg : Function.Surjective g) :
    Function.Surjective ((range f).liftQ g h)

Proof state:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : range f ≤ ker g
hg : Function.Surjective ⇑g
x₃ : P
⊢ ∃ a, ((range f).liftQ g h) a = x₃

Tactic:
obtain ⟨x₂, rfl⟩ := hg x₃

Result:
case intro
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : range f ≤ ker g
hg : Function.Surjective ⇑g
x₂ : N
⊢ ∃ a, ((range f).liftQ g h) a = g x₂

Proof state:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : range f ≤ ker g
hg : Function.Surjective ⇑g
⊢ Function.Surjective ⇑((range f).liftQ g h)

Tactic:
intro x₃

Result:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : range f ≤ ker g
hg : Function.Surjective ⇑g
x₃ : P
⊢ ∃ a, ((range f).liftQ g h) a = x₃

Proof state:
case intro
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : range f ≤ ker g
hg : Function.Surjective ⇑g
x₂ : N
⊢ ∃ a, ((range f).liftQ g h) a = g x₂

Tactic:
exact ⟨Submodule.Quotient.mk x₂, rfl⟩

Result:
no goals
-- Mathlib/Data/List/DropRight.lean
lemma rdrop_add (i j : ℕ) : (l.rdrop i).rdrop j = l.rdrop (i + j)

Proof state:
α : Type u_1
l : List α
i j : ℕ
⊢ (l.rdrop i).rdrop j = l.rdrop (i + j)

Tactic:
simp_rw [rdrop_eq_reverse_drop_reverse, reverse_reverse, drop_drop]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean
theorem involute_eq_id :
    (involute : CliffordAlgebra (0 : QuadraticForm R Unit) →ₐ[R] _) = AlgHom.id R _

Proof state:
case a.h
R : Type u_1
inst✝ : CommRing R
x✝ : Unit
⊢ (involute.toLinearMap ∘ₗ ι 0) x✝ = ((AlgHom.id R (CliffordAlgebra 0)).toLinearMap ∘ₗ ι 0) x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ involute = AlgHom.id R (CliffordAlgebra 0)

Tactic:
ext

Result:
case a.h
R : Type u_1
inst✝ : CommRing R
x✝ : Unit
⊢ (involute.toLinearMap ∘ₗ ι 0) x✝ = ((AlgHom.id R (CliffordAlgebra 0)).toLinearMap ∘ₗ ι 0) x✝
-- Mathlib/Order/Filter/AtTopBot/Defs.lean
theorem Frequently.forall_exists_of_atTop [Preorder α] {p : α → Prop}
    (h : ∃ᶠ x in atTop, p x) (a : α) : ∃ b ≥ a, p b

Proof state:
α : Type u_3
inst✝ : Preorder α
p : α → Prop
a : α
h : ∀ b ≥ a, ¬p b
⊢ ∀ᶠ (x : α) in atTop, ¬p x

Tactic:
exact (eventually_ge_atTop a).mono h

Result:
no goals

Proof state:
α : Type u_3
inst✝ : Preorder α
p : α → Prop
h : ∃ᶠ (x : α) in atTop, p x
a : α
⊢ ∃ b ≥ a, p b

Tactic:
rw [Filter.Frequently] at h

Result:
α : Type u_3
inst✝ : Preorder α
p : α → Prop
h : ¬∀ᶠ (x : α) in atTop, ¬p x
a : α
⊢ ∃ b ≥ a, p b

Proof state:
α : Type u_3
inst✝ : Preorder α
p : α → Prop
h : ¬∀ᶠ (x : α) in atTop, ¬p x
a : α
⊢ ∃ b ≥ a, p b

Tactic:
contrapose! h

Result:
α : Type u_3
inst✝ : Preorder α
p : α → Prop
a : α
h : ∀ b ≥ a, ¬p b
⊢ ∀ᶠ (x : α) in atTop, ¬p x
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem mem_sSup_of_mem {S : Set (Submonoid M)} {s : Submonoid M} (hs : s ∈ S) :
    ∀ {x : M}, x ∈ s → x ∈ sSup S

Proof state:
M : Type u_1
inst✝ : MulOneClass M
S : Set (Submonoid M)
s : Submonoid M
hs : s ∈ S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S

Tactic:
rw [← SetLike.le_def]

Result:
M : Type u_1
inst✝ : MulOneClass M
S : Set (Submonoid M)
s : Submonoid M
hs : s ∈ S
⊢ s ≤ sSup S

Proof state:
M : Type u_1
inst✝ : MulOneClass M
S : Set (Submonoid M)
s : Submonoid M
hs : s ∈ S
⊢ s ≤ sSup S

Tactic:
exact le_sSup hs

Result:
no goals
-- Mathlib/RingTheory/Valuation/Quotient.lean
theorem supp_quot_supp : supp (v.onQuot le_rfl) = 0

Proof state:
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
⊢ (v.onQuot ⋯).supp = 0

Tactic:
rw [supp_quot]

Result:
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
⊢ Ideal.map (Ideal.Quotient.mk v.supp) v.supp = 0

Proof state:
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
⊢ Ideal.map (Ideal.Quotient.mk v.supp) v.supp = 0

Tactic:
exact Ideal.map_quotient_self _

Result:
no goals