harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Complex/AbsMax.lean
theorem norm_eqOn_of_isPreconnected_of_isMaxOn {f : E → F} {U : Set E} {c : E}
    (hc : IsPreconnected U) (ho : IsOpen U) (hd : DifferentiableOn ℂ f U) (hcU : c ∈ U)
    (hm : IsMaxOn (norm ∘ f) U c) : EqOn (norm ∘ f) (const E ‖f c‖) U

Proof state:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
U : Set E
c : E
hc : IsPreconnected U
ho : IsOpen U
hd : DifferentiableOn ℂ f U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set E := U ∩ {z | IsMaxOn (norm ∘ f) U z}
hV : ∀ x ∈ V, ‖f x‖ = ‖f c‖
hVo : IsOpen V
hVne : (U ∩ V).Nonempty
⊢ U ⊆ V

Tactic:
set W := U ∩ {z | ‖f z‖ ≠ ‖f c‖}

Result:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
U : Set E
c : E
hc : IsPreconnected U
ho : IsOpen U
hd : DifferentiableOn ℂ f U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set E := U ∩ {z | IsMaxOn (norm ∘ f) U z}
hV : ∀ x ∈ V, ‖f x‖ = ‖f c‖
hVo : IsOpen V
hVne : (U ∩ V).Nonempty
W : Set E := U ∩ {z | ‖f z‖ ≠ ‖f c‖}
⊢ U ⊆ V

Proof state:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
U : Set E
c : E
hc : IsPreconnected U
ho : IsOpen U
hd : DifferentiableOn ℂ f U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set E := U ∩ {z | IsMaxOn (norm ∘ f) U z}
hV : ∀ x ∈ V, ‖f x‖ = ‖f c‖
hVo : IsOpen V
hVne : (U ∩ V).Nonempty
W : Set E := U ∩ {z | ‖f z‖ ≠ ‖f c‖}
⊢ U ⊆ V

Tactic:
have hWo : IsOpen W := hd.continuousOn.norm.isOpen_inter_preimage ho isOpen_ne

Result:
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
U : Set E
c : E
hc : IsPreconnected U
ho : IsOpen U
hd : DifferentiableOn ℂ f U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
V : Set E := U ∩ {z | IsMaxOn (norm ∘ f) U z}
hV : ∀ x ∈ V, ‖f x‖ = ‖f c‖
hVo : IsOpen V
hVne : (U ∩ V).Nonempty
W : Set E := U ∩ {z | ‖f z‖ ≠ ‖f c‖}
hWo : IsOpen W
⊢ U ⊆ V
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem add_le_right_iff_mul_omega0_le {a b : Ordinal} : a + b ≤ b ↔ a * ω ≤ b

Proof state:
a b : Ordinal.{u_1}
⊢ a + b ≤ b ↔ a * ω ≤ b

Tactic:
rw [← add_eq_right_iff_mul_omega0_le]

Result:
a b : Ordinal.{u_1}
⊢ a + b ≤ b ↔ a + b = b

Proof state:
a b : Ordinal.{u_1}
⊢ a + b ≤ b ↔ a + b = b

Tactic:
exact (isNormal_add_right a).le_iff_eq

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/End.lean
@[simp]
lemma zero_smulRight (x : M) : (0 : M₁ →ₗ[R] S).smulRight x = 0

Proof state:
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
x : M
⊢ smulRight 0 x = 0

Tactic:
ext

Result:
case h
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
x : M
x✝ : M₁
⊢ (smulRight 0 x) x✝ = 0 x✝

Proof state:
case h
R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
x : M
x✝ : M₁
⊢ (smulRight 0 x) x✝ = 0 x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Interval.lean
theorem concat_comp_IccInclusionLeft (hb : f ⊤ = g ⊥) :
    (concat f g).comp IccInclusionLeft = f

Proof state:
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
hb : f ⊤ = g ⊥
⊢ (f.concat g).comp IccInclusionLeft = f

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
hb : f ⊤ = g ⊥
x : ↑(Icc a b)
⊢ ((f.concat g).comp IccInclusionLeft) x = f x

Proof state:
case h
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
hb : f ⊤ = g ⊥
x : ↑(Icc a b)
⊢ ((f.concat g).comp IccInclusionLeft) x = f x

Tactic:
simp [concat, IccExtendCM, hb, IccInclusionLeft, projIccCM, inclusion, x.2.2]

Result:
no goals
-- Mathlib/RingTheory/Binomial.lean
theorem multichoose_succ_neg_natCast [NatPowAssoc R] (n : ℕ) :
    multichoose (-n : R) (n + 1) = 0

Proof state:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
n : ℕ
⊢ multichoose (-↑n) (n + 1) = 0

Tactic:
rw [← nsmul_right_inj (Nat.factorial_ne_zero (n + 1)), smul_zero,
  factorial_nsmul_multichoose_eq_ascPochhammer, smeval_neg_nat,
  smeval_ascPochhammer_succ_neg n, Int.cast_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Bootstrap.lean
theorem foldrM_eq_foldrM_toList [Monad m]
    (f : α → β → m β) (init : β) (arr : Array α) :
    arr.foldrM f init = arr.toList.foldrM f init

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
arr : Array α
⊢ foldrM f init arr = List.foldrM f init arr.toList

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem map_push {f : α → β} {as : Vector α n} {x : α} :
    (as.push x).map f = (as.map f).push (f x)

Proof state:
α : Type u_1
β : Type u_2
n : Nat
f : α → β
as : Vector α n
x : α
⊢ map f (as.push x) = (map f as).push (f x)

Tactic:
cases as

Result:
case mk
α : Type u_1
β : Type u_2
n : Nat
f : α → β
x : α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ map f ({ toArray := toArray✝, size_toArray := size_toArray✝ }.push x) =
    (map f { toArray := toArray✝, size_toArray := size_toArray✝ }).push (f x)

Proof state:
case mk
α : Type u_1
β : Type u_2
n : Nat
f : α → β
x : α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ map f ({ toArray := toArray✝, size_toArray := size_toArray✝ }.push x) =
    (map f { toArray := toArray✝, size_toArray := size_toArray✝ }).push (f x)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldrM_append [Monad m] [LawfulMonad m] (f : α → β → m β) (b) (l : Vector α n) (l' : Vector α k) :
    (l ++ l').foldrM f b = l'.foldrM f b >>= l.foldrM f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n k : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
b : β
l : Vector α n
l' : Vector α k
⊢ foldrM f b (l ++ l') = do
    let b ← foldrM f b l'
    foldrM f b l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
k : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
b : β
l' : Vector α k
l : Array α
⊢ foldrM f b ({ toArray := l, size_toArray := ⋯ } ++ l') = do
    let b ← foldrM f b l'
    foldrM f b { toArray := l, size_toArray := ⋯ }

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
k : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
b : β
l' : Vector α k
l : Array α
⊢ foldrM f b ({ toArray := l, size_toArray := ⋯ } ++ l') = do
    let b ← foldrM f b l'
    foldrM f b { toArray := l, size_toArray := ⋯ }

Tactic:
rcases l' with ⟨l', rfl⟩

Result:
case mk.mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
b : β
l l' : Array α
⊢ foldrM f b ({ toArray := l, size_toArray := ⋯ } ++ { toArray := l', size_toArray := ⋯ }) = do
    let b ← foldrM f b { toArray := l', size_toArray := ⋯ }
    foldrM f b { toArray := l, size_toArray := ⋯ }

Proof state:
case mk.mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
b : β
l l' : Array α
⊢ foldrM f b ({ toArray := l, size_toArray := ⋯ } ++ { toArray := l', size_toArray := ⋯ }) = do
    let b ← foldrM f b { toArray := l', size_toArray := ⋯ }
    foldrM f b { toArray := l, size_toArray := ⋯ }

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Factorization.lean
lemma comp_eq_top_iff : W₁.comp W₂ = ⊤ ↔ HasFactorization W₁ W₂

Proof state:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
W₁ W₂ : MorphismProperty C
⊢ W₁.comp W₂ = ⊤ → W₁.HasFactorization W₂

Tactic:
intro h

Result:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
W₁ W₂ : MorphismProperty C
h : W₁.comp W₂ = ⊤
⊢ W₁.HasFactorization W₂

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
W₁ W₂ : MorphismProperty C
h : W₁.comp W₂ = ⊤
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ W₁.comp W₂ f

Tactic:
simp only [h, top_apply]

Result:
no goals

Proof state:
case mpr.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
W₁ W₂ : MorphismProperty C
a✝ : W₁.HasFactorization W₂
X Y : C
f : X ⟶ Y
⊢ W₁.comp W₂ f ↔ ⊤ f

Tactic:
simp only [top_apply, iff_true]

Result:
case mpr.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
W₁ W₂ : MorphismProperty C
a✝ : W₁.HasFactorization W₂
X Y : C
f : X ⟶ Y
⊢ W₁.comp W₂ f

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
W₁ W₂ : MorphismProperty C
⊢ W₁.comp W₂ = ⊤ ↔ W₁.HasFactorization W₂

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
W₁ W₂ : MorphismProperty C
⊢ W₁.comp W₂ = ⊤ → W₁.HasFactorization W₂

case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
W₁ W₂ : MorphismProperty C
⊢ W₁.HasFactorization W₂ → W₁.comp W₂ = ⊤

Proof state:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
W₁ W₂ : MorphismProperty C
h : W₁.comp W₂ = ⊤
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this : W₁.comp W₂ f
⊢ Nonempty (W₁.MapFactorizationData W₂ f)

Tactic:
exact ⟨this.some⟩

Result:
no goals

Proof state:
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
W₁ W₂ : MorphismProperty C
a✝ : W₁.HasFactorization W₂
⊢ W₁.comp W₂ = ⊤

Tactic:
ext X Y f

Result:
case mpr.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
W₁ W₂ : MorphismProperty C
a✝ : W₁.HasFactorization W₂
X Y : C
f : X ⟶ Y
⊢ W₁.comp W₂ f ↔ ⊤ f

Proof state:
case mpr.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
W₁ W₂ : MorphismProperty C
a✝ : W₁.HasFactorization W₂
X Y : C
f : X ⟶ Y
⊢ W₁.comp W₂ f

Tactic:
exact ⟨factorizationData W₁ W₂ f⟩

Result:
no goals

Proof state:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
W₁ W₂ : MorphismProperty C
h : W₁.comp W₂ = ⊤
⊢ W₁.HasFactorization W₂

Tactic:
refine ⟨fun f => ?_⟩

Result:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
W₁ W₂ : MorphismProperty C
h : W₁.comp W₂ = ⊤
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ Nonempty (W₁.MapFactorizationData W₂ f)

Proof state:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
W₁ W₂ : MorphismProperty C
h : W₁.comp W₂ = ⊤
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ Nonempty (W₁.MapFactorizationData W₂ f)

Tactic:
have : W₁.comp W₂ f := by simp only [h, top_apply]

Result:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
W₁ W₂ : MorphismProperty C
h : W₁.comp W₂ = ⊤
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this : W₁.comp W₂ f
⊢ Nonempty (W₁.MapFactorizationData W₂ f)

Proof state:
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
W₁ W₂ : MorphismProperty C
⊢ W₁.HasFactorization W₂ → W₁.comp W₂ = ⊤

Tactic:
intro

Result:
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
W₁ W₂ : MorphismProperty C
a✝ : W₁.HasFactorization W₂
⊢ W₁.comp W₂ = ⊤
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_rotateLeft {m w : Nat} {x : BitVec w} :
    (x.rotateLeft m).msb = x.getMsbD (m % w)

Proof state:
case neg
m w : Nat
x : BitVec w
h : ¬w = 0
⊢ x.getMsbD (m % w) = true → 0 < w

Tactic:
omega

Result:
no goals

Proof state:
case pos
m w : Nat
x : BitVec w
h : w = 0
⊢ (decide (0 < w) && x.getMsbD ((m + 0) % w)) = x.getMsbD (m % w)

Tactic:
simp [h]

Result:
no goals

Proof state:
m w : Nat
x : BitVec w
⊢ (decide (0 < w) && x.getMsbD ((m + 0) % w)) = x.getMsbD (m % w)

Tactic:
by_cases h : w = 0

Result:
case pos
m w : Nat
x : BitVec w
h : w = 0
⊢ (decide (0 < w) && x.getMsbD ((m + 0) % w)) = x.getMsbD (m % w)

case neg
m w : Nat
x : BitVec w
h : ¬w = 0
⊢ (decide (0 < w) && x.getMsbD ((m + 0) % w)) = x.getMsbD (m % w)

Proof state:
m w : Nat
x : BitVec w
⊢ (x.rotateLeft m).msb = x.getMsbD (m % w)

Tactic:
simp only [BitVec.msb, getMsbD_rotateLeft]

Result:
m w : Nat
x : BitVec w
⊢ (decide (0 < w) && x.getMsbD ((m + 0) % w)) = x.getMsbD (m % w)

Proof state:
case neg
m w : Nat
x : BitVec w
h : ¬w = 0
⊢ (decide (0 < w) && x.getMsbD ((m + 0) % w)) = x.getMsbD (m % w)

Tactic:
simp

Result:
case neg
m w : Nat
x : BitVec w
h : ¬w = 0
⊢ x.getMsbD (m % w) = true → 0 < w
-- Mathlib/Data/Nat/Choose/Factorization.lean
theorem factorization_choose_eq_zero_of_lt (h : n < p) : (choose n k).factorization p = 0

Proof state:
p n k : ℕ
h : n < p
⊢ (n.choose k).factorization p = 0

Tactic:
by_cases hnk : n < k

Result:
case pos
p n k : ℕ
h : n < p
hnk : n < k
⊢ (n.choose k).factorization p = 0

case neg
p n k : ℕ
h : n < p
hnk : ¬n < k
⊢ (n.choose k).factorization p = 0

Proof state:
case pos
p n k : ℕ
h : n < p
hnk : n < k
⊢ (n.choose k).factorization p = 0

Tactic:
simp [choose_eq_zero_of_lt hnk]

Result:
no goals

Proof state:
case neg
p n k : ℕ
h : n < p
hnk : ¬n < k
⊢ (n.choose k).factorization p = 0

Tactic:
rw [choose_eq_factorial_div_factorial (le_of_not_lt hnk),
  factorization_div (factorial_mul_factorial_dvd_factorial (le_of_not_lt hnk)), Finsupp.coe_tsub,
  Pi.sub_apply, factorization_factorial_eq_zero_of_lt h, zero_tsub]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
lemma Monic.irreducible_iff_natDegree (hp : p.Monic) :
    Irreducible p ↔
      p ≠ 1 ∧ ∀ f g : R[X], f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0

Proof state:
case pos
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p = 1
⊢ Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0

Tactic:
simp [hp1]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : ¬p = 1
⊢ Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0

Tactic:
rw [irreducible_of_monic hp hp1, and_iff_right hp1]

Result:
case neg
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : ¬p = 1
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1) ↔
    ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0

Proof state:
case neg
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : ¬p = 1
⊢ (∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1) ↔
    ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0

Tactic:
refine forall₄_congr fun a b ha hb => ?_

Result:
case neg
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : ¬p = 1
a b : R[X]
ha : a.Monic
hb : b.Monic
⊢ a * b = p → a = 1 ∨ b = 1 ↔ a * b = p → a.natDegree = 0 ∨ b.natDegree = 0

Proof state:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
⊢ Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0

Tactic:
by_cases hp1 : p = 1

Result:
case pos
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : p = 1
⊢ Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0

case neg
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : ¬p = 1
⊢ Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : R[X]), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0

Proof state:
case neg
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hp : p.Monic
hp1 : ¬p = 1
a b : R[X]
ha : a.Monic
hb : b.Monic
⊢ a * b = p → a = 1 ∨ b = 1 ↔ a * b = p → a.natDegree = 0 ∨ b.natDegree = 0

Tactic:
rw [ha.natDegree_eq_zero_iff_eq_one, hb.natDegree_eq_zero_iff_eq_one]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Bounded.lean
theorem isCompact_of_isClosed_isBounded [ProperSpace α] (hc : IsClosed s) (hb : IsBounded s) :
    IsCompact s

Proof state:
case inl
α : Type u
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
hc : IsClosed ∅
hb : Bornology.IsBounded ∅
⊢ IsCompact ∅

Tactic:
exact isCompact_empty

Result:
no goals

Proof state:
case inr.intro.intro
α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
hc : IsClosed s
hb : Bornology.IsBounded s
x : α
r : ℝ
hr : s ⊆ closedBall x r
⊢ IsCompact s

Tactic:
exact (isCompact_closedBall x r).of_isClosed_subset hc hr

Result:
no goals

Proof state:
α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
hc : IsClosed s
hb : Bornology.IsBounded s
⊢ IsCompact s

Tactic:
rcases eq_empty_or_nonempty s with (rfl | ⟨x, -⟩)

Result:
case inl
α : Type u
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
hc : IsClosed ∅
hb : Bornology.IsBounded ∅
⊢ IsCompact ∅

case inr.intro
α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
hc : IsClosed s
hb : Bornology.IsBounded s
x : α
⊢ IsCompact s

Proof state:
case inr.intro
α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
hc : IsClosed s
hb : Bornology.IsBounded s
x : α
⊢ IsCompact s

Tactic:
rcases hb.subset_closedBall x with ⟨r, hr⟩

Result:
case inr.intro.intro
α : Type u
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : ProperSpace α
hc : IsClosed s
hb : Bornology.IsBounded s
x : α
r : ℝ
hr : s ⊆ closedBall x r
⊢ IsCompact s
-- Mathlib/Data/Matroid/Map.lean
@[simp] lemma restrictSubtype_ground_isBasis_iff {I X : Set M.E} :
    (M.restrictSubtype M.E).IsBasis I X ↔ M.IsBasis I X

Proof state:
α : Type u_1
M : Matroid α
I X : Set ↑M.E
⊢ (M.restrictSubtype M.E).IsBasis I X ↔ M.IsBasis (Subtype.val '' I) (Subtype.val '' X)

Tactic:
rw [restrictSubtype_isBasis_iff, isBasis'_iff_isBasis]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Basic.lean
theorem dist_smul_vadd_sq (r : ℝ) (v : V) (p₁ p₂ : P) :
    dist (r • v +ᵥ p₁) p₂ * dist (r • v +ᵥ p₁) p₂ =
      ⟪v, v⟫ * r * r + 2 * ⟪v, p₁ -ᵥ p₂⟫ * r + ⟪p₁ -ᵥ 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
r : ℝ
v : V
p₁ p₂ : P
⊢ r * (r * inner v v) + 2 * (r * inner v (p₁ -ᵥ p₂)) + inner (p₁ -ᵥ p₂) (p₁ -ᵥ p₂) =
    inner v v * r * r + 2 * inner v (p₁ -ᵥ p₂) * r + inner (p₁ -ᵥ p₂) (p₁ -ᵥ p₂)

Tactic:
ring

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
r : ℝ
v : V
p₁ p₂ : P
⊢ dist (r • v +ᵥ p₁) p₂ * dist (r • v +ᵥ p₁) p₂ =
    inner v v * r * r + 2 * inner v (p₁ -ᵥ p₂) * r + inner (p₁ -ᵥ p₂) (p₁ -ᵥ p₂)

Tactic:
rw [dist_eq_norm_vsub V _ p₂, ← real_inner_self_eq_norm_mul_norm, vadd_vsub_assoc,
  real_inner_add_add_self, real_inner_smul_left, real_inner_smul_left, real_inner_smul_right]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
r : ℝ
v : V
p₁ p₂ : P
⊢ r * (r * inner v v) + 2 * (r * inner v (p₁ -ᵥ p₂)) + inner (p₁ -ᵥ p₂) (p₁ -ᵥ p₂) =
    inner v v * r * r + 2 * inner v (p₁ -ᵥ p₂) * r + inner (p₁ -ᵥ p₂) (p₁ -ᵥ p₂)
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup'_lt_iff : s.sup' H f < a ↔ ∀ i ∈ s, f i < a

Proof state:
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ (∀ b ∈ s, (WithBot.some ∘ f) b < ↑a) ↔ ∀ i ∈ s, f i < a

Tactic:
exact forall₂_congr (fun _ _ => WithBot.coe_lt_coe)

Result:
no goals

Proof state:
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ s.sup' H f < a ↔ ∀ i ∈ s, f i < a

Tactic:
rw [← WithBot.coe_lt_coe, coe_sup', Finset.sup_lt_iff (WithBot.bot_lt_coe a)]

Result:
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ (∀ b ∈ s, (WithBot.some ∘ f) b < ↑a) ↔ ∀ i ∈ s, f i < a
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem eq_σ_comp_of_not_injective' {n : ℕ} {Δ' : SimplexCategory} (θ : mk (n + 1) ⟶ Δ')
    (i : Fin (n + 1)) (hi : θ.toOrderHom (Fin.castSucc i) = θ.toOrderHom i.succ) :
    ∃ θ' : mk n ⟶ Δ', θ = σ i ≫ θ'

Proof state:
case pos
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h' : x ≤ i.castSucc
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) ((Hom.toOrderHom (δ i.succ)) (i.predAbove x))

Tactic:
rw [Fin.predAbove_of_le_castSucc i x h']

Result:
case pos
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h' : x ≤ i.castSucc
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) ((Hom.toOrderHom (δ i.succ)) (x.castPred ⋯))

Proof state:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h' : x ≤ i.castSucc
⊢ (x.castPred ⋯).castSucc < i.succ

Tactic:
exact (Fin.castSucc_lt_succ_iff.mpr h')

Result:
no goals

Proof state:
case h.a.h
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
⊢ ⇑(Hom.toOrderHom θ) = ⇑(Hom.toOrderHom (σ i ≫ δ i.succ ≫ θ))

Tactic:
ext1 x

Result:
case h.a.h.h
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom (σ i ≫ δ i.succ ≫ θ)) x

Proof state:
case pos.h.e_6.h.h
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h'✝ : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
h' : i.castSucc < y.succ
hy : x = y.succ
h'' : y = i
⊢ i.castSucc < i.succ

Tactic:
exact Fin.lt_succ

Result:
no goals

Proof state:
case pos.h.e_6.h
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h'✝ : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
h' : i.castSucc < y.succ
hy : x = y.succ
h'' : y = i
⊢ i.castSucc = (Hom.toOrderHom (δ i.succ)) i

Tactic:
dsimp [δ]

Result:
case pos.h.e_6.h
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h'✝ : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
h' : i.castSucc < y.succ
hy : x = y.succ
h'' : y = i
⊢ i.castSucc = i.succ.succAbove i
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma nonsingular_iff_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :
    W.Nonsingular P ↔ W.Equation P ∧ (eval P W.polynomialX ≠ 0 ∨ eval P W.polynomialY ≠ 0)

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.Nonsingular P ↔ W.Equation P ∧ ((eval P) W.polynomialX ≠ 0 ∨ (eval P) W.polynomialY ≠ 0)

Tactic:
rw [nonsingular_of_Z_ne_zero hPz, Affine.Nonsingular, ← equation_of_Z_ne_zero hPz,
  ← eval_polynomialX_of_Z_ne_zero hPz, div_ne_zero_iff, and_iff_left <| pow_ne_zero 2 hPz,
  ← eval_polynomialY_of_Z_ne_zero hPz, div_ne_zero_iff, and_iff_left <| pow_ne_zero 2 hPz]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nmul_le_iff : a ⨳ b ≤ c ↔ ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'

Proof state:
a b c : Ordinal.{u}
⊢ a ⨳ b ≤ c ↔ ∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'

Tactic:
rw [← not_iff_not]

Result:
a b c : Ordinal.{u}
⊢ ¬a ⨳ b ≤ c ↔ ¬∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'

Proof state:
a b c : Ordinal.{u}
⊢ ¬a ⨳ b ≤ c ↔ ¬∀ a' < a, ∀ b' < b, a' ⨳ b ♯ a ⨳ b' < c ♯ a' ⨳ b'

Tactic:
simp [lt_nmul_iff]

Result:
no goals