harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Galois/Basic.lean
@[simp]
lemma fiberEqualizerEquiv_symm_ι_apply {X Y : C} {f g : X ⟶ Y} (x : F.obj X)
    (h : F.map f x = F.map g x) :
    F.map (equalizer.ι f g) ((fiberEqualizerEquiv F f g).symm ⟨x, h⟩) = x

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f g : X ⟶ Y
x : (F.obj X).carrier
h : F.map f x = F.map g x
⊢ F.map (equalizer.ι f g)
      ((PreservesEqualizer.iso (F ⋙ FintypeCat.incl) f g).inv ((Types.equalizerIso (F.map f) (F.map g)).inv ⟨x, h⟩)) =
    x

Tactic:
change ((Types.equalizerIso _ _).inv ≫ _ ≫ (F ⋙ FintypeCat.incl).map (equalizer.ι f g)) _ = _

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f g : X ⟶ Y
x : (F.obj X).carrier
h : F.map f x = F.map g x
⊢ ((Types.equalizerIso (F.map f) (F.map g)).inv ≫
        (PreservesEqualizer.iso (F ⋙ FintypeCat.incl) f g).inv ≫ (F ⋙ FintypeCat.incl).map (equalizer.ι f g))
      ⟨x, h⟩ =
    x

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f g : X ⟶ Y
x : (F.obj X).carrier
h : F.map f x = F.map g x
⊢ F.map (equalizer.ι f g) ((fiberEqualizerEquiv F f g).symm ⟨x, h⟩) = x

Tactic:
simp [fiberEqualizerEquiv]

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f g : X ⟶ Y
x : (F.obj X).carrier
h : F.map f x = F.map g x
⊢ F.map (equalizer.ι f g)
      ((PreservesEqualizer.iso (F ⋙ FintypeCat.incl) f g).inv ((Types.equalizerIso (F.map f) (F.map g)).inv ⟨x, h⟩)) =
    x

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
f g : X ⟶ Y
x : (F.obj X).carrier
h : F.map f x = F.map g x
⊢ ((Types.equalizerIso (F.map f) (F.map g)).inv ≫
        (PreservesEqualizer.iso (F ⋙ FintypeCat.incl) f g).inv ≫ (F ⋙ FintypeCat.incl).map (equalizer.ι f g))
      ⟨x, h⟩ =
    x

Tactic:
erw [PreservesEqualizer.iso_inv_ι, Types.equalizerIso_inv_comp_ι]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem orderOf_le_of_pow_eq_one (hn : 0 < n) (h : x ^ n = 1) : orderOf x ≤ n :=
  IsPeriodicPt.minimalPeriod_le hn (by rwa [isPeriodicPt_mul_iff_pow_eq_one])

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
hn : 0 < n
h : x ^ n = 1
⊢ IsPeriodicPt (fun x_1 => x * x_1) n 1

Tactic:
rwa [isPeriodicPt_mul_iff_pow_eq_one]

Result:
no goals
-- Mathlib/RingTheory/ClassGroup.lean
theorem ClassGroup.mk_canonicalEquiv (K' : Type*) [Field K'] [Algebra R K'] [IsFractionRing R K']
    (I : (FractionalIdeal R⁰ K)ˣ) :
    ClassGroup.mk (Units.map (↑(canonicalEquiv R⁰ K K')) I : (FractionalIdeal R⁰ K')ˣ) =
      ClassGroup.mk I

Proof state:
R : Type u_1
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : Field K
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : IsDomain R
K' : Type u_3
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : (FractionalIdeal R⁰ K)ˣ
⊢ mk ((Units.map ↑(canonicalEquiv R⁰ K K')) I) = mk I

Tactic:
erw [ClassGroup.mk, MonoidHom.comp_apply, ← MonoidHom.comp_apply (Units.map _),
    ← Units.map_comp, ← RingEquiv.coe_monoidHom_trans,
    FractionalIdeal.canonicalEquiv_trans_canonicalEquiv]

Result:
R : Type u_1
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : Field K
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : IsDomain R
K' : Type u_3
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : (FractionalIdeal R⁰ K)ˣ
⊢ (QuotientGroup.mk' (toPrincipalIdeal R (FractionRing R)).range)
      ((Units.map ↑(canonicalEquiv R⁰ K (FractionRing R))) I) =
    mk I

Proof state:
R : Type u_1
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : Field K
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : IsDomain R
K' : Type u_3
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : (FractionalIdeal R⁰ K)ˣ
⊢ (QuotientGroup.mk' (toPrincipalIdeal R (FractionRing R)).range)
      ((Units.map ↑(canonicalEquiv R⁰ K (FractionRing R))) I) =
    mk I

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/MetricSpace/IsometricSMul.lean
theorem preimage_mul_right_ball [IsometricSMul Gᵐᵒᵖ G] (a b : G) (r : ℝ) :
    (fun x => x * a) ⁻¹' ball b r = ball (b / a) r

Proof state:
G : Type v
inst✝² : Group G
inst✝¹ : PseudoMetricSpace G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ
⊢ (fun x => x * a) ⁻¹' ball b r = ball (b / a) r

Tactic:
rw [div_eq_mul_inv]

Result:
G : Type v
inst✝² : Group G
inst✝¹ : PseudoMetricSpace G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ
⊢ (fun x => x * a) ⁻¹' ball b r = ball (b * a⁻¹) r

Proof state:
G : Type v
inst✝² : Group G
inst✝¹ : PseudoMetricSpace G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ
⊢ (fun x => x * a) ⁻¹' ball b r = ball (b * a⁻¹) r

Tactic:
exact preimage_smul_ball (MulOpposite.op a) b r

Result:
no goals
-- Mathlib/CategoryTheory/Sites/DenseSubsite/Basic.lean
theorem appHom_valid_glue {X : D} {Y : C} (f : op X ⟶ op (G.obj Y)) :
    appHom α X ≫ ℱ'.val.map f = ℱ.map f ≫ α.app (op Y)

Proof state:
C : Type u_1
inst✝³ : Category.{u_6, u_1} C
D : Type u_2
inst✝² : Category.{u_5, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : D
Y : C
f : op X ⟶ op (G.obj Y)
⊢ appHom α X ≫ ℱ'.val.map f = ℱ.map f ≫ α.app (op Y)

Tactic:
ext

Result:
case h
C : Type u_1
inst✝³ : Category.{u_6, u_1} C
D : Type u_2
inst✝² : Category.{u_5, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : D
Y : C
f : op X ⟶ op (G.obj Y)
a✝ : ℱ.obj (op X)
⊢ (appHom α X ≫ ℱ'.val.map f) a✝ = (ℱ.map f ≫ α.app (op Y)) a✝

Proof state:
case h
C : Type u_1
inst✝³ : Category.{u_6, u_1} C
D : Type u_2
inst✝² : Category.{u_5, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : D
Y : C
f : op X ⟶ op (G.obj Y)
a✝ : ℱ.obj (op X)
⊢ (appHom α X ≫ ℱ'.val.map f) a✝ = (ℱ.map f ≫ α.app (op Y)) a✝

Tactic:
apply appHom_restrict

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem mul_zero (a : R) : a * 0 = 0

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ a * 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem factorial_dvd_factorial {m n} (h : m ≤ n) : m ! ∣ n !

Proof state:
case refl
m n : ℕ
⊢ m ! ∣ m !

Tactic:
exact Nat.dvd_refl _

Result:
no goals

Proof state:
case step
m n m✝ : ℕ
a✝ : m.le m✝
ih : m ! ∣ m✝!
⊢ m ! ∣ m✝.succ !

Tactic:
exact Nat.dvd_trans ih (Nat.dvd_mul_left _ _)

Result:
no goals

Proof state:
m n : ℕ
h : m ≤ n
⊢ m ! ∣ n !

Tactic:
induction h with
| refl => exact Nat.dvd_refl _
| step _ ih => exact Nat.dvd_trans ih (Nat.dvd_mul_left _ _)

Result:
no goals
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
theorem mkQ_map_self : map p.mkQ p = ⊥

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
⊢ map p.mkQ p = ⊥

Tactic:
rw [eq_bot_iff, map_le_iff_le_comap, comap_bot, ker_mkQ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem flatMap_reverse {β} (l : List α) (f : α → List β) : (l.reverse.flatMap f) = (l.flatMap (reverse ∘ f)).reverse

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : α → List β
⊢ flatMap f l.reverse = (flatMap (reverse ∘ f) l).reverse

Tactic:
induction l <;> simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_erase_self [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {fallback : β} :
    getD (m.erase k) k fallback = fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k : α
fallback : β
⊢ getD (m.erase k) k fallback = fallback

Tactic:
simp_to_model [erase] using List.getValueD_eraseKey_self

Result:
no goals
-- Mathlib/Algebra/Ring/SumsOfSquares.lean
theorem IsSumSq.add [AddMonoid R] [Mul R] {s₁ s₂ : R}
    (h₁ : IsSumSq s₁) (h₂ : IsSumSq s₂) : IsSumSq (s₁ + s₂)

Proof state:
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
s₁ s₂ : R
h₁ : IsSumSq s₁
h₂ : IsSumSq s₂
⊢ IsSumSq (s₁ + s₂)

Tactic:
induction h₁ <;> simp_all [add_assoc, sq_add]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/CompatibleSheafification.lean
theorem sheafificationWhiskerLeftIso_hom_app (P : Cᵒᵖ ⥤ D) (F : D ⥤ E)
    [∀ (F : D ⥤ E) (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F]
    [∀ (F : D ⥤ E) (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D),
        PreservesLimit (W.index P).multicospan F] :
    (sheafificationWhiskerLeftIso J P).hom.app F = (J.sheafifyCompIso F P).hom

Proof state:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
P : Cᵒᵖ ⥤ D
F : D ⥤ E
inst✝¹ : ∀ (F : D ⥤ E) (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (F : D ⥤ E) (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
⊢ (J.sheafificationWhiskerLeftIso P).hom.app F = (J.sheafifyCompIso F P).hom

Tactic:
dsimp [sheafificationWhiskerLeftIso, sheafifyCompIso]

Result:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
P : Cᵒᵖ ⥤ D
F : D ⥤ E
inst✝¹ : ∀ (F : D ⥤ E) (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (F : D ⥤ E) (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
⊢ (J.plusCompIso F (J.plusObj P)).hom ≫ J.plusMap (J.plusCompIso F P).hom ≫ 𝟙 (J.plusObj (J.plusObj (P ⋙ F))) =
    (J.plusCompIso F (J.plusObj P)).hom ≫ J.plusMap (J.plusCompIso F P).hom

Proof state:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
P : Cᵒᵖ ⥤ D
F : D ⥤ E
inst✝¹ : ∀ (F : D ⥤ E) (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (F : D ⥤ E) (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
⊢ (J.plusCompIso F (J.plusObj P)).hom ≫ J.plusMap (J.plusCompIso F P).hom ≫ 𝟙 (J.plusObj (J.plusObj (P ⋙ F))) =
    (J.plusCompIso F (J.plusObj P)).hom ≫ J.plusMap (J.plusCompIso F P).hom

Tactic:
rw [Category.comp_id]

Result:
no goals
-- Mathlib/Logic/Basic.lean
lemma forall_or_exists_not (P : α → Prop) : (∀ a, P a) ∨ ∃ a, ¬ P a

Proof state:
α : Sort u_1
P : α → Prop
⊢ (∀ (a : α), P a) ∨ ∃ a, ¬P a

Tactic:
rw [← not_forall]

Result:
α : Sort u_1
P : α → Prop
⊢ (∀ (a : α), P a) ∨ ¬∀ (x : α), P x

Proof state:
α : Sort u_1
P : α → Prop
⊢ (∀ (a : α), P a) ∨ ¬∀ (x : α), P x

Tactic:
exact em _

Result:
no goals
-- Mathlib/CategoryTheory/Limits/IsLimit.lean
theorem coneOfHom_homOfCone (s : Cone F) : coneOfHom h (homOfCone h s) = s

Proof state:
case e_π
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : yoneda.obj X ⋙ uliftFunctor.{u₁, v₃} ≅ F.cones
s : Cone F
s_pt : C
s_π : (const J).obj s_pt ⟶ F
⊢ h.hom.app (op s_pt) { down := (h.inv.app (op s_pt) s_π).down } = s_π

Tactic:
convert congrFun (congrFun (congrArg NatTrans.app h.inv_hom_id) (op s_pt)) s_π using 1

Result:
no goals

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : yoneda.obj X ⋙ uliftFunctor.{u₁, v₃} ≅ F.cones
s : Cone F
s_pt : C
s_π : (const J).obj s_pt ⟶ F
⊢ { pt := { pt := s_pt, π := s_π }.pt,
      π :=
        h.hom.app (op { pt := s_pt, π := s_π }.pt)
          { down := (h.inv.app (op { pt := s_pt, π := s_π }.pt) { pt := s_pt, π := s_π }.π).down } } =
    { pt := s_pt, π := s_π }

Tactic:
congr

Result:
case e_π
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : yoneda.obj X ⋙ uliftFunctor.{u₁, v₃} ≅ F.cones
s : Cone F
s_pt : C
s_π : (const J).obj s_pt ⟶ F
⊢ h.hom.app (op { pt := s_pt, π := s_π }.pt)
      { down := (h.inv.app (op { pt := s_pt, π := s_π }.pt) { pt := s_pt, π := s_π }.π).down } =
    s_π

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : yoneda.obj X ⋙ uliftFunctor.{u₁, v₃} ≅ F.cones
s : Cone F
⊢ { pt := s.pt, π := h.hom.app (op s.pt) { down := (h.inv.app (op s.pt) s.π).down } } = s

Tactic:
match s with
| .mk s_pt s_π =>
  congr; dsimp
  convert congrFun (congrFun (congrArg NatTrans.app h.inv_hom_id) (op s_pt)) s_π using 1

Result:
no goals

Proof state:
case e_π
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : yoneda.obj X ⋙ uliftFunctor.{u₁, v₃} ≅ F.cones
s : Cone F
s_pt : C
s_π : (const J).obj s_pt ⟶ F
⊢ h.hom.app (op { pt := s_pt, π := s_π }.pt)
      { down := (h.inv.app (op { pt := s_pt, π := s_π }.pt) { pt := s_pt, π := s_π }.π).down } =
    s_π

Tactic:
dsimp

Result:
case e_π
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : yoneda.obj X ⋙ uliftFunctor.{u₁, v₃} ≅ F.cones
s : Cone F
s_pt : C
s_π : (const J).obj s_pt ⟶ F
⊢ h.hom.app (op s_pt) { down := (h.inv.app (op s_pt) s_π).down } = s_π

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : yoneda.obj X ⋙ uliftFunctor.{u₁, v₃} ≅ F.cones
s : Cone F
⊢ coneOfHom h (homOfCone h s) = s

Tactic:
dsimp [coneOfHom, homOfCone]

Result:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : yoneda.obj X ⋙ uliftFunctor.{u₁, v₃} ≅ F.cones
s : Cone F
⊢ { pt := s.pt, π := h.hom.app (op s.pt) { down := (h.inv.app (op s.pt) s.π).down } } = s
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem inr_fst' {b : BinaryBicone X Y} (h : b.IsBilimit) :
    IsPushout b.inr (0 : Y ⟶ 0) b.fst (0 : 0 ⟶ X)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPushout 0 (0 ≫ 0) (b.inl ≫ b.fst) 0

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ b.inr ≫ b.fst = 0 ≫ 0

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPushout b.inr 0 b.fst 0

Tactic:
refine of_top ?_ (by simp) (of_isBilimit h)

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
b : BinaryBicone X Y
h : b.IsBilimit
⊢ IsPushout 0 (0 ≫ 0) (b.inl ≫ b.fst) 0
-- Mathlib/RingTheory/TensorProduct/Basic.lean
theorem baseChange_sub : (f - g).baseChange A = f.baseChange A - g.baseChange A

Proof state:
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f g : M →ₗ[R] N
⊢ baseChange A (f - g) = baseChange A f - baseChange A g

Tactic:
ext

Result:
case a.h.h
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f g : M →ₗ[R] N
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A (f - g))) 1) x✝ =
    ((AlgebraTensorModule.curry (baseChange A f - baseChange A g)) 1) x✝

Proof state:
case a.h.h
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommRing R
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f g : M →ₗ[R] N
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A (f - g))) 1) x✝ =
    ((AlgebraTensorModule.curry (baseChange A f - baseChange A g)) 1) x✝

Tactic:
simp [baseChange_eq_ltensor, tmul_sub]

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem closedBall_finset_sup (p : ι → Seminorm 𝕜 E) (s : Finset ι) (x : E) {r : ℝ} (hr : 0 ≤ r) :
    closedBall (s.sup p) x r = s.inf fun i => closedBall (p i) x r

Proof state:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ
hr : 0 ≤ r
⊢ (s.sup p).closedBall x r = ⨅ a ∈ s, (p a).closedBall x r

Tactic:
exact closedBall_finset_sup_eq_iInter _ _ _ hr

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ
hr : 0 ≤ r
⊢ (s.sup p).closedBall x r = s.inf fun i => (p i).closedBall x r

Tactic:
rw [Finset.inf_eq_iInf]

Result:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ
hr : 0 ≤ r
⊢ (s.sup p).closedBall x r = ⨅ a ∈ s, (p a).closedBall x r
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem unzip_mkArray {n : Nat} {a : α} {b : β} :
    unzip (mkArray n (a, b)) = (mkArray n a, mkArray n b)

Proof state:
α : Type u_1
β : Type u_2
n : Nat
a : α
b : β
⊢ (mkArray n (a, b)).unzip = (mkArray n a, mkArray n b)

Tactic:
ext1 <;> simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem dist_dist_dist_le_right (x y z : α) : dist (dist x y) (dist x z) ≤ dist y z

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y z : α
⊢ dist (dist x y) (dist x z) ≤ dist y z

Tactic:
simpa only [dist_comm x] using dist_dist_dist_le_left y z x

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Strong.lean
theorem whiskerLeft_naturality_comp (f : a' ⟶ G.obj a) (g : a ⟶ b) (h : b ⟶ c) :
    f ◁ (θ.naturality (g ≫ h)).hom ≫ f ◁ θ.app a ◁ H.mapComp g h =
      f ◁ G.mapComp g h ▷ θ.app c ≫
        f ◁ (α_ _ _ _).hom ≫
          f ◁ G.map g ◁ (θ.naturality h).hom ≫
            f ◁ (α_ _ _ _).inv ≫ f ◁ (θ.naturality g).hom ▷ H.map h ≫ f ◁ (α_ _ _ _).hom

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
G H : OplaxFunctor B C
θ : StrongOplaxNatTrans G H
a b c : B
a' : C
f : a' ⟶ G.obj a
g : a ⟶ b
h : b ⟶ c
⊢ f ◁ (θ.naturality (g ≫ h)).hom ≫ f ◁ θ.app a ◁ H.mapComp g h =
    f ◁ G.mapComp g h ▷ θ.app c ≫
      f ◁ (α_ (G.map g) (G.map h) (θ.app c)).hom ≫
        f ◁ G.map g ◁ (θ.naturality h).hom ≫
          f ◁ (α_ (G.map g) (θ.app b) (H.map h)).inv ≫
            f ◁ (θ.naturality g).hom ▷ H.map h ≫ f ◁ (α_ (θ.app a) (H.map g) (H.map h)).hom

Tactic:
apply θ.toOplax.whiskerLeft_naturality_comp

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem Nonempty.eq_univ [Subsingleton α] : s.Nonempty → s = univ

Proof state:
case intro
α : Type u
s : Set α
inst✝ : Subsingleton α
x : α
hx : x ∈ s
⊢ s = univ

Tactic:
exact eq_univ_of_forall fun y => by rwa [Subsingleton.elim y x]

Result:
no goals

Proof state:
α : Type u
s : Set α
inst✝ : Subsingleton α
x : α
hx : x ∈ s
y : α
⊢ y ∈ s

Tactic:
rwa [Subsingleton.elim y x]

Result:
no goals

Proof state:
α : Type u
s : Set α
inst✝ : Subsingleton α
⊢ s.Nonempty → s = univ

Tactic:
rintro ⟨x, hx⟩

Result:
case intro
α : Type u
s : Set α
inst✝ : Subsingleton α
x : α
hx : x ∈ s
⊢ s = univ
-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem gcd_mul_right' [GCDMonoid α] (a b c : α) :
    Associated (gcd (b * a) (c * a)) (gcd b c * a)

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
⊢ Associated (gcd (b * a) (c * a)) (gcd b c * a)

Tactic:
simp only [mul_comm, gcd_mul_left']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem isInfix_filter_iff {p : α → Bool} {l₁ l₂ : List α} :
    l₂ <:+: l₁.filter p ↔ ∃ l, l <:+: l₁ ∧ l₂ = l.filter p

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
⊢ l₂ <:+: filter p l₁ ↔ ∃ l, l <:+: l₁ ∧ l₂ = filter p l

Tactic:
rw [← filterMap_eq_filter, isInfix_filterMap_iff]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem T_sub_one (n : ℤ) : T R (n - 1) = 2 * X * T R n - T R (n + 1)

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ T R (n - 1) = 2 * X * T R n - T R (n + 1)

Tactic:
linear_combination (norm := ring_nf) T_add_two R (n - 1)

Result:
no goals
-- Mathlib/Topology/VectorBundle/Basic.lean
theorem coordChangeL_apply' (e e' : Trivialization F (π F E)) [e.IsLinear R] [e'.IsLinear R] {b : B}
    (hb : b ∈ e.baseSet ∩ e'.baseSet) (y : F) :
    coordChangeL R e e' b y = (e' (e.toPartialHomeomorph.symm (b, y))).2

Proof state:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : TopologicalSpace F
inst✝⁷ : TopologicalSpace B
inst✝⁶ : TopologicalSpace (TotalSpace F E)
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module R F
inst✝³ : (x : B) → AddCommMonoid (E x)
inst✝² : (x : B) → Module R (E x)
e e' : Trivialization F TotalSpace.proj
inst✝¹ : Trivialization.IsLinear R e
inst✝ : Trivialization.IsLinear R e'
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
y : F
⊢ (coordChangeL R e e' b) y = (↑e' (↑e.symm (b, y))).2

Tactic:
rw [e.coordChangeL_apply e' hb, e.mk_symm hb.1]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Invariant.lean
@[simp]
protected lemma id :
    invtSubmodule (LinearMap.id : End R M) = ⊤ :=
  eq_top_iff.mpr fun x ↦ by simp [invtSubmodule]

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : Submodule R M
⊢ x ∈ ⊤ → x ∈ invtSubmodule LinearMap.id

Tactic:
simp [invtSubmodule]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Int.lean
theorem add_nonnneg_iff_neg_le {a b : Int} : 0 ≤ a + b ↔ -b ≤ a

Proof state:
a b : Int
⊢ 0 ≤ a + b ↔ -b ≤ a

Tactic:
rw [le_add_iff_sub_le, Int.zero_sub]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Lattice.lean
lemma inf_iInf {ι : Type*} [Nonempty ι] {p : ι → Submodule R M} (q : Submodule R M) :
    q ⊓ ⨅ i, p i = ⨅ i, q ⊓ p i :=
  SetLike.coe_injective <| by simpa only [inf_coe, iInf_coe] using Set.inter_iInter _ _

Proof state:
R : Type u_1
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Nonempty ι
p : ι → Submodule R M
q : Submodule R M
⊢ ↑(q ⊓ ⨅ i, p i) = ↑(⨅ i, q ⊓ p i)

Tactic:
simpa only [inf_coe, iInf_coe] using Set.inter_iInter _ _

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/RightDerived.lean
@[reassoc (attr := simp)]
lemma toRightDerivedZero'_comp_iCycles {C} [Category C] [Abelian C] {X : C}
    (P : InjectiveResolution X) (F : C ⥤ D) [F.Additive] :
    P.toRightDerivedZero' F ≫
      HomologicalComplex.iCycles _ _ = F.map (P.ι.f 0)

Proof state:
D : Type u_1
inst✝⁴ : Category.{u_4, u_1} D
inst✝³ : Abelian D
C : Type u_2
inst✝² : Category.{u_3, u_2} C
inst✝¹ : Abelian C
X : C
P : InjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
⊢ P.toRightDerivedZero' F ≫ ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex).iCycles 0 = F.map (P.ι.f 0)

Tactic:
simp [toRightDerivedZero']

Result:
no goals