harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
lemma map_injective (hf : Function.Injective f) : Function.Injective <| map W f :=
  (injective_iff_map_eq_zero _).mpr fun y hy => by
    obtain ⟨p, q, rfl⟩ := exists_smul_basis_eq y
    simp_rw [map_add, CoordinateRing.map_smul, map_one, map_mk, map_X] at hy
    obtain ⟨hp, hq⟩ := smul_basis_eq_zero hy
    rw [Polynomial.map_eq_zero_iff hf] at hp hq
    simp_rw [hp, hq, zero_smul, add_zero]

Proof state:
case intro.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
W : Affine R
f : R →+* S
hf : Function.Injective ⇑f
p q : R[X]
hy : Polynomial.map f p • 1 + Polynomial.map f q • (mk (WeierstrassCurve.map W f)) Y = 0
hp : Polynomial.map f p = 0
hq : Polynomial.map f q = 0
⊢ p • 1 + q • (mk W) Y = 0

Tactic:
rw [Polynomial.map_eq_zero_iff hf] at hp hq

Result:
case intro.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
W : Affine R
f : R →+* S
hf : Function.Injective ⇑f
p q : R[X]
hy : Polynomial.map f p • 1 + Polynomial.map f q • (mk (WeierstrassCurve.map W f)) Y = 0
hp : p = 0
hq : q = 0
⊢ p • 1 + q • (mk W) Y = 0

Proof state:
case intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
W : Affine R
f : R →+* S
hf : Function.Injective ⇑f
p q : R[X]
hy : (map W f) (p • 1 + q • (mk W) Y) = 0
⊢ p • 1 + q • (mk W) Y = 0

Tactic:
simp_rw [map_add, CoordinateRing.map_smul, map_one, map_mk, map_X] at hy

Result:
case intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
W : Affine R
f : R →+* S
hf : Function.Injective ⇑f
p q : R[X]
hy : Polynomial.map f p • 1 + Polynomial.map f q • (mk (WeierstrassCurve.map W f)) Y = 0
⊢ p • 1 + q • (mk W) Y = 0

Proof state:
case intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
W : Affine R
f : R →+* S
hf : Function.Injective ⇑f
p q : R[X]
hy : Polynomial.map f p • 1 + Polynomial.map f q • (mk (WeierstrassCurve.map W f)) Y = 0
⊢ p • 1 + q • (mk W) Y = 0

Tactic:
obtain ⟨hp, hq⟩ := smul_basis_eq_zero hy

Result:
case intro.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
W : Affine R
f : R →+* S
hf : Function.Injective ⇑f
p q : R[X]
hy : Polynomial.map f p • 1 + Polynomial.map f q • (mk (WeierstrassCurve.map W f)) Y = 0
hp : Polynomial.map f p = 0
hq : Polynomial.map f q = 0
⊢ p • 1 + q • (mk W) Y = 0

Proof state:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
W : Affine R
f : R →+* S
hf : Function.Injective ⇑f
y : W.CoordinateRing
hy : (map W f) y = 0
⊢ y = 0

Tactic:
obtain ⟨p, q, rfl⟩ := exists_smul_basis_eq y

Result:
case intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
W : Affine R
f : R →+* S
hf : Function.Injective ⇑f
p q : R[X]
hy : (map W f) (p • 1 + q • (mk W) Y) = 0
⊢ p • 1 + q • (mk W) Y = 0

Proof state:
case intro.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
W : Affine R
f : R →+* S
hf : Function.Injective ⇑f
p q : R[X]
hy : Polynomial.map f p • 1 + Polynomial.map f q • (mk (WeierstrassCurve.map W f)) Y = 0
hp : p = 0
hq : q = 0
⊢ p • 1 + q • (mk W) Y = 0

Tactic:
simp_rw [hp, hq, zero_smul, add_zero]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem Pairwise.chain (p : Pairwise R (a :: l)) : Chain R a l

Proof state:
α✝ : Type u_1
R : α✝ → α✝ → Prop
a : α✝
l : List α✝
p : Pairwise R (a :: l)
r : ∀ (a' : α✝), a' ∈ l → R a a'
p' : Pairwise R l
⊢ Chain R a l

Tactic:
clear p

Result:
α✝ : Type u_1
R : α✝ → α✝ → Prop
a : α✝
l : List α✝
r : ∀ (a' : α✝), a' ∈ l → R a a'
p' : Pairwise R l
⊢ Chain R a l

Proof state:
case cons
α✝ : Type u_1
R : α✝ → α✝ → Prop
l✝ : List α✝
b : α✝
l : List α✝
r' : ∀ (a' : α✝), a' ∈ l → R b a'
a✝ : Pairwise R l
IH : ∀ {a : α✝}, (∀ (a' : α✝), a' ∈ l → R a a') → Chain R a l
a : α✝
r : ∀ (a' : α✝), a' ∈ b :: l → R a a'
⊢ Chain R a (b :: l)

Tactic:
simp only [chain_cons, forall_mem_cons] at r

Result:
case cons
α✝ : Type u_1
R : α✝ → α✝ → Prop
l✝ : List α✝
b : α✝
l : List α✝
r' : ∀ (a' : α✝), a' ∈ l → R b a'
a✝ : Pairwise R l
IH : ∀ {a : α✝}, (∀ (a' : α✝), a' ∈ l → R a a') → Chain R a l
a : α✝
r : R a b ∧ ∀ (x : α✝), x ∈ l → R a x
⊢ Chain R a (b :: l)

Proof state:
α✝ : Type u_1
R : α✝ → α✝ → Prop
a : α✝
l : List α✝
p : Pairwise R (a :: l)
⊢ Chain R a l

Tactic:
let ⟨r, p'⟩ := pairwise_cons.1 p

Result:
α✝ : Type u_1
R : α✝ → α✝ → Prop
a : α✝
l : List α✝
p : Pairwise R (a :: l)
r : ∀ (a' : α✝), a' ∈ l → R a a'
p' : Pairwise R l
⊢ Chain R a l

Proof state:
α✝ : Type u_1
R : α✝ → α✝ → Prop
a : α✝
l : List α✝
r : ∀ (a' : α✝), a' ∈ l → R a a'
p' : Pairwise R l
⊢ Chain R a l

Tactic:
induction p' generalizing a with
| nil => exact Chain.nil
| @cons b l r' _ IH =>
  simp only [chain_cons, forall_mem_cons] at r
  exact chain_cons.2 ⟨r.1, IH r'⟩

Result:
no goals

Proof state:
case nil
α✝ : Type u_1
R : α✝ → α✝ → Prop
l : List α✝
a : α✝
r : ∀ (a' : α✝), a' ∈ [] → R a a'
⊢ Chain R a []

Tactic:
exact Chain.nil

Result:
no goals

Proof state:
case cons
α✝ : Type u_1
R : α✝ → α✝ → Prop
l✝ : List α✝
b : α✝
l : List α✝
r' : ∀ (a' : α✝), a' ∈ l → R b a'
a✝ : Pairwise R l
IH : ∀ {a : α✝}, (∀ (a' : α✝), a' ∈ l → R a a') → Chain R a l
a : α✝
r : R a b ∧ ∀ (x : α✝), x ∈ l → R a x
⊢ Chain R a (b :: l)

Tactic:
exact chain_cons.2 ⟨r.1, IH r'⟩

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Radical.lean
theorem comap_jacobson_of_ker_le (surj : Function.Surjective f)
    (le : LinearMap.ker f ≤ jacobson R M) :
    comap f (jacobson R₂ M₂) = jacobson R M

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : Ring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
F : Type u_5
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
surj : Function.Surjective ⇑f
le : LinearMap.ker f ≤ jacobson R M
⊢ comap f (jacobson R₂ M₂) = jacobson R M

Tactic:
rw [← map_jacobson_of_ker_le surj le, comap_map_eq_self le]

Result:
no goals
-- Mathlib/Order/WellFoundedSet.lean
theorem PartiallyWellOrderedOn.wellFoundedOn [IsPreorder α r] (h : s.PartiallyWellOrderedOn r) :
    s.WellFoundedOn fun a b => r a b ∧ ¬r b a

Proof state:
α : Type u_2
r : α → α → Prop
s : Set α
inst✝ : IsPreorder α r
this : Preorder α := Preorder.mk ⋯ ⋯ ⋯
h : s.PartiallyWellOrderedOn fun x1 x2 => x1 ≤ x2
⊢ ∀ (f : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 < x2), ¬∀ (n : ℕ), f n ∈ s

Tactic:
intro f hf

Result:
α : Type u_2
r : α → α → Prop
s : Set α
inst✝ : IsPreorder α r
this : Preorder α := Preorder.mk ⋯ ⋯ ⋯
h : s.PartiallyWellOrderedOn fun x1 x2 => x1 ≤ x2
f : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 < x2
hf : ∀ (n : ℕ), f n ∈ s
⊢ False

Proof state:
case intro.intro.intro
α : Type u_2
r : α → α → Prop
s : Set α
inst✝ : IsPreorder α r
this : Preorder α := Preorder.mk ⋯ ⋯ ⋯
h : s.PartiallyWellOrderedOn fun x1 x2 => x1 ≤ x2
f : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 < x2
hf : ∀ (n : ℕ), f n ∈ s
m n : ℕ
hlt : m < n
hle : f m ≤ f n
⊢ False

Tactic:
exact (f.map_rel_iff.2 hlt).not_le hle

Result:
no goals

Proof state:
α : Type u_2
r : α → α → Prop
s : Set α
inst✝ : IsPreorder α r
h : s.PartiallyWellOrderedOn r
⊢ s.WellFoundedOn fun a b => r a b ∧ ¬r b a

Tactic:
letI : Preorder α :=
  { le := r
    le_refl := refl_of r
    le_trans := fun _ _ _ => trans_of r }

Result:
α : Type u_2
r : α → α → Prop
s : Set α
inst✝ : IsPreorder α r
h : s.PartiallyWellOrderedOn r
this : Preorder α := Preorder.mk ⋯ ⋯ ⋯
⊢ s.WellFoundedOn fun a b => r a b ∧ ¬r b a

Proof state:
α : Type u_2
r : α → α → Prop
s : Set α
inst✝ : IsPreorder α r
this : Preorder α := Preorder.mk ⋯ ⋯ ⋯
h : s.PartiallyWellOrderedOn fun x1 x2 => x1 ≤ x2
f : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 < x2
hf : ∀ (n : ℕ), f n ∈ s
⊢ False

Tactic:
obtain ⟨m, n, hlt, hle⟩ := h f hf

Result:
case intro.intro.intro
α : Type u_2
r : α → α → Prop
s : Set α
inst✝ : IsPreorder α r
this : Preorder α := Preorder.mk ⋯ ⋯ ⋯
h : s.PartiallyWellOrderedOn fun x1 x2 => x1 ≤ x2
f : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 < x2
hf : ∀ (n : ℕ), f n ∈ s
m n : ℕ
hlt : m < n
hle : f m ≤ f n
⊢ False

Proof state:
α : Type u_2
r : α → α → Prop
s : Set α
inst✝ : IsPreorder α r
this : Preorder α := Preorder.mk ⋯ ⋯ ⋯
h : s.PartiallyWellOrderedOn fun x1 x2 => x1 ≤ x2
⊢ s.WellFoundedOn fun x1 x2 => x1 < x2

Tactic:
rw [wellFoundedOn_iff_no_descending_seq]

Result:
α : Type u_2
r : α → α → Prop
s : Set α
inst✝ : IsPreorder α r
this : Preorder α := Preorder.mk ⋯ ⋯ ⋯
h : s.PartiallyWellOrderedOn fun x1 x2 => x1 ≤ x2
⊢ ∀ (f : (fun x1 x2 => x1 > x2) ↪r fun x1 x2 => x1 < x2), ¬∀ (n : ℕ), f n ∈ s
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem monomial_sub (n : ℕ) : monomial n (a - b) = monomial n a - monomial n b

Proof state:
R : Type u
a b : R
inst✝ : Ring R
n : ℕ
⊢ (monomial n) (a - b) = (monomial n) a - (monomial n) b

Tactic:
rw [sub_eq_add_neg, monomial_add, monomial_neg, sub_eq_add_neg]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem normalize_eq_zero (d0 : d ≠ 0) : normalize n d d0 = 0 ↔ n = 0

Proof state:
case refine'_3
d : Nat
n : Int
d0 : d ≠ 0
this : normalize ?refine'_1 d d0 = normalize ?refine'_2 1 Nat.one_ne_zero ↔ ?refine'_1 * ↑1 = ?refine'_2 * ↑d
⊢ normalize n d d0 = 0 ↔ n = 0

case refine'_1
d : Nat
n : Int
d0 : d ≠ 0
⊢ Int

case refine'_2
d : Nat
n : Int
d0 : d ≠ 0
⊢ Int

Tactic:
rw [normalize_zero (d := 1)] at this

Result:
case refine'_3
d : Nat
n : Int
d0 : d ≠ 0
this : normalize ?refine'_1 d d0 = 0 ↔ ?refine'_1 * ↑1 = 0 * ↑d
⊢ normalize n d d0 = 0 ↔ n = 0

case refine'_1
d : Nat
n : Int
d0 : d ≠ 0
⊢ Int

Proof state:
d : Nat
n : Int
d0 : d ≠ 0
⊢ normalize n d d0 = 0 ↔ n = 0

Tactic:
have' := normalize_eq_iff d0 Nat.one_ne_zero

Result:
case refine'_3
d : Nat
n : Int
d0 : d ≠ 0
this : normalize ?refine'_1 d d0 = normalize ?refine'_2 1 Nat.one_ne_zero ↔ ?refine'_1 * ↑1 = ?refine'_2 * ↑d
⊢ normalize n d d0 = 0 ↔ n = 0

case refine'_1
d : Nat
n : Int
d0 : d ≠ 0
⊢ Int

case refine'_2
d : Nat
n : Int
d0 : d ≠ 0
⊢ Int

Proof state:
case refine'_3
d : Nat
n : Int
d0 : d ≠ 0
this : normalize n d d0 = 0 ↔ n * ↑1 = 0 * ↑d
⊢ n * ↑1 = 0 * ↑d ↔ n = 0

Tactic:
simp

Result:
no goals

Proof state:
case refine'_3
d : Nat
n : Int
d0 : d ≠ 0
this : normalize ?refine'_1 d d0 = 0 ↔ ?refine'_1 * ↑1 = 0 * ↑d
⊢ normalize n d d0 = 0 ↔ n = 0

case refine'_1
d : Nat
n : Int
d0 : d ≠ 0
⊢ Int

Tactic:
rw [this]

Result:
case refine'_3
d : Nat
n : Int
d0 : d ≠ 0
this : normalize n d d0 = 0 ↔ n * ↑1 = 0 * ↑d
⊢ n * ↑1 = 0 * ↑d ↔ n = 0
-- Mathlib/Data/Int/Basic.lean
@[norm_cast] lemma natCast_dvd_natCast {m n : ℕ} : (↑m : ℤ) ∣ ↑n ↔ m ∣ n where
  mp

Proof state:
case intro.inr
m n : ℕ
a : ℤ
h : ↑n = ↑m * a
hm : m > 0
⊢ m ∣ n

Tactic:
have ha : 0 ≤ a := Int.not_lt.1 fun ha ↦ by
  simpa [← h, Int.not_lt.2 (Int.natCast_nonneg _)]
    using Int.mul_neg_of_pos_of_neg (natCast_pos.2 hm) ha

Result:
case intro.inr
m n : ℕ
a : ℤ
h : ↑n = ↑m * a
hm : m > 0
ha : 0 ≤ a
⊢ m ∣ n

Proof state:
m n : ℕ
a : ℤ
h : ↑n = ↑m * a
hm : m > 0
ha : a < 0
⊢ False

Tactic:
simpa [← h, Int.not_lt.2 (Int.natCast_nonneg _)]
  using Int.mul_neg_of_pos_of_neg (natCast_pos.2 hm) ha

Result:
no goals

Proof state:
m n : ℕ
⊢ ↑m ∣ ↑n → m ∣ n

Tactic:
rintro ⟨a, h⟩

Result:
case intro
m n : ℕ
a : ℤ
h : ↑n = ↑m * a
⊢ m ∣ n

Proof state:
case intro.inr
m n : ℕ
a : ℤ
h : ↑n = ↑m * a
hm : m > 0
ha : 0 ≤ a
⊢ m ∣ n

Tactic:
lift a to ℕ using ha

Result:
case intro.inr.intro
m n : ℕ
hm : m > 0
a : ℕ
h : ↑n = ↑m * ↑a
⊢ m ∣ n

Proof state:
m n : ℕ
⊢ m ∣ n → ↑m ∣ ↑n

Tactic:
rintro ⟨a, rfl⟩

Result:
case intro
m a : ℕ
⊢ ↑m ∣ ↑(m * a)

Proof state:
case intro.inl
n : ℕ
a : ℤ
h : ↑n = ↑0 * a
⊢ 0 ∣ n

Tactic:
simpa using h

Result:
no goals

Proof state:
case intro
m n : ℕ
a : ℤ
h : ↑n = ↑m * a
⊢ m ∣ n

Tactic:
obtain rfl | hm := m.eq_zero_or_pos

Result:
case intro.inl
n : ℕ
a : ℤ
h : ↑n = ↑0 * a
⊢ 0 ∣ n

case intro.inr
m n : ℕ
a : ℤ
h : ↑n = ↑m * a
hm : m > 0
⊢ m ∣ n

Proof state:
case intro.inr.intro
m n : ℕ
hm : m > 0
a : ℕ
h : n = m * a
⊢ m ∣ n

Tactic:
exact ⟨a, h⟩

Result:
no goals

Proof state:
case intro
m a : ℕ
⊢ ↑m ∣ ↑(m * a)

Tactic:
simp [Int.dvd_mul_right]

Result:
no goals

Proof state:
case intro.inr.intro
m n : ℕ
hm : m > 0
a : ℕ
h : ↑n = ↑m * ↑a
⊢ m ∣ n

Tactic:
norm_cast at h

Result:
case intro.inr.intro
m n : ℕ
hm : m > 0
a : ℕ
h : n = m * a
⊢ m ∣ n
-- Mathlib/GroupTheory/Commutator/Finite.lean
lemma index_center_le_pow : (center G).index ≤ Nat.card (commutatorSet G) ^ Group.rank G

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : Group.FG G
inst✝ : Finite ↑(commutatorSet G)
⊢ (center G).index ≤ Nat.card ↑(commutatorSet G) ^ Group.rank G

Tactic:
obtain ⟨S, hS1, hS2⟩ := Group.rank_spec G

Result:
case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : Group.FG G
inst✝ : Finite ↑(commutatorSet G)
S : Finset G
hS1 : S.card = Group.rank G
hS2 : closure ↑S = ⊤
⊢ (center G).index ≤ Nat.card ↑(commutatorSet G) ^ Group.rank G

Proof state:
case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : Group.FG G
inst✝ : Finite ↑(commutatorSet G)
S : Finset G
hS1 : S.card = Group.rank G
hS2 : closure ↑S = ⊤
⊢ (center G).index ≤ Nat.card ↑(commutatorSet G) ^ Group.rank G

Tactic:
rw [← hS1, ← Fintype.card_coe, ← Nat.card_eq_fintype_card, ← Finset.coe_sort_coe, ← Nat.card_fun]

Result:
case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : Group.FG G
inst✝ : Finite ↑(commutatorSet G)
S : Finset G
hS1 : S.card = Group.rank G
hS2 : closure ↑S = ⊤
⊢ (center G).index ≤ Nat.card (↑↑S → ↑(commutatorSet G))

Proof state:
case intro.intro
G : Type u_1
inst✝² : Group G
inst✝¹ : Group.FG G
inst✝ : Finite ↑(commutatorSet G)
S : Finset G
hS1 : S.card = Group.rank G
hS2 : closure ↑S = ⊤
⊢ (center G).index ≤ Nat.card (↑↑S → ↑(commutatorSet G))

Tactic:
exact Finite.card_le_of_embedding (quotientCenterEmbedding hS2)

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem b₄_of_isCharTwoJEqZeroNF_of_char_two : W.b₄ = 0

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJEqZeroNF
inst✝ : CharP R 2
⊢ W.b₄ = 0

Tactic:
rw [b₄_of_isCharTwoJEqZeroNF]

Result:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJEqZeroNF
inst✝ : CharP R 2
⊢ 2 * W.a₄ = 0

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJEqZeroNF
inst✝ : CharP R 2
⊢ 2 * W.a₄ = 0

Tactic:
linear_combination W.a₄ * CharP.cast_eq_zero R 2

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Basic.lean
theorem tsub_lt_self_iff (ha : AddLECancellable a) : a - b < a ↔ 0 < a ∧ 0 < b

Proof state:
α : Type u_1
inst✝³ : LinearOrderedAddCommMonoid α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a : α
ha : AddLECancellable a
h : a - 0 < a
⊢ False

Tactic:
rw [tsub_zero] at h

Result:
α : Type u_1
inst✝³ : LinearOrderedAddCommMonoid α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a : α
ha : AddLECancellable a
h : a < a
⊢ False

Proof state:
α : Type u_1
inst✝³ : LinearOrderedAddCommMonoid α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
ha : AddLECancellable a
⊢ a - b < a ↔ 0 < a ∧ 0 < b

Tactic:
refine
  ⟨fun h => ⟨(zero_le _).trans_lt h, (zero_le b).lt_of_ne ?_⟩, fun h => ha.tsub_lt_self h.1 h.2⟩

Result:
α : Type u_1
inst✝³ : LinearOrderedAddCommMonoid α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
ha : AddLECancellable a
h : a - b < a
⊢ 0 ≠ b

Proof state:
α : Type u_1
inst✝³ : LinearOrderedAddCommMonoid α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
ha : AddLECancellable a
h : a - b < a
⊢ 0 ≠ b

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝³ : LinearOrderedAddCommMonoid α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a : α
ha : AddLECancellable a
h : a - 0 < a
⊢ False

Proof state:
α : Type u_1
inst✝³ : LinearOrderedAddCommMonoid α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a : α
ha : AddLECancellable a
h : a < a
⊢ False

Tactic:
exact h.false

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem Integrable.bdd_mul' {f g : α → 𝕜} {c : ℝ} (hg : Integrable g μ)
    (hf : AEStronglyMeasurable f μ) (hf_bound : ∀ᵐ x ∂μ, ‖f x‖ ≤ c) :
    Integrable (fun x => f x * g x) μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_6
inst✝ : NormedRing 𝕜
f g : α → 𝕜
c : ℝ
hg : Integrable g μ
hf : AEStronglyMeasurable f μ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
⊢ ∀ᵐ (a : α) ∂μ, ‖f a * g a‖ ≤ (c • fun a => ‖g a‖) a

Tactic:
filter_upwards [hf_bound] with x hx

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_6
inst✝ : NormedRing 𝕜
f g : α → 𝕜
c : ℝ
hg : Integrable g μ
hf : AEStronglyMeasurable f μ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
x : α
hx : ‖f x‖ ≤ c
⊢ ‖f x * g x‖ ≤ (c • fun a => ‖g a‖) x

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_6
inst✝ : NormedRing 𝕜
f g : α → 𝕜
c : ℝ
hg : Integrable g μ
hf : AEStronglyMeasurable f μ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
⊢ Integrable (fun x => f x * g x) μ

Tactic:
refine Integrable.mono' (hg.norm.smul c) (hf.mul hg.1) ?_

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_6
inst✝ : NormedRing 𝕜
f g : α → 𝕜
c : ℝ
hg : Integrable g μ
hf : AEStronglyMeasurable f μ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
⊢ ∀ᵐ (a : α) ∂μ, ‖f a * g a‖ ≤ (c • fun a => ‖g a‖) a

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_6
inst✝ : NormedRing 𝕜
f g : α → 𝕜
c : ℝ
hg : Integrable g μ
hf : AEStronglyMeasurable f μ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
x : α
hx : ‖f x‖ ≤ c
⊢ ‖f x * g x‖ ≤ c * ‖g x‖

Tactic:
exact (norm_mul_le _ _).trans (mul_le_mul_of_nonneg_right hx (norm_nonneg _))

Result:
no goals

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_6
inst✝ : NormedRing 𝕜
f g : α → 𝕜
c : ℝ
hg : Integrable g μ
hf : AEStronglyMeasurable f μ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
x : α
hx : ‖f x‖ ≤ c
⊢ ‖f x * g x‖ ≤ (c • fun a => ‖g a‖) x

Tactic:
rw [Pi.smul_apply, smul_eq_mul]

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_6
inst✝ : NormedRing 𝕜
f g : α → 𝕜
c : ℝ
hg : Integrable g μ
hf : AEStronglyMeasurable f μ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
x : α
hx : ‖f x‖ ≤ c
⊢ ‖f x * g x‖ ≤ c * ‖g x‖
-- Mathlib/Analysis/InnerProductSpace/Defs.lean
theorem inner_mul_symm_re_eq_norm (x y : F) : re (⟪x, y⟫ * ⟪y, x⟫) = ‖⟪x, y⟫ * ⟪y, x⟫‖

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ re (⟪x, y⟫_𝕜 * ⟪y, x⟫_𝕜) = ‖⟪x, y⟫_𝕜 * ⟪y, x⟫_𝕜‖

Tactic:
rw [← inner_conj_symm, mul_comm]

Result:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ re (⟪y, x⟫_𝕜 * (starRingEnd 𝕜) ⟪y, x⟫_𝕜) = ‖⟪y, x⟫_𝕜 * (starRingEnd 𝕜) ⟪y, x⟫_𝕜‖

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ re (⟪y, x⟫_𝕜 * (starRingEnd 𝕜) ⟪y, x⟫_𝕜) = ‖⟪y, x⟫_𝕜 * (starRingEnd 𝕜) ⟪y, x⟫_𝕜‖

Tactic:
exact re_eq_norm_of_mul_conj (inner y x)

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Abs.lean
theorem HasStrictFDerivAt.abs_of_neg (hf : HasStrictFDerivAt f f' x)
    (h₀ : f x < 0) : HasStrictFDerivAt (fun x ↦ |f x|) (-f') x

Proof state:
case h.e'_12.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
x : E
hf : HasStrictFDerivAt f f' x
h₀ : f x < 0
y : E
⊢ (-f') y = ((ContinuousLinearMap.smulRight 1 (-1)).comp f') y

Tactic:
simp

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
x : E
hf : HasStrictFDerivAt f f' x
h₀ : f x < 0
⊢ HasStrictFDerivAt (fun x => |f x|) (-f') x

Tactic:
convert (hasStrictDerivAt_abs_neg h₀).hasStrictFDerivAt.comp x hf using 1

Result:
case h.e'_12
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
x : E
hf : HasStrictFDerivAt f f' x
h₀ : f x < 0
⊢ -f' = (ContinuousLinearMap.smulRight 1 (-1)).comp f'

Proof state:
case h.e'_12
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
x : E
hf : HasStrictFDerivAt f f' x
h₀ : f x < 0
⊢ -f' = (ContinuousLinearMap.smulRight 1 (-1)).comp f'

Tactic:
ext y

Result:
case h.e'_12.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
x : E
hf : HasStrictFDerivAt f f' x
h₀ : f x < 0
y : E
⊢ (-f') y = ((ContinuousLinearMap.smulRight 1 (-1)).comp f') y
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Perm.lean
theorem erase_cons_subperm_cons_erase (a b : α) (l : List α) :
    (a :: l).erase b <+~ a :: l.erase b

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
h : ¬a = b
this : ¬(a == b) = true
⊢ (a :: l).erase b <+~ a :: l.erase b

Tactic:
rw [erase_cons_tail this]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
h : a = b
⊢ (a :: l).erase b <+~ a :: l.erase b

Tactic:
rw [h, erase_cons_head]

Result:
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
h : a = b
⊢ l <+~ b :: l.erase b

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
h : a = b
⊢ l <+~ b :: l.erase b

Tactic:
apply subperm_cons_erase

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
h : ¬a = b
⊢ (a :: l).erase b <+~ a :: l.erase b

Tactic:
have : ¬(a == b) = true := by simp only [beq_false_of_ne h, not_false_eq_true, reduceCtorEq]

Result:
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
h : ¬a = b
this : ¬(a == b) = true
⊢ (a :: l).erase b <+~ a :: l.erase b

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
h : ¬a = b
⊢ ¬(a == b) = true

Tactic:
simp only [beq_false_of_ne h, not_false_eq_true, reduceCtorEq]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
⊢ (a :: l).erase b <+~ a :: l.erase b

Tactic:
if h : a = b then
  rw [h, erase_cons_head]; apply subperm_cons_erase
else
  have : ¬(a == b) = true := by simp only [beq_false_of_ne h, not_false_eq_true, reduceCtorEq]
  rw [erase_cons_tail this]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem tprod_range {g : γ → β} (f : β → α) (hg : Injective g) :
    ∏' x : Set.range g, f x = ∏' x, f (g x)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
g : γ → β
f : β → α
hg : Injective g
⊢ ∏' (x : ↑Set.univ), f (g ↑x) = ∏' (x : γ), f (g x)

Tactic:
simp_rw [← comp_apply (g := g), tprod_univ (f ∘ g)]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
g : γ → β
f : β → α
hg : Injective g
⊢ ∏' (x : ↑(Set.range g)), f ↑x = ∏' (x : γ), f (g x)

Tactic:
rw [← Set.image_univ, tprod_image f hg.injOn]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
g : γ → β
f : β → α
hg : Injective g
⊢ ∏' (x : ↑Set.univ), f (g ↑x) = ∏' (x : γ), f (g x)
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem hasLimitOfEquivalenceComp (e : K ≌ J) [HasLimit (e.functor ⋙ F)] : HasLimit F

Proof state:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
e : K ≌ J
inst✝ : HasLimit (e.functor ⋙ F)
this : HasLimit (e.inverse ⋙ e.functor ⋙ F)
⊢ HasLimit F

Tactic:
apply hasLimitOfIso (e.invFunIdAssoc F)

Result:
no goals

Proof state:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
e : K ≌ J
inst✝ : HasLimit (e.functor ⋙ F)
⊢ HasLimit F

Tactic:
haveI : HasLimit (e.inverse ⋙ e.functor ⋙ F) := Limits.hasLimitEquivalenceComp e.symm

Result:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
e : K ≌ J
inst✝ : HasLimit (e.functor ⋙ F)
this : HasLimit (e.inverse ⋙ e.functor ⋙ F)
⊢ HasLimit F