harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_lt_cos_of_nonneg_of_le_pi {x y : ℝ} (hx₁ : 0 ≤ x) (hy₂ : y ≤ π) (hxy : x < y) :
    cos y < cos x

Proof state:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
⊢ cos y < cos x

Tactic:
rw [← sin_pi_div_two_sub, ← sin_pi_div_two_sub]

Result:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
⊢ sin (π / 2 - y) < sin (π / 2 - x)

Proof state:
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
⊢ sin (π / 2 - y) < sin (π / 2 - x)

Tactic:
apply sin_lt_sin_of_lt_of_le_pi_div_two <;> linarith

Result:
no goals
-- Mathlib/Data/Sign.lean
/-- `SignType.sign` respects strictly monotone zero-preserving maps. -/
lemma StrictMono.sign_comp {β F : Type*} [Zero β] [Preorder β] [DecidableRel ((· < ·) : β → β → _)]
    [FunLike F α β] [ZeroHomClass F α β] {f : F} (hf : StrictMono f) (a : α) :
    sign (f a) = sign a

Proof state:
α : Type u_1
inst✝⁶ : Zero α
inst✝⁵ : LinearOrder α
β : Type u_2
F : Type u_3
inst✝⁴ : Zero β
inst✝³ : Preorder β
inst✝² : DecidableRel fun x1 x2 => x1 < x2
inst✝¹ : FunLike F α β
inst✝ : ZeroHomClass F α β
f : F
hf : StrictMono ⇑f
a : α
⊢ sign (f a) = sign a

Tactic:
simp only [sign_apply, ← map_zero f, hf.lt_iff_lt]

Result:
no goals
-- Mathlib/CategoryTheory/Galois/IsFundamentalgroup.lean
lemma toAut_isHomeomorph : IsHomeomorph (toAut F G)

Proof state:
C : Type u₁
inst✝⁸ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁷ : GaloisCategory C
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).carrier
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : IsFundamentalGroup F G
⊢ Continuous ⇑(toAut F G) ∧ Function.Bijective ⇑(toAut F G)

Tactic:
exact ⟨toAut_continuous F G, toAut_bijective F G⟩

Result:
no goals

Proof state:
C : Type u₁
inst✝⁸ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁷ : GaloisCategory C
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).carrier
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : IsFundamentalGroup F G
⊢ IsHomeomorph ⇑(toAut F G)

Tactic:
rw [isHomeomorph_iff_continuous_bijective]

Result:
C : Type u₁
inst✝⁸ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝⁷ : GaloisCategory C
G : Type u_1
inst✝⁶ : Group G
inst✝⁵ : (X : C) → MulAction G (F.obj X).carrier
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : IsFundamentalGroup F G
⊢ Continuous ⇑(toAut F G) ∧ Function.Bijective ⇑(toAut F G)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem find?_range_eq_some {n : Nat} {i : Nat} {p : Nat → Bool} :
    (range n).find? p = some i ↔ p i ∧ i ∈ range n ∧ ∀ j, j < i → !p j

Proof state:
n i : Nat
p : Nat → Bool
⊢ find? p (range n) = some i ↔ p i = true ∧ i ∈ range n ∧ ∀ (j : Nat), j < i → (!p j) = true

Tactic:
simp [range_eq_range']

Result:
no goals
-- Mathlib/Data/Bool/Count.lean
theorem length_sub_one_le_two_mul_count_bool (hl : Chain' (· ≠ ·) l) (b : Bool) :
    length l - 1 ≤ 2 * count b l

Proof state:
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) l
b : Bool
⊢ l.length - 1 ≤ if Even l.length then l.length else if (some b == l.head?) = true then l.length + 1 else l.length - 1

Tactic:
split_ifs <;> simp [le_tsub_add, Nat.le_succ_of_le]

Result:
no goals

Proof state:
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) l
b : Bool
⊢ l.length - 1 ≤ 2 * count b l

Tactic:
rw [hl.two_mul_count_bool_eq_ite]

Result:
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) l
b : Bool
⊢ l.length - 1 ≤ if Even l.length then l.length else if (some b == l.head?) = true then l.length + 1 else l.length - 1
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@[reassoc (attr := simp)]
lemma δ_fst (X Y : C) : OplaxMonoidal.δ F X Y ≫ fst _ _ = F.map (fst _ _)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ChosenFiniteProducts C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
inst✝ : ChosenFiniteProducts D
F : C ⥤ D
X Y : C
⊢ OplaxMonoidal.δ F X Y ≫ fst (F.obj X) (F.obj Y) = F.map (fst X Y)

Tactic:
simp [δ_of_chosenFiniteProducts]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_le_pi_div_two_iff {z : ℂ} : arg z ≤ π / 2 ↔ 0 ≤ re z ∨ im z < 0

Proof state:
case inl
z : ℂ
hre : 0 ≤ z.re
⊢ z.arg ≤ π / 2 ↔ 0 ≤ z.re ∨ z.im < 0

Tactic:
simp only [hre, arg_of_re_nonneg hre, Real.arcsin_le_pi_div_two, true_or]

Result:
no goals

Proof state:
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ z.arg ≤ π / 2 ↔ z.im < 0

Tactic:
simp only [him.not_lt]

Result:
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ z.arg ≤ π / 2 ↔ False

Proof state:
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ z.arg ≤ π / 2 ↔ False

Tactic:
rw [iff_false, not_le, arg_of_re_neg_of_im_nonneg hre him, ← sub_lt_iff_lt_add, half_sub,
  Real.neg_pi_div_two_lt_arcsin, neg_im, neg_div, neg_lt_neg_iff, div_lt_one, ←
  abs_of_nonneg him, abs_im_lt_norm]

Result:
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ z.re ≠ 0

case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ 0 < ‖z‖

Proof state:
case inr
z : ℂ
hre : z.re < 0
⊢ z.arg ≤ π / 2 ↔ 0 ≤ z.re ∨ z.im < 0

Tactic:
simp only [hre.not_le, false_or]

Result:
case inr
z : ℂ
hre : z.re < 0
⊢ z.arg ≤ π / 2 ↔ z.im < 0

Proof state:
case inr
z : ℂ
hre : z.re < 0
⊢ z.arg ≤ π / 2 ↔ z.im < 0

Tactic:
rcases le_or_lt 0 (im z) with him | him

Result:
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ z.arg ≤ π / 2 ↔ z.im < 0

case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ z.arg ≤ π / 2 ↔ z.im < 0

Proof state:
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ z.arg ≤ π / 2 ↔ True

Tactic:
rw [iff_true, arg_of_re_neg_of_im_neg hre him]

Result:
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ Real.arcsin ((-z).im / ‖z‖) - π ≤ π / 2

Proof state:
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ Real.arcsin ((-z).im / ‖z‖) - π ≤ π / 2

Tactic:
exact (sub_le_self _ Real.pi_pos.le).trans (Real.arcsin_le_pi_div_two _)

Result:
no goals

Proof state:
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ z.arg ≤ π / 2 ↔ z.im < 0

Tactic:
simp only [him]

Result:
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ z.arg ≤ π / 2 ↔ True

Proof state:
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ z.re ≠ 0

case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ 0 < ‖z‖

Tactic:
exacts [hre.ne, norm_pos_iff.mpr <| ne_of_apply_ne re hre.ne]

Result:
no goals

Proof state:
z : ℂ
⊢ z.arg ≤ π / 2 ↔ 0 ≤ z.re ∨ z.im < 0

Tactic:
rcases le_or_lt 0 (re z) with hre | hre

Result:
case inl
z : ℂ
hre : 0 ≤ z.re
⊢ z.arg ≤ π / 2 ↔ 0 ≤ z.re ∨ z.im < 0

case inr
z : ℂ
hre : z.re < 0
⊢ z.arg ≤ π / 2 ↔ 0 ≤ z.re ∨ z.im < 0
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_equivSentence [L[[α]].Structure M] [(L.lhomWithConstants α).IsExpansionOn M]
    (φ : L.Formula α) : (equivSentence φ).Realize M ↔ φ.Realize fun a => (L.con a : M)

Proof state:
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
φ : L.Formula α
⊢ M ⊨ equivSentence φ ↔ φ.Realize fun a => ↑(L.con a)

Tactic:
rw [← realize_equivSentence_symm_con M (equivSentence φ), _root_.Equiv.symm_apply_apply]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Scheme.lean
theorem appLE_comp_appLE {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U V W e₁ e₂) :
    g.appLE U V e₁ ≫ f.appLE V W e₂ =
      (f ≫ g).appLE U W (e₂.trans ((Opens.map f.base).map (homOfLE e₁)).le)

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
V : Y.Opens
W : X.Opens
e₁ : V ≤ g ⁻¹ᵁ U
e₂ : W ≤ f ⁻¹ᵁ V
⊢ Hom.appLE g U V e₁ ≫ Hom.appLE f V W e₂ = Hom.appLE (f ≫ g) U W ⋯

Tactic:
dsimp [Hom.appLE]

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
V : Y.Opens
W : X.Opens
e₁ : V ≤ g ⁻¹ᵁ U
e₂ : W ≤ f ⁻¹ᵁ V
⊢ (Hom.app g U ≫ Y.presheaf.map (homOfLE e₁).op) ≫ Hom.app f V ≫ X.presheaf.map (homOfLE e₂).op =
    (Hom.app g U ≫ Hom.app f (g ⁻¹ᵁ U)) ≫ X.presheaf.map (homOfLE ⋯).op

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
V : Y.Opens
W : X.Opens
e₁ : V ≤ g ⁻¹ᵁ U
e₂ : W ≤ f ⁻¹ᵁ V
⊢ Hom.app g U ≫
      Hom.app f (g ⁻¹ᵁ U) ≫ X.presheaf.map (((Opens.map f.base).map (homOfLE e₁).op.unop).op ≫ (homOfLE e₂).op) =
    (Hom.app g U ≫ Hom.app f (g ⁻¹ᵁ U)) ≫ X.presheaf.map (homOfLE ⋯).op

Tactic:
rfl

Result:
no goals

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
V : Y.Opens
W : X.Opens
e₁ : V ≤ g ⁻¹ᵁ U
e₂ : W ≤ f ⁻¹ᵁ V
⊢ (Hom.app g U ≫ Y.presheaf.map (homOfLE e₁).op) ≫ Hom.app f V ≫ X.presheaf.map (homOfLE e₂).op =
    (Hom.app g U ≫ Hom.app f (g ⁻¹ᵁ U)) ≫ X.presheaf.map (homOfLE ⋯).op

Tactic:
rw [Category.assoc, f.naturality_assoc, ← Functor.map_comp]

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
V : Y.Opens
W : X.Opens
e₁ : V ≤ g ⁻¹ᵁ U
e₂ : W ≤ f ⁻¹ᵁ V
⊢ Hom.app g U ≫
      Hom.app f (g ⁻¹ᵁ U) ≫ X.presheaf.map (((Opens.map f.base).map (homOfLE e₁).op.unop).op ≫ (homOfLE e₂).op) =
    (Hom.app g U ≫ Hom.app f (g ⁻¹ᵁ U)) ≫ X.presheaf.map (homOfLE ⋯).op
-- Mathlib/CategoryTheory/Limits/IndYoneda.lean
@[reassoc (attr := simp)]
lemma colimitHomIsoLimitYoneda'_hom_comp_π [HasLimitsOfShape I (Type u₂)] (A : C) (i : I) :
    (colimitHomIsoLimitYoneda' F A).hom ≫ limit.π (F.rightOp ⋙ yoneda.obj A) i =
      (coyoneda.map (colimit.ι F ⟨i⟩).op).app A

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : Iᵒᵖ ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape I (Type u₂)
A : C
i : I
⊢ (colimitHomIsoLimitYoneda' F A).hom ≫ limit.π (F.rightOp ⋙ yoneda.obj A) i =
    (coyoneda.map (colimit.ι F (op i)).op).app A

Tactic:
simp only [yoneda_obj_obj, colimitHomIsoLimitYoneda', Iso.trans_hom,
  Iso.app_hom, Category.assoc]

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : Iᵒᵖ ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape I (Type u₂)
A : C
i : I
⊢ (coyonedaOpColimitIsoLimitCoyoneda' F).hom.app A ≫
      (limitObjIsoLimitCompEvaluation (F.rightOp ⋙ coyoneda) A).hom ≫ limit.π (F.rightOp ⋙ yoneda.obj A) i =
    (coyoneda.map (colimit.ι F (op i)).op).app A

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : Iᵒᵖ ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape I (Type u₂)
A : C
i : I
⊢ ((coyonedaOpColimitIsoLimitCoyoneda' F).hom ≫ limit.π (F.rightOp ⋙ coyoneda) i).app A =
    (coyoneda.map (colimit.ι F (op i)).op).app A

Tactic:
rw [coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π]

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : Iᵒᵖ ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape I (Type u₂)
A : C
i : I
⊢ (coyonedaOpColimitIsoLimitCoyoneda' F).hom.app A ≫
      (limitObjIsoLimitCompEvaluation (F.rightOp ⋙ coyoneda) A).hom ≫ limit.π (F.rightOp ⋙ yoneda.obj A) i =
    (coyoneda.map (colimit.ι F (op i)).op).app A

Tactic:
erw [limitObjIsoLimitCompEvaluation_hom_π]

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : Iᵒᵖ ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape I (Type u₂)
A : C
i : I
⊢ (coyonedaOpColimitIsoLimitCoyoneda' F).hom.app A ≫ (limit.π (F.rightOp ⋙ coyoneda) i).app A =
    (coyoneda.map (colimit.ι F (op i)).op).app A

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : Iᵒᵖ ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape I (Type u₂)
A : C
i : I
⊢ (coyonedaOpColimitIsoLimitCoyoneda' F).hom.app A ≫ (limit.π (F.rightOp ⋙ coyoneda) i).app A =
    (coyoneda.map (colimit.ι F (op i)).op).app A

Tactic:
change ((coyonedaOpColimitIsoLimitCoyoneda' F).hom ≫ _).app A = _

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : Iᵒᵖ ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape I (Type u₂)
A : C
i : I
⊢ ((coyonedaOpColimitIsoLimitCoyoneda' F).hom ≫ limit.π (F.rightOp ⋙ coyoneda) i).app A =
    (coyoneda.map (colimit.ι F (op i)).op).app A
-- Mathlib/RingTheory/HahnSeries/Addition.lean
theorem support_add_subset {x y : HahnSeries Γ R} : support (x + y) ⊆ support x ∪ support y :=
  fun a ha => by
  rw [mem_support, coeff_add] at ha
  rw [Set.mem_union, mem_support, mem_support]
  contrapose! ha
  rw [ha.1, ha.2, add_zero]

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x y : HahnSeries Γ R
a : Γ
ha : x.coeff a = 0 ∧ y.coeff a = 0
⊢ x.coeff a + y.coeff a = 0

Tactic:
rw [ha.1, ha.2, add_zero]

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x y : HahnSeries Γ R
a : Γ
ha : x.coeff a + y.coeff a ≠ 0
⊢ x.coeff a ≠ 0 ∨ y.coeff a ≠ 0

Tactic:
contrapose! ha

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x y : HahnSeries Γ R
a : Γ
ha : x.coeff a = 0 ∧ y.coeff a = 0
⊢ x.coeff a + y.coeff a = 0

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x y : HahnSeries Γ R
a : Γ
ha : a ∈ (x + y).support
⊢ a ∈ x.support ∪ y.support

Tactic:
rw [mem_support, coeff_add] at ha

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x y : HahnSeries Γ R
a : Γ
ha : x.coeff a + y.coeff a ≠ 0
⊢ a ∈ x.support ∪ y.support

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x y : HahnSeries Γ R
a : Γ
ha : x.coeff a + y.coeff a ≠ 0
⊢ a ∈ x.support ∪ y.support

Tactic:
rw [Set.mem_union, mem_support, mem_support]

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x y : HahnSeries Γ R
a : Γ
ha : x.coeff a + y.coeff a ≠ 0
⊢ x.coeff a ≠ 0 ∨ y.coeff a ≠ 0
-- Mathlib/Geometry/Manifold/Algebra/LeftInvariantDerivation.lean
theorem comp_L : (X f).comp (𝑳 I g) = X (f.comp (𝑳 I g))

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
g : G
X : LeftInvariantDerivation I G
f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ (X f).comp (𝑳 I g) = X (f.comp (𝑳 I g))

Tactic:
ext h

Result:
case h
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
g : G
X : LeftInvariantDerivation I G
f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
h : G
⊢ ((X f).comp (𝑳 I g)) h = (X (f.comp (𝑳 I g))) h

Proof state:
case h
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
g : G
X : LeftInvariantDerivation I G
f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
h : G
⊢ ((X f).comp (𝑳 I g)) h = (X (f.comp (𝑳 I g))) h

Tactic:
rw [ContMDiffMap.comp_apply, L_apply, ← evalAt_apply, evalAt_mul, hfdifferential_apply,
  fdifferential_apply, evalAt_apply]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
theorem natCast_eq_zero_or_one_of_two_eq_zero (n : ℕ) (h : (2 : R) = 0) :
    (n : R) = 0 ∨ (n : R) = 1

Proof state:
case inr
R : Type u_4
inst✝ : AddMonoidWithOne R
n : ℕ
h : 2 = 0
hn : Odd n
⊢ ↑n = 0 ∨ ↑n = 1

Tactic:
exact Or.inr <| natCast_eq_one_of_odd_of_two_eq_zero hn h

Result:
no goals

Proof state:
R : Type u_4
inst✝ : AddMonoidWithOne R
n : ℕ
h : 2 = 0
⊢ ↑n = 0 ∨ ↑n = 1

Tactic:
obtain hn | hn := Nat.even_or_odd n

Result:
case inl
R : Type u_4
inst✝ : AddMonoidWithOne R
n : ℕ
h : 2 = 0
hn : Even n
⊢ ↑n = 0 ∨ ↑n = 1

case inr
R : Type u_4
inst✝ : AddMonoidWithOne R
n : ℕ
h : 2 = 0
hn : Odd n
⊢ ↑n = 0 ∨ ↑n = 1

Proof state:
case inl
R : Type u_4
inst✝ : AddMonoidWithOne R
n : ℕ
h : 2 = 0
hn : Even n
⊢ ↑n = 0 ∨ ↑n = 1

Tactic:
exact Or.inl <| natCast_eq_zero_of_even_of_two_eq_zero hn h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Pairwise.lean
theorem pairwise_filter {p : α → Prop} [DecidablePred p] {l : List α} :
    Pairwise R (filter p l) ↔ Pairwise (fun x y => p x → p y → R x y) l

Proof state:
α : Type u_1
R : α → α → Prop
p : α → Prop
inst✝ : DecidablePred p
l : List α
⊢ Pairwise R (filter (fun b => decide (p b)) l) ↔ Pairwise (fun x y => p x → p y → R x y) l

Tactic:
rw [← filterMap_eq_filter, pairwise_filterMap]

Result:
α : Type u_1
R : α → α → Prop
p : α → Prop
inst✝ : DecidablePred p
l : List α
⊢ Pairwise
      (fun a a' =>
        ∀ (b : α),
          b ∈ Option.guard (fun x => decide (p x) = true) a →
            ∀ (b' : α), b' ∈ Option.guard (fun x => decide (p x) = true) a' → R b b')
      l ↔
    Pairwise (fun x y => p x → p y → R x y) l

Proof state:
α : Type u_1
R : α → α → Prop
p : α → Prop
inst✝ : DecidablePred p
l : List α
⊢ Pairwise
      (fun a a' =>
        ∀ (b : α),
          b ∈ Option.guard (fun x => decide (p x) = true) a →
            ∀ (b' : α), b' ∈ Option.guard (fun x => decide (p x) = true) a' → R b b')
      l ↔
    Pairwise (fun x y => p x → p y → R x y) l

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem ofNat_le {m n : Nat} : (↑m : Int) ≤ ↑n ↔ m ≤ n :=
  ⟨fun h =>
    let ⟨k, hk⟩ := le.dest h
    Nat.le.intro <| Int.ofNat.inj <| (Int.ofNat_add m k).trans hk,
  fun h =>
    let ⟨k, (hk : m + k = n)⟩ := Nat.le.dest h
    le.intro k (by rw [← hk]; rfl)⟩

Proof state:
m n : Nat
h : m ≤ n
k : Nat
hk : m + k = n
⊢ ↑m + ↑k = ↑(m + k)

Tactic:
rfl

Result:
no goals

Proof state:
m n : Nat
h : m ≤ n
k : Nat
hk : m + k = n
⊢ ↑m + ↑k = ↑n

Tactic:
rw [← hk]

Result:
m n : Nat
h : m ≤ n
k : Nat
hk : m + k = n
⊢ ↑m + ↑k = ↑(m + k)
-- Mathlib/Data/Set/Insert.lean
theorem insert_diff_of_mem (s) (h : a ∈ t) : insert a s \ t = s \ t

Proof state:
case h
α : Type u
t : Set α
a : α
s : Set α
h : a ∈ t
x✝ : α
⊢ x✝ ∈ insert a s \ t ↔ x✝ ∈ s \ t

Tactic:
constructor <;> simp +contextual [or_imp, h]

Result:
no goals

Proof state:
α : Type u
t : Set α
a : α
s : Set α
h : a ∈ t
⊢ insert a s \ t = s \ t

Tactic:
ext

Result:
case h
α : Type u
t : Set α
a : α
s : Set α
h : a ∈ t
x✝ : α
⊢ x✝ ∈ insert a s \ t ↔ x✝ ∈ s \ t
-- Mathlib/Data/Multiset/UnionInter.lean
theorem disjoint_cons_left {a : α} {s t : Multiset α} :
    Disjoint (a ::ₘ s) t ↔ a ∉ t ∧ Disjoint s t :=
  (@disjoint_add_left _ {a} s t).trans <| by rw [singleton_disjoint]

Proof state:
α : Type u_1
a : α
s t : Multiset α
⊢ _root_.Disjoint {a} t ∧ _root_.Disjoint s t ↔ a ∉ t ∧ _root_.Disjoint s t

Tactic:
rw [singleton_disjoint]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem iterate_derivative_intCast_mul {n : ℤ} {k : ℕ} {f : R[X]} :
    derivative^[k] ((n : R[X]) * f) = n * derivative^[k] f

Proof state:
R : Type u
inst✝ : Ring R
n : ℤ
k : ℕ
f : R[X]
⊢ (⇑derivative)^[k] (↑n * f) = ↑n * (⇑derivative)^[k] f

Tactic:
induction' k with k ih generalizing f <;> simp [*]

Result:
no goals
-- Mathlib/Data/Matrix/Bilinear.lean
theorem pow_mulRightLinearMap (a : Matrix m m A) (k : ℕ) :
    mulRightLinearMap l R a ^ k = mulRightLinearMap l R (a ^ k) :=
  match k with
  | 0 => by rw [pow_zero, pow_zero, mulRightLinearMap_one, LinearMap.one_eq_id]
  | (n + 1) => by
    rw [pow_succ, pow_succ', mulRightLinearMap_mul, LinearMap.mul_eq_comp, pow_mulRightLinearMap]

Proof state:
l : Type u_1
m : Type u_2
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : Matrix m m A
k n : ℕ
⊢ mulRightLinearMap l R a ^ (n + 1) = mulRightLinearMap l R (a ^ (n + 1))

Tactic:
rw [pow_succ, pow_succ', mulRightLinearMap_mul, LinearMap.mul_eq_comp, pow_mulRightLinearMap]

Result:
no goals

Proof state:
l : Type u_1
m : Type u_2
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : Matrix m m A
k : ℕ
⊢ mulRightLinearMap l R a ^ 0 = mulRightLinearMap l R (a ^ 0)

Tactic:
rw [pow_zero, pow_zero, mulRightLinearMap_one, LinearMap.one_eq_id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/HashMap/Lemmas.lean
theorem ext {m m' : HashMap α β} : m.inner = m'.inner → m = m'

Proof state:
case mk.mk
α : Type u
β : Type v
x✝¹ : BEq α
x✝ : Hashable α
inner✝¹ inner✝ : DHashMap α fun x => β
⊢ { inner := inner✝¹ }.inner = { inner := inner✝ }.inner → { inner := inner✝¹ } = { inner := inner✝ }

Tactic:
rintro rfl

Result:
case mk.mk
α : Type u
β : Type v
x✝¹ : BEq α
x✝ : Hashable α
inner✝ : DHashMap α fun x => β
⊢ { inner := inner✝ } = { inner := { inner := inner✝ }.inner }

Proof state:
case mk
α : Type u
β : Type v
x✝¹ : BEq α
x✝ : Hashable α
m' : HashMap α β
inner✝ : DHashMap α fun x => β
⊢ { inner := inner✝ }.inner = m'.inner → { inner := inner✝ } = m'

Tactic:
cases m'

Result:
case mk.mk
α : Type u
β : Type v
x✝¹ : BEq α
x✝ : Hashable α
inner✝¹ inner✝ : DHashMap α fun x => β
⊢ { inner := inner✝¹ }.inner = { inner := inner✝ }.inner → { inner := inner✝¹ } = { inner := inner✝ }

Proof state:
α : Type u
β : Type v
x✝¹ : BEq α
x✝ : Hashable α
m m' : HashMap α β
⊢ m.inner = m'.inner → m = m'

Tactic:
cases m

Result:
case mk
α : Type u
β : Type v
x✝¹ : BEq α
x✝ : Hashable α
m' : HashMap α β
inner✝ : DHashMap α fun x => β
⊢ { inner := inner✝ }.inner = m'.inner → { inner := inner✝ } = m'

Proof state:
case mk.mk
α : Type u
β : Type v
x✝¹ : BEq α
x✝ : Hashable α
inner✝ : DHashMap α fun x => β
⊢ { inner := inner✝ } = { inner := { inner := inner✝ }.inner }

Tactic:
rfl

Result:
no goals