harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Tactic/NormNum/Basic.lean
theorem isRat_sub {α} [Ring α] {f : α → α → α} {a b : α} {na nb nc : ℤ} {da db dc k : ℕ}
    (hf : f = HSub.hSub) (ra : IsRat a na da) (rb : IsRat b nb db)
    (h₁ : Int.sub (Int.mul na db) (Int.mul nb da) = Int.mul k nc)
    (h₂ : Nat.mul da db = Nat.mul k dc) :
    IsRat (f a b) nc dc

Proof state:
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : (na.mul ↑db).sub (nb.mul ↑da) = (↑k).mul nc
h₂ : da.mul db = k.mul dc
⊢ IsRat (a + -b) nc dc

Tactic:
refine isRat_add rfl ra (isRat_neg (n' := -nb) rfl rb rfl) (k := k) (nc := nc) ?_ h₂

Result:
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : (na.mul ↑db).sub (nb.mul ↑da) = (↑k).mul nc
h₂ : da.mul db = k.mul dc
⊢ (na.mul ↑db).add ((-nb).mul ↑da) = (↑k).mul nc

Proof state:
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : (na.mul ↑db).sub (nb.mul ↑da) = (↑k).mul nc
h₂ : da.mul db = k.mul dc
⊢ IsRat (f a b) nc dc

Tactic:
rw [hf, sub_eq_add_neg]

Result:
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : (na.mul ↑db).sub (nb.mul ↑da) = (↑k).mul nc
h₂ : da.mul db = k.mul dc
⊢ IsRat (a + -b) nc dc

Proof state:
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : (na.mul ↑db).sub (nb.mul ↑da) = (↑k).mul nc
h₂ : da.mul db = k.mul dc
⊢ (na.mul ↑db).add (-(nb * ↑da)) = (↑k).mul nc

Tactic:
exact h₁

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : (na.mul ↑db).sub (nb.mul ↑da) = (↑k).mul nc
h₂ : da.mul db = k.mul dc
⊢ (na.mul ↑db).add ((-nb).mul ↑da) = (↑k).mul nc

Tactic:
rw [show Int.mul (-nb) _ = _ from neg_mul ..]

Result:
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : (na.mul ↑db).sub (nb.mul ↑da) = (↑k).mul nc
h₂ : da.mul db = k.mul dc
⊢ (na.mul ↑db).add (-(nb * ↑da)) = (↑k).mul nc
-- Mathlib/Topology/ContinuousMap/ZeroAtInfty.lean
/-- A continuous function on a compact space is automatically a continuous function vanishing at
infinity. This is not an instance to avoid type class loops. -/
lemma zeroAtInftyContinuousMapClass.ofCompact {G : Type*} [FunLike G α β]
    [ContinuousMapClass G α β] [CompactSpace α] : ZeroAtInftyContinuousMapClass G α β where
  map_continuous := map_continuous
  zero_at_infty

Proof state:
α : Type u
β : Type v
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : Zero β
G : Type u_2
inst✝² : FunLike G α β
inst✝¹ : ContinuousMapClass G α β
inst✝ : CompactSpace α
⊢ ∀ (f : G), Tendsto (⇑f) (cocompact α) (𝓝 0)

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem rescale_mul (a b : R) : rescale (a * b) = (rescale b).comp (rescale a)

Proof state:
case a.h
R : Type u_1
inst✝ : CommSemiring R
a b : R
x✝ : R⟦X⟧
n✝ : ℕ
⊢ (coeff R n✝) ((rescale (a * b)) x✝) = (coeff R n✝) (((rescale b).comp (rescale a)) x✝)

Tactic:
simp [← rescale_rescale]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a b : R
⊢ rescale (a * b) = (rescale b).comp (rescale a)

Tactic:
ext

Result:
case a.h
R : Type u_1
inst✝ : CommSemiring R
a b : R
x✝ : R⟦X⟧
n✝ : ℕ
⊢ (coeff R n✝) ((rescale (a * b)) x✝) = (coeff R n✝) (((rescale b).comp (rescale a)) x✝)
-- Mathlib/RingTheory/RingHom/Locally.lean
/-- If `P` is stable under base change, then so is `Locally P`. -/
lemma locally_isStableUnderBaseChange (hPi : RespectsIso P) (hPb : IsStableUnderBaseChange P) :
    IsStableUnderBaseChange (Locally P)

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
hPb : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
hf : Locally (fun {R S} [CommRing R] [CommRing S] => P) (algebraMap R T)
⊢ Locally (fun {R S} [CommRing R] [CommRing S] => P) Algebra.TensorProduct.includeLeftRingHom

Tactic:
obtain ⟨s, hsone, hs⟩ := hf

Result:
case intro.intro
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
hPb : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
s : Set T
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap T (Localization.Away t)).comp (algebraMap R T))
⊢ Locally (fun {R S} [CommRing R] [CommRing S] => P) Algebra.TensorProduct.includeLeftRingHom
-- Mathlib/Data/Set/Card.lean
theorem ncard_diff (hst : s ⊆ t) (hs : s.Finite

Proof state:
case inr
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : autoParam s.Finite _auto✝
ht : t.Infinite
⊢ (t \ s).ncard = t.ncard - s.ncard

Tactic:
rw [ht.ncard, Nat.zero_sub, (ht.diff hs).ncard]

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : autoParam s.Finite _auto✝
⊢ (t \ s).ncard = t.ncard - s.ncard

Tactic:
obtain ht | ht := t.finite_or_infinite

Result:
case inl
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : autoParam s.Finite _auto✝
ht : t.Finite
⊢ (t \ s).ncard = t.ncard - s.ncard

case inr
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : autoParam s.Finite _auto✝
ht : t.Infinite
⊢ (t \ s).ncard = t.ncard - s.ncard

Proof state:
case inl
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : autoParam s.Finite _auto✝
ht : t.Finite
⊢ (t \ s).ncard = t.ncard - s.ncard

Tactic:
rw [← ncard_diff_add_ncard_of_subset hst ht, add_tsub_cancel_right]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem div_le_self_iff (a : α) {b : α} : a / b ≤ a ↔ 1 ≤ b

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b : α
⊢ a / b ≤ a ↔ 1 ≤ b

Tactic:
simp [div_eq_mul_inv]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Ultra.lean
lemma isNonarchimedean_nnnorm {R} [SeminormedAddCommGroup R] [IsUltrametricDist R] :
    IsNonarchimedean (‖·‖₊ : R → ℝ)

Proof state:
R : Type u_4
inst✝¹ : SeminormedAddCommGroup R
inst✝ : IsUltrametricDist R
x y : R
⊢ (fun x => ↑‖x‖₊) (x + y) ≤ (fun x => ↑‖x‖₊) x ⊔ (fun x => ↑‖x‖₊) y

Tactic:
convert dist_triangle_max 0 x (x + y) using 1

Result:
case h.e'_3
R : Type u_4
inst✝¹ : SeminormedAddCommGroup R
inst✝ : IsUltrametricDist R
x y : R
⊢ (fun x => ↑‖x‖₊) (x + y) = dist 0 (x + y)

case h.e'_4
R : Type u_4
inst✝¹ : SeminormedAddCommGroup R
inst✝ : IsUltrametricDist R
x y : R
⊢ (fun x => ↑‖x‖₊) x ⊔ (fun x => ↑‖x‖₊) y = dist 0 x ⊔ dist x (x + y)

Proof state:
case h.e'_3
R : Type u_4
inst✝¹ : SeminormedAddCommGroup R
inst✝ : IsUltrametricDist R
x y : R
⊢ (fun x => ↑‖x‖₊) (x + y) = dist 0 (x + y)

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_4
R : Type u_4
inst✝¹ : SeminormedAddCommGroup R
inst✝ : IsUltrametricDist R
x y : R
⊢ (fun x => ↑‖x‖₊) x ⊔ (fun x => ↑‖x‖₊) y = dist 0 x ⊔ dist x (x + y)

Tactic:
congr <;> simp [SeminormedAddGroup.dist_eq]

Result:
no goals

Proof state:
R : Type u_4
inst✝¹ : SeminormedAddCommGroup R
inst✝ : IsUltrametricDist R
⊢ IsNonarchimedean fun x => ↑‖x‖₊

Tactic:
intro x y

Result:
R : Type u_4
inst✝¹ : SeminormedAddCommGroup R
inst✝ : IsUltrametricDist R
x y : R
⊢ (fun x => ↑‖x‖₊) (x + y) ≤ (fun x => ↑‖x‖₊) x ⊔ (fun x => ↑‖x‖₊) y
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem hasProd_extend_one {g : β → γ} (hg : Injective g) :
    HasProd (extend g f 1) a ↔ HasProd f a

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
g : β → γ
hg : Injective g
⊢ HasProd (extend g f 1) a ↔ HasProd f a

Tactic:
rw [← hg.hasProd_iff, extend_comp hg]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
g : β → γ
hg : Injective g
⊢ ∀ x ∉ Set.range g, extend g f 1 x = 1

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
g : β → γ
hg : Injective g
⊢ ∀ x ∉ Set.range g, extend g f 1 x = 1

Tactic:
exact extend_apply' _ _

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
theorem dist_eq_iff_eq_sq_sinh (hr : 0 ≤ r) :
    dist z w = r ↔ dist (z : ℂ) w ^ 2 / (4 * z.im * w.im) = sinh (r / 2) ^ 2

Proof state:
case hb
z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ sinh (r / 2)

Tactic:
positivity

Result:
no goals

Proof state:
z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ dist ↑z ↑w ^ 2 / (2 ^ 2 * (z.im * w.im)) = sinh (r / 2) ^ 2 ↔ dist ↑z ↑w ^ 2 / (4 * (z.im * w.im)) = sinh (r / 2) ^ 2

Tactic:
norm_num

Result:
no goals

Proof state:
z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ z.im * w.im

case ha
z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ dist ↑z ↑w / (2 * √(z.im * w.im))

case hb
z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ sinh (r / 2)

Tactic:
all_goals positivity

Result:
no goals

Proof state:
z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ dist z w = r ↔ dist ↑z ↑w ^ 2 / (4 * z.im * w.im) = sinh (r / 2) ^ 2

Tactic:
rw [dist_eq_iff_eq_sinh, ← sq_eq_sq₀, div_pow, mul_pow, sq_sqrt, mul_assoc]

Result:
z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ dist ↑z ↑w ^ 2 / (2 ^ 2 * (z.im * w.im)) = sinh (r / 2) ^ 2 ↔ dist ↑z ↑w ^ 2 / (4 * (z.im * w.im)) = sinh (r / 2) ^ 2

z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ z.im * w.im

case ha
z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ dist ↑z ↑w / (2 * √(z.im * w.im))

case hb
z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ sinh (r / 2)
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem xPrevIsoSelf_comp_dTo {j : ι} (h : ¬c.Rel (c.prev j) j) :
    (C.xPrevIsoSelf h).inv ≫ C.dTo j = 0

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j : ι
h : ¬c.Rel (c.prev j) j
⊢ (C.xPrevIsoSelf h).inv ≫ C.dTo j = 0

Tactic:
simp [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem size_swapIfInBounds (a : Array α) (i j) :
    (a.swapIfInBounds i j).size = a.size

Proof state:
case isTrue
α : Type u_1
a : Array α
i j : Nat
h✝ : i < a.size
⊢ (if h₂ : j < a.size then a.swap i j h✝ h₂ else a).size = a.size

Tactic:
try split

Result:
case isTrue.isTrue
α : Type u_1
a : Array α
i j : Nat
h✝¹ : i < a.size
h✝ : j < a.size
⊢ (a.swap i j h✝¹ h✝).size = a.size

case isTrue.isFalse
α : Type u_1
a : Array α
i j : Nat
h✝¹ : i < a.size
h✝ : ¬j < a.size
⊢ a.size = a.size

Proof state:
α : Type u_1
a : Array α
i j : Nat
⊢ (if h₁ : i < a.size then if h₂ : j < a.size then a.swap i j h₁ h₂ else a else a).size = a.size

Tactic:
split <;> (try split) <;> simp [size_swap]

Result:
no goals

Proof state:
case isTrue
α : Type u_1
a : Array α
i j : Nat
h✝ : i < a.size
⊢ (if h₂ : j < a.size then a.swap i j h✝ h₂ else a).size = a.size

Tactic:
split

Result:
case isTrue.isTrue
α : Type u_1
a : Array α
i j : Nat
h✝¹ : i < a.size
h✝ : j < a.size
⊢ (a.swap i j h✝¹ h✝).size = a.size

case isTrue.isFalse
α : Type u_1
a : Array α
i j : Nat
h✝¹ : i < a.size
h✝ : ¬j < a.size
⊢ a.size = a.size

Proof state:
α : Type u_1
a : Array α
i j : Nat
⊢ (a.swapIfInBounds i j).size = a.size

Tactic:
unfold swapIfInBounds

Result:
α : Type u_1
a : Array α
i j : Nat
⊢ (if h₁ : i < a.size then if h₂ : j < a.size then a.swap i j h₁ h₂ else a else a).size = a.size
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem range'_eq_range'TR : @range' = @range'TR

Proof state:
⊢ @range' = @range'TR

Tactic:
apply funext

Result:
case h

⊢ ∀ (x : Nat), @range' x = @range'TR x

Proof state:
s✝ n✝ : Nat
step : optParam Nat 1
s n m : Nat
⊢ range'TR.go step (n + 1) (s + step * (n + 1)) (range' (s + step * (n + 1)) m step) = range' s (n + 1 + m) step

Tactic:
simp [range'TR.go]

Result:
s✝ n✝ : Nat
step : optParam Nat 1
s n m : Nat
⊢ range'TR.go step n (s + step * (n + 1) - step) ((s + step * (n + 1) - step) :: range' (s + step * (n + 1)) m step) =
    range' s (n + 1 + m) step

Proof state:
case h

⊢ ∀ (x : Nat), @range' x = @range'TR x

Tactic:
intro s

Result:
case h
s : Nat
⊢ @range' s = @range'TR s

Proof state:
case h.h.h
s n : Nat
step : optParam Nat 1
⊢ range' s n step = range'TR s n step

Tactic:
exact (go s n 0).symm

Result:
no goals

Proof state:
case h.h
s n : Nat
⊢ @range' s n = @range'TR s n

Tactic:
apply funext

Result:
case h.h.h
s n : Nat
⊢ ∀ (x : optParam Nat 1), range' s n x = range'TR s n x

Proof state:
s✝ n✝ : Nat
step : optParam Nat 1
s n m : Nat
⊢ range'TR.go step n (s + step * (n + 1) - step) ((s + step * (n + 1) - step) :: range' (s + step * (n + 1)) m step) =
    range' s (n + 1 + m) step

Tactic:
rw [Nat.mul_succ, ← Nat.add_assoc, Nat.add_sub_cancel, Nat.add_right_comm n]

Result:
s✝ n✝ : Nat
step : optParam Nat 1
s n m : Nat
⊢ range'TR.go step n (s + step * n) ((s + step * n) :: range' (s + step * n + step) m step) = range' s (n + m + 1) step

Proof state:
s✝ n : Nat
step : optParam Nat 1
s m : Nat
⊢ range'TR.go step 0 (s + step * 0) (range' (s + step * 0) m step) = range' s (0 + m) step

Tactic:
simp [range'TR.go]

Result:
no goals

Proof state:
case h.h
s : Nat
⊢ ∀ (x : Nat), @range' s x = @range'TR s x

Tactic:
intro n

Result:
case h.h
s n : Nat
⊢ @range' s n = @range'TR s n

Proof state:
case h
s : Nat
⊢ @range' s = @range'TR s

Tactic:
apply funext

Result:
case h.h
s : Nat
⊢ ∀ (x : Nat), @range' s x = @range'TR s x

Proof state:
case h.h.h
s n : Nat
⊢ ∀ (x : optParam Nat 1), range' s n x = range'TR s n x

Tactic:
intro step

Result:
case h.h.h
s n : Nat
step : optParam Nat 1
⊢ range' s n step = range'TR s n step

Proof state:
s✝ n✝ : Nat
step : optParam Nat 1
s n m : Nat
⊢ range'TR.go step n (s + step * n) ((s + step * n) :: range' (s + step * n + step) m step) = range' s (n + m + 1) step

Tactic:
exact go s n (m + 1)

Result:
no goals
-- Mathlib/Topology/Order/Monotone.lean
theorem Antitone.map_ciSup_of_continuousAt {ι : Sort*} [Nonempty ι] {f : α → β} {g : ι → α}
    (Cf : ContinuousAt f (iSup g)) (Af : Antitone f)
    (bdd : BddAbove (range g)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
ι : Sort u_3
inst✝ : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Af : Antitone f
bdd : autoParam (BddAbove (range g)) _auto✝
⊢ f (⨆ i, g i) = ⨅ i, f (g i)

Tactic:
rw [iSup, Antitone.map_csSup_of_continuousAt Cf Af (range_nonempty g) bdd, ← range_comp, iInf,
  comp_def]

Result:
no goals
-- Mathlib/NumberTheory/PythagoreanTriples.lean
theorem ne_zero_of_coprime (hc : Int.gcd x y = 1) : z ≠ 0

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ 0 < z * z

Tactic:
rw [← h.eq, ← sq, ← sq]

Result:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ 0 < x ^ 2 + y ^ 2

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ 0 < x ^ 2 + y ^ 2

Tactic:
have hc' : Int.gcd x y ≠ 0 := by
  rw [hc]
  exact one_ne_zero

Result:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hc' : x.gcd y ≠ 0
⊢ 0 < x ^ 2 + y ^ 2

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ x.gcd y ≠ 0

Tactic:
rw [hc]

Result:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ 1 ≠ 0

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

Result:
no goals

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
this : 0 < z * z
⊢ z ≠ 0

Tactic:
rintro rfl

Result:
x y : ℤ
hc : x.gcd y = 1
h : PythagoreanTriple x y 0
this : 0 < 0 * 0
⊢ False

Proof state:
case inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hc' : x.gcd y ≠ 0
hxz : x ≠ 0
⊢ 0 < x ^ 2 + y ^ 2

Tactic:
apply lt_add_of_pos_of_le (sq_pos_of_ne_zero hxz) (sq_nonneg y)

Result:
no goals

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ z ≠ 0

Tactic:
suffices 0 < z * z by
  rintro rfl
  norm_num at this

Result:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ 0 < z * z

Proof state:
x y : ℤ
hc : x.gcd y = 1
h : PythagoreanTriple x y 0
this : 0 < 0 * 0
⊢ False

Tactic:
norm_num at this

Result:
no goals

Proof state:
case inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hc' : x.gcd y ≠ 0
hyz : y ≠ 0
⊢ 0 < x ^ 2 + y ^ 2

Tactic:
apply lt_add_of_le_of_pos (sq_nonneg x) (sq_pos_of_ne_zero hyz)

Result:
no goals

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hc' : x.gcd y ≠ 0
⊢ 0 < x ^ 2 + y ^ 2

Tactic:
rcases Int.ne_zero_of_gcd hc' with hxz | hyz

Result:
case inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hc' : x.gcd y ≠ 0
hxz : x ≠ 0
⊢ 0 < x ^ 2 + y ^ 2

case inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hc' : x.gcd y ≠ 0
hyz : y ≠ 0
⊢ 0 < x ^ 2 + y ^ 2
-- Mathlib/Data/DFinsupp/Defs.lean
theorem erase_def (i : ι) (f : Π₀ i, β i) : f.erase i = mk (f.support.erase i) fun j => f j.1

Proof state:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : Π₀ (i : ι), β i
⊢ erase i f = mk (f.support.erase i) fun j => f ↑j

Tactic:
ext j

Result:
case h
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : Π₀ (i : ι), β i
j : ι
⊢ (erase i f) j = (mk (f.support.erase i) fun j => f ↑j) j

Proof state:
case h
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : Π₀ (i : ι), β i
j : ι
⊢ (erase i f) j = (mk (f.support.erase i) fun j => f ↑j) j

Tactic:
by_cases h1 : j = i <;> by_cases h2 : f j ≠ 0 <;> simp at h2 <;> simp [h1, h2]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Roots.lean
theorem isRoot_cyclotomic_iff' {n : ℕ} {K : Type*} [Field K] {μ : K} [NeZero (n : K)] :
    IsRoot (cyclotomic n K) μ ↔ IsPrimitiveRoot μ n

Proof state:
case intro.intro
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : X - C μ ∣ cyclotomic n K
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : X - C μ ∣ cyclotomic i K
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
⊢ False

Tactic:
have hni : {i, n} ⊆ n.divisors := by simpa [Finset.insert_subset_iff, key'] using hnpos.ne'

Result:
case intro.intro
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : X - C μ ∣ cyclotomic n K
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : X - C μ ∣ cyclotomic i K
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ n.divisors
⊢ False

Proof state:
case intro.intro
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : X - C μ ∣ cyclotomic n K
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hiμ : X - C μ ∣ cyclotomic i K
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ n.divisors
⊢ False

Tactic:
obtain ⟨k, hk⟩ := hiμ

Result:
case intro.intro.intro
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
inst✝ : NeZero ↑n
hnpos : 0 < n
hμ : X - C μ ∣ cyclotomic n K
hμn : orderOf μ ∣ n
hnμ : orderOf μ ≠ n
ho : 0 < orderOf μ
i : ℕ
hio : i ∣ orderOf μ
key : i < n
key' : i ∣ n
hni : {i, n} ⊆ n.divisors
k : K[X]
hk : cyclotomic i K = (X - C μ) * k
⊢ False
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem norm_image_sub_le_of_bound (f : MultilinearMap 𝕜 E G)
    {C : ℝ} (hC : 0 ≤ C) (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) (m₁ m₂ : ∀ i, E i) :
    ‖f m₁ - f m₂‖ ≤ C * Fintype.card ι * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖

Proof state:
case pos
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
i j : ι
a✝ : j ∈ univ
h : j = i
⊢ (if i = i then ‖m₁ i - m₂ i‖ else ‖m₁ i‖ ⊔ ‖m₂ i‖) ≤ update (fun x => ‖m₁‖ ⊔ ‖m₂‖) i ‖m₁ - m₂‖ i

Tactic:
simp only [ite_true, Function.update_self]

Result:
case pos
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
i j : ι
a✝ : j ∈ univ
h : j = i
⊢ ‖m₁ i - m₂ i‖ ≤ ‖m₁ - m₂‖

Proof state:
case h0
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
⊢ ∀ i_1 ∈ univ, 0 ≤ if i_1 = i then ‖m₁ i - m₂ i‖ else ‖m₁ i_1‖ ⊔ ‖m₂ i_1‖

Tactic:
intro j _

Result:
case h0
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m₁ m₂ : (i : ι) → E i
i j : ι
a✝ : j ∈ univ
⊢ 0 ≤ if j = i then ‖m₁ i - m₂ i‖ else ‖m₁ j‖ ⊔ ‖m₂ j‖