harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean
theorem ihom_ev_app (M N : ModuleCat.{u} R) :
    (ihom.ev M).app N = ModuleCat.ofHom (TensorProduct.uncurry R M ((ihom M).obj N) N
      (LinearMap.lcomp _ _ homLinearEquiv.toLinearMap ∘ₗ LinearMap.id.flip))

Proof state:
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ MonoidalClosed.uncurry (𝟙 ((ihom M).obj N)) =
    ↟((TensorProduct.uncurry R ↑M ↑((ihom M).obj N) ↑N) (LinearMap.lcomp R ↑N ↑homLinearEquiv ∘ₗ LinearMap.id.flip))

Tactic:
ext : 1

Result:
case hf
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ Hom.hom (MonoidalClosed.uncurry (𝟙 ((ihom M).obj N))) =
    Hom.hom
      (↟((TensorProduct.uncurry R ↑M ↑((ihom M).obj N) ↑N) (LinearMap.lcomp R ↑N ↑homLinearEquiv ∘ₗ LinearMap.id.flip)))

Proof state:
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ (ihom.ev M).app N =
    ↟((TensorProduct.uncurry R ↑M ↑((ihom M).obj N) ↑N) (LinearMap.lcomp R ↑N ↑homLinearEquiv ∘ₗ LinearMap.id.flip))

Tactic:
rw [← MonoidalClosed.uncurry_id_eq_ev]

Result:
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ MonoidalClosed.uncurry (𝟙 ((ihom M).obj N)) =
    ↟((TensorProduct.uncurry R ↑M ↑((ihom M).obj N) ↑N) (LinearMap.lcomp R ↑N ↑homLinearEquiv ∘ₗ LinearMap.id.flip))

Proof state:
case hf
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ Hom.hom (MonoidalClosed.uncurry (𝟙 ((ihom M).obj N))) =
    Hom.hom
      (↟((TensorProduct.uncurry R ↑M ↑((ihom M).obj N) ↑N) (LinearMap.lcomp R ↑N ↑homLinearEquiv ∘ₗ LinearMap.id.flip)))

Tactic:
apply TensorProduct.ext'

Result:
case hf.H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ ∀ (x : ↑M) (y : ↑((ihom M).obj N)),
    (Hom.hom (MonoidalClosed.uncurry (𝟙 ((ihom M).obj N)))) (x ⊗ₜ[R] y) =
      (Hom.hom
          (↟((TensorProduct.uncurry R ↑M ↑((ihom M).obj N) ↑N)
              (LinearMap.lcomp R ↑N ↑homLinearEquiv ∘ₗ LinearMap.id.flip))))
        (x ⊗ₜ[R] y)

Proof state:
case hf.H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ ∀ (x : ↑M) (y : ↑((ihom M).obj N)),
    (Hom.hom (MonoidalClosed.uncurry (𝟙 ((ihom M).obj N)))) (x ⊗ₜ[R] y) =
      (Hom.hom
          (↟((TensorProduct.uncurry R ↑M ↑((ihom M).obj N) ↑N)
              (LinearMap.lcomp R ↑N ↑homLinearEquiv ∘ₗ LinearMap.id.flip))))
        (x ⊗ₜ[R] y)

Tactic:
apply monoidalClosed_uncurry

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mem_singleton_self (a : α) : a ∈ #v[a]

Proof state:
α : Type u_1
a : α
⊢ a ∈ { toArray := #[a], size_toArray := ⋯ }

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Lemmas.lean
theorem splitInTwo_fst_sorted (l : { l : List α // l.length = n }) (h : Pairwise le l.1) : Pairwise le (splitInTwo l).1.1

Proof state:
α : Type u_1
n : Nat
le : α → α → Prop
l : { l // l.length = n }
h : Pairwise le l.val
⊢ Pairwise le (splitInTwo l).fst.val

Tactic:
rw [splitInTwo_fst]

Result:
α : Type u_1
n : Nat
le : α → α → Prop
l : { l // l.length = n }
h : Pairwise le l.val
⊢ Pairwise le ⟨take ((n + 1) / 2) l.val, ⋯⟩.val

Proof state:
α : Type u_1
n : Nat
le : α → α → Prop
l : { l // l.length = n }
h : Pairwise le l.val
⊢ Pairwise le ⟨take ((n + 1) / 2) l.val, ⋯⟩.val

Tactic:
exact h.take

Result:
no goals
-- Mathlib/Algebra/Polynomial/BigOperators.lean
theorem degree_prod_le : (∏ i ∈ s, f i).degree ≤ ∑ i ∈ s, (f i).degree

Proof state:
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
⊢ (∏ i ∈ s, f i).degree ≤ ∑ i ∈ s, (f i).degree

Tactic:
simpa only [Multiset.map_map] using degree_multiset_prod_le (s.1.map f)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem sum_roots_eq_nextCoeff_of_monic_of_split {P : K[X]} (hmo : P.Monic)
    (hP : P.Splits (RingHom.id K)) : P.nextCoeff = -P.roots.sum

Proof state:
K : Type v
inst✝ : Field K
P : K[X]
hmo : P.Monic
hP : Splits (RingHom.id K) P
⊢ (Multiset.map (fun a => X - C a) P.roots).prod.nextCoeff = -P.roots.sum

Tactic:
rw [Monic.nextCoeff_multiset_prod _ _ fun a ha => _]

Result:
K : Type v
inst✝ : Field K
P : K[X]
hmo : P.Monic
hP : Splits (RingHom.id K) P
⊢ (Multiset.map (fun i => (X - C i).nextCoeff) P.roots).sum = -P.roots.sum

K : Type v
inst✝ : Field K
P : K[X]
hmo : P.Monic
hP : Splits (RingHom.id K) P
⊢ ∀ a ∈ P.roots, (X - C a).Monic

Proof state:
K : Type v
inst✝ : Field K
P : K[X]
hmo : P.Monic
hP : Splits (RingHom.id K) P
⊢ ∀ a ∈ P.roots, (X - C a).Monic

Tactic:
simp only [monic_X_sub_C, implies_true]

Result:
no goals

Proof state:
K : Type v
inst✝ : Field K
P : K[X]
hmo : P.Monic
hP : Splits (RingHom.id K) P
⊢ (Multiset.map (fun i => (X - C i).nextCoeff) P.roots).sum = -P.roots.sum

Tactic:
simp_rw [nextCoeff_X_sub_C, Multiset.sum_map_neg']

Result:
no goals

Proof state:
K : Type v
inst✝ : Field K
P : K[X]
hmo : P.Monic
hP : Splits (RingHom.id K) P
⊢ P.nextCoeff = -P.roots.sum

Tactic:
nth_rw 1 [eq_prod_roots_of_monic_of_splits_id hmo hP]

Result:
K : Type v
inst✝ : Field K
P : K[X]
hmo : P.Monic
hP : Splits (RingHom.id K) P
⊢ (Multiset.map (fun a => X - C a) P.roots).prod.nextCoeff = -P.roots.sum
-- Mathlib/MeasureTheory/OuterMeasure/Induced.lean
theorem trim_anti_measurableSpace {α} (m : OuterMeasure α) {m0 m1 : MeasurableSpace α}
    (h : m0 ≤ m1) : @trim _ m1 m ≤ @trim _ m0 m

Proof state:
α : Type u_2
m : OuterMeasure α
m0 m1 : MeasurableSpace α
h : m0 ≤ m1
⊢ m.trim ≤ m.trim

Tactic:
simp only [le_trim_iff]

Result:
α : Type u_2
m : OuterMeasure α
m0 m1 : MeasurableSpace α
h : m0 ≤ m1
⊢ ∀ (s : Set α), MeasurableSet s → m.trim s ≤ m s

Proof state:
α : Type u_2
m : OuterMeasure α
m0 m1 : MeasurableSpace α
h : m0 ≤ m1
s : Set α
hs : MeasurableSet s
⊢ m.trim s ≤ m s

Tactic:
rw [trim_eq _ (h s hs)]

Result:
no goals

Proof state:
α : Type u_2
m : OuterMeasure α
m0 m1 : MeasurableSpace α
h : m0 ≤ m1
⊢ ∀ (s : Set α), MeasurableSet s → m.trim s ≤ m s

Tactic:
intro s hs

Result:
α : Type u_2
m : OuterMeasure α
m0 m1 : MeasurableSpace α
h : m0 ≤ m1
s : Set α
hs : MeasurableSet s
⊢ m.trim s ≤ m s
-- Mathlib/RingTheory/Ideal/Quotient/Defs.lean
theorem factor_eq : factor (le_refl S) = RingHom.id _

Proof state:
R : Type u
inst✝¹ : Ring R
S : Ideal R
inst✝ : S.IsTwoSided
⊢ factor ⋯ = RingHom.id (R ⧸ S)

Tactic:
ext

Result:
case h.a
R : Type u
inst✝¹ : Ring R
S : Ideal R
inst✝ : S.IsTwoSided
x✝ : R
⊢ ((factor ⋯).comp (mk S)) x✝ = ((RingHom.id (R ⧸ S)).comp (mk S)) x✝

Proof state:
case h.a
R : Type u
inst✝¹ : Ring R
S : Ideal R
inst✝ : S.IsTwoSided
x✝ : R
⊢ ((factor ⋯).comp (mk S)) x✝ = ((RingHom.id (R ⧸ S)).comp (mk S)) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/ExtClass.lean
@[simp]
lemma comp_extClass_assoc {Y : C} {n : ℕ} (γ : Ext S.X₁ Y n) {n' : ℕ} (h : 1 + n = n') :
    (Ext.mk₀ S.g).comp (hS.extClass.comp γ h) (zero_add n') = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
γ : Ext S.X₁ Y n
n' : ℕ
h : 1 + n = n'
⊢ 0 + 1 + n = n'

Tactic:
omega

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
γ : Ext S.X₁ Y n
n' : ℕ
h : 1 + n = n'
⊢ 0 + 1 = 1

Tactic:
omega

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
γ : Ext S.X₁ Y n
n' : ℕ
h : 1 + n = n'
⊢ (Ext.mk₀ S.g).comp (hS.extClass.comp γ h) ⋯ = 0

Tactic:
rw [← Ext.comp_assoc (a₁₂ := 1) _ _ _ (by omega) (by omega) (by omega),
  comp_extClass, Ext.zero_comp]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
γ : Ext S.X₁ Y n
n' : ℕ
h : 1 + n = n'
⊢ 1 + n = n'

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem infty_equiv_isometry [∀ i, PseudoEMetricSpace (β i)] :
    Isometry (WithLp.equiv ∞ (∀ i, β i)) :=
  fun x y =>
  le_antisymm (by simpa only [ENNReal.coe_one, one_mul] using lipschitzWith_equiv ∞ β x y)
    (by
      simpa only [ENNReal.div_top, ENNReal.zero_toReal, NNReal.rpow_zero, ENNReal.coe_one,
        one_mul] using antilipschitzWith_equiv ∞ β x y)

Proof state:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
x y : WithLp ⊤ ((i : ι) → β i)
⊢ edist ((WithLp.equiv ⊤ ((i : ι) → β i)) x) ((WithLp.equiv ⊤ ((i : ι) → β i)) y) ≤ edist x y

Tactic:
simpa only [ENNReal.coe_one, one_mul] using lipschitzWith_equiv ∞ β x y

Result:
no goals

Proof state:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
x y : WithLp ⊤ ((i : ι) → β i)
⊢ edist x y ≤ edist ((WithLp.equiv ⊤ ((i : ι) → β i)) x) ((WithLp.equiv ⊤ ((i : ι) → β i)) y)

Tactic:
simpa only [ENNReal.div_top, ENNReal.zero_toReal, NNReal.rpow_zero, ENNReal.coe_one,
  one_mul] using antilipschitzWith_equiv ∞ β x y

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Defs.lean
@[simp] lemma nilpotencyClass_zero [Nontrivial R] :
    nilpotencyClass (0 : R) = 1 :=
  nilpotencyClass_eq_succ_iff.mpr <| by constructor <;> simp

Proof state:
R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
⊢ 0 ^ (0 + 1) = 0 ∧ 0 ^ 0 ≠ 0

Tactic:
constructor <;> simp

Result:
no goals
-- Mathlib/Data/Nat/BitIndices.lean
theorem bitIndices_two_pow (k : ℕ) : bitIndices (2^k) = [k]

Proof state:
k : ℕ
⊢ map (fun x => x + k) (bitIndices 1) = [k]

Tactic:
simp

Result:
no goals

Proof state:
k : ℕ
⊢ (2 ^ k).bitIndices = [k]

Tactic:
rw [← mul_one (a := 2^k), bitIndices_two_pow_mul]

Result:
k : ℕ
⊢ map (fun x => x + k) (bitIndices 1) = [k]
-- Mathlib/Algebra/Order/Sub/Unbundled/Hom.lean
theorem AddHom.le_map_tsub [Preorder β] [Add β] [Sub β] [OrderedSub β] (f : AddHom α β)
    (hf : Monotone f) (a b : α) : f a - f b ≤ f (a - b)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : Add α
inst✝⁵ : Sub α
inst✝⁴ : OrderedSub α
inst✝³ : Preorder β
inst✝² : Add β
inst✝¹ : Sub β
inst✝ : OrderedSub β
f : α →ₙ+ β
hf : Monotone ⇑f
a b : α
⊢ f a ≤ f (a - b + b)

Tactic:
exact hf le_tsub_add

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : Add α
inst✝⁵ : Sub α
inst✝⁴ : OrderedSub α
inst✝³ : Preorder β
inst✝² : Add β
inst✝¹ : Sub β
inst✝ : OrderedSub β
f : α →ₙ+ β
hf : Monotone ⇑f
a b : α
⊢ f a - f b ≤ f (a - b)

Tactic:
rw [tsub_le_iff_right, ← f.map_add]

Result:
α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : Add α
inst✝⁵ : Sub α
inst✝⁴ : OrderedSub α
inst✝³ : Preorder β
inst✝² : Add β
inst✝¹ : Sub β
inst✝ : OrderedSub β
f : α →ₙ+ β
hf : Monotone ⇑f
a b : α
⊢ f a ≤ f (a - b + b)
-- Mathlib/SetTheory/Cardinal/ENat.lean
@[simp]
lemma range_ofENat : range ofENat = Iic ℵ₀

Proof state:
x : Cardinal.{u_1}
hx : x ≤ ℵ₀
⊢ x ∈ range ofENat

Tactic:
rcases hx.lt_or_eq with hlt | rfl

Result:
case inl
x : Cardinal.{u_1}
hx : x ≤ ℵ₀
hlt : x < ℵ₀
⊢ x ∈ range ofENat

case inr
hx : ℵ₀ ≤ ℵ₀
⊢ ℵ₀ ∈ range ofENat

Proof state:
case inr
hx : ℵ₀ ≤ ℵ₀
⊢ ℵ₀ ∈ range ofENat

Tactic:
exact mem_range_self (⊤ : ℕ∞)

Result:
no goals

Proof state:
case inl
x : Cardinal.{u_1}
hx : x ≤ ℵ₀
hlt : x < ℵ₀
⊢ x ∈ range ofENat

Tactic:
lift x to ℕ using hlt

Result:
case inl.intro
x : ℕ
hx : ↑x ≤ ℵ₀
⊢ ↑x ∈ range ofENat

Proof state:
⊢ range ofENat = Iic ℵ₀

Tactic:
refine (range_subset_iff.2 ofENat_le_aleph0).antisymm fun x (hx : x ≤ ℵ₀) ↦ ?_

Result:
x : Cardinal.{u_1}
hx : x ≤ ℵ₀
⊢ x ∈ range ofENat

Proof state:
case inl.intro
x : ℕ
hx : ↑x ≤ ℵ₀
⊢ ↑x ∈ range ofENat

Tactic:
exact mem_range_self (x : ℕ∞)

Result:
no goals
-- Mathlib/Algebra/Category/Grp/EpiMono.lean
theorem epi_iff_surjective : Epi f ↔ Function.Surjective f

Proof state:
A B : AddGrp
f : A ⟶ B
e' : Epi f
⊢ Epi (groupAddGroupEquivalence.inverse.map f)

Tactic:
apply groupAddGroupEquivalence.inverse.map_epi

Result:
no goals

Proof state:
A B : AddGrp
f : A ⟶ B
⊢ Epi f ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
have i1 : Epi f ↔ Epi (groupAddGroupEquivalence.inverse.map f) := by
  refine ⟨?_, groupAddGroupEquivalence.inverse.epi_of_epi_map⟩
  intro e'
  apply groupAddGroupEquivalence.inverse.map_epi

Result:
A B : AddGrp
f : A ⟶ B
i1 : Epi f ↔ Epi (groupAddGroupEquivalence.inverse.map f)
⊢ Epi f ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Proof state:
A B : AddGrp
f : A ⟶ B
⊢ Epi f → Epi (groupAddGroupEquivalence.inverse.map f)

Tactic:
intro e'

Result:
A B : AddGrp
f : A ⟶ B
e' : Epi f
⊢ Epi (groupAddGroupEquivalence.inverse.map f)

Proof state:
A B : AddGrp
f : A ⟶ B
⊢ Epi f ↔ Epi (groupAddGroupEquivalence.inverse.map f)

Tactic:
refine ⟨?_, groupAddGroupEquivalence.inverse.epi_of_epi_map⟩

Result:
A B : AddGrp
f : A ⟶ B
⊢ Epi f → Epi (groupAddGroupEquivalence.inverse.map f)

Proof state:
A B : AddGrp
f : A ⟶ B
i1 : Epi f ↔ Epi (groupAddGroupEquivalence.inverse.map f)
⊢ Epi f ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
rwa [Grp.epi_iff_surjective] at i1

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ENat.lean
@[simp] lemma ofENat_le_lift {x : Cardinal.{v}} {m : ℕ∞} : m ≤ lift.{u} x ↔ m ≤ x

Proof state:
x : Cardinal.{v}
m : ℕ∞
⊢ ↑m ≤ lift.{u, v} x ↔ ↑m ≤ x

Tactic:
rw [← lift_ofENat.{u, v}, lift_le]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean
lemma HasAffineProperty.affineAnd_le_affineAnd {P P' : MorphismProperty Scheme.{u}}
    (hP : HasAffineProperty P (affineAnd Q)) (hP' : HasAffineProperty P' (affineAnd Q'))
    (hQQ' : ∀ {R S : Type u} [CommRing R] [CommRing S] {f : R →+* S}, Q f → Q' f) :
    P ≤ P'

Proof state:
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P P' : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
hP' : HasAffineProperty P' (affineAnd fun {R S} [CommRing R] [CommRing S] => Q')
hQQ' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, Q f → Q' f
⊢ P ≤ P'

Tactic:
rw [HasAffineProperty.eq_targetAffineLocally (P := P),
  HasAffineProperty.eq_targetAffineLocally (P := P')]

Result:
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P P' : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
hP' : HasAffineProperty P' (affineAnd fun {R S} [CommRing R] [CommRing S] => Q')
hQQ' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, Q f → Q' f
⊢ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] => Q) ≤
    targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] => Q')

Proof state:
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P P' : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] => Q)
hP' : HasAffineProperty P' (affineAnd fun {R S} [CommRing R] [CommRing S] => Q')
hQQ' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, Q f → Q' f
⊢ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] => Q) ≤
    targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] => Q')

Tactic:
exact targetAffineLocally_affineAnd_le hQQ'

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
theorem two_mul_arctan_sub_pi {x : ℝ} (h : x < -1) :
    2 * arctan x = arctan (2 * x / (1 - x ^ 2)) - π

Proof state:
x : ℝ
h : x < -1
⊢ x < 0

Tactic:
linarith

Result:
no goals

Proof state:
x : ℝ
h : x < -1
⊢ 1 < x * x

Tactic:
nlinarith

Result:
no goals

Proof state:
x : ℝ
h : x < -1
⊢ 2 * arctan x = arctan (2 * x / (1 - x ^ 2)) - π

Tactic:
rw [two_mul, arctan_add_eq_sub_pi (by nlinarith) (by linarith)]

Result:
x : ℝ
h : x < -1
⊢ arctan ((x + x) / (1 - x * x)) - π = arctan (2 * x / (1 - x ^ 2)) - π

Proof state:
x : ℝ
h : x < -1
⊢ arctan ((x + x) / (1 - x * x)) - π = arctan (2 * x / (1 - x ^ 2)) - π

Tactic:
congr 2

Result:
case e_a.e_x
x : ℝ
h : x < -1
⊢ (x + x) / (1 - x * x) = 2 * x / (1 - x ^ 2)

Proof state:
case e_a.e_x
x : ℝ
h : x < -1
⊢ (x + x) / (1 - x * x) = 2 * x / (1 - x ^ 2)

Tactic:
ring

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey!_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α]
    [Inhabited α] (h : m.WF) {l : List α} {k : α} :
    k ∈ m → getKey! (insertManyIfNewUnit m l) k = getKey! m k

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
m : Raw α fun x => Unit
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.WF
l : List α
k : α
⊢ k ∈ m → (insertManyIfNewUnit m l).getKey! k = m.getKey! k

Tactic:
simp only [mem_iff_contains]

Result:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
m : Raw α fun x => Unit
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.WF
l : List α
k : α
⊢ m.contains k = true → (insertManyIfNewUnit m l).getKey! k = m.getKey! k

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
m : Raw α fun x => Unit
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.WF
l : List α
k : α
⊢ m.contains k = true → (insertManyIfNewUnit m l).getKey! k = m.getKey! k

Tactic:
simp_to_raw using Raw₀.Const.getKey!_insertManyIfNewUnit_list_of_contains

Result:
no goals
-- Mathlib/Topology/Algebra/Support.lean
theorem _root_.hasCompactMulSupport_comp_left (hg : ∀ {x}, g x = 1 ↔ x = 1) :
    HasCompactMulSupport (g ∘ f) ↔ HasCompactMulSupport f

Proof state:
α : Type u_2
β : Type u_4
γ : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : One β
inst✝ : One γ
g : β → γ
f : α → β
hg : ∀ {x : β}, g x = 1 ↔ x = 1
⊢ HasCompactMulSupport (g ∘ f) ↔ HasCompactMulSupport f

Tactic:
simp_rw [hasCompactMulSupport_def, mulSupport_comp_eq g (@hg) f]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem reverse_eq_empty_iff {xs : Array α} : xs.reverse = #[] ↔ xs = #[]

Proof state:
α : Type u_1
xs : Array α
⊢ xs.reverse = #[] ↔ xs = #[]

Tactic:
cases xs

Result:
case mk
α : Type u_1
toList✝ : List α
⊢ { toList := toList✝ }.reverse = #[] ↔ { toList := toList✝ } = #[]

Proof state:
case mk
α : Type u_1
toList✝ : List α
⊢ { toList := toList✝ }.reverse = #[] ↔ { toList := toList✝ } = #[]

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem countP_flatMap (p : β → Bool) (l : Vector α n) (f : α → Vector β m) :
    countP p (l.flatMap f) = (map (countP p ∘ f) l).sum

Proof state:
α : Type u_2
β : Type u_1
n m : Nat
p : β → Bool
l : Vector α n
f : α → Vector β m
⊢ countP p (l.flatMap f) = (map (countP p ∘ f) l).sum

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_2
β : Type u_1
m : Nat
p : β → Bool
f : α → Vector β m
l : Array α
⊢ countP p ({ toArray := l, size_toArray := ⋯ }.flatMap f) =
    (map (countP p ∘ f) { toArray := l, size_toArray := ⋯ }).sum

Proof state:
case mk
α : Type u_2
β : Type u_1
m : Nat
p : β → Bool
f : α → Vector β m
l : Array α
⊢ countP p ({ toArray := l, size_toArray := ⋯ }.flatMap f) =
    (map (countP p ∘ f) { toArray := l, size_toArray := ⋯ }).sum

Tactic:
simp [Array.countP_flatMap, Function.comp_def]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Sphere.lean
theorem two_zsmul_oangle_center_add_two_zsmul_oangle_eq_pi {s : Sphere P} {p₁ p₂ p₃ : P}
    (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) (hp₂p₁ : p₂ ≠ p₁) (hp₂p₃ : p₂ ≠ p₃)
    (hp₁p₃ : p₁ ≠ p₃) : (2 : ℤ) • ∡ p₃ p₁ s.center + (2 : ℤ) • ∡ p₁ p₂ p₃ = π

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hp₁p₃ : p₁ ≠ p₃
⊢ 2 • ∡ p₃ p₁ s.center + 2 • ∡ p₁ p₂ p₃ = ↑π

Tactic:
rw [← oangle_center_eq_two_zsmul_oangle hp₁ hp₂ hp₃ hp₂p₁ hp₂p₃,
  oangle_eq_pi_sub_two_zsmul_oangle_center_right hp₁ hp₃ hp₁p₃, add_sub_cancel]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem neg_add_lt_left_of_lt_add {a b c : Int} (h : a < b + c) : -b + a < c

Proof state:
a b c : Int
h : a < b + c
⊢ -b + a < c

Tactic:
rw [Int.add_comm]

Result:
a b c : Int
h : a < b + c
⊢ a + -b < c

Proof state:
a b c : Int
h : a < b + c
⊢ a + -b < c

Tactic:
exact Int.sub_left_lt_of_lt_add h

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem trailingDegree_mul' (h : p.trailingCoeff * q.trailingCoeff ≠ 0) :
    (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).trailingDegree ≤ ↑(p.natTrailingDegree + q.natTrailingDegree)

Tactic:
apply trailingDegree_le_of_ne_zero

Result:
case h
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).coeff (p.natTrailingDegree + q.natTrailingDegree) ≠ 0

Proof state:
case h
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).coeff (p.natTrailingDegree + q.natTrailingDegree) ≠ 0

Tactic:
rwa [coeff_mul_natTrailingDegree_add_natTrailingDegree]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q = 0
⊢ p.trailingCoeff * q.trailingCoeff = 0

Tactic:
rw [hq, trailingCoeff_zero, mul_zero]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p = 0
⊢ p.trailingCoeff * q.trailingCoeff = 0

Tactic:
rw [hp, trailingCoeff_zero, zero_mul]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).trailingDegree ≤ p.trailingDegree + q.trailingDegree

Tactic:
rw [trailingDegree_eq_natTrailingDegree hp, trailingDegree_eq_natTrailingDegree hq, ←
  ENat.coe_add]

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).trailingDegree ≤ ↑(p.natTrailingDegree + q.natTrailingDegree)

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Tactic:
have hq : q ≠ 0 := fun hq => h (by rw [hq, trailingCoeff_zero, mul_zero])

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Tactic:
have hp : p ≠ 0 := fun hp => h (by rw [hp, trailingCoeff_zero, zero_mul])

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree

Tactic:
refine le_antisymm ?_ le_trailingDegree_mul

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).trailingDegree ≤ p.trailingDegree + q.trailingDegree