harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Int/Basic.lean
theorem sq_of_gcd_eq_one {a b c : ℤ} (h : Int.gcd a b = 1) (heq : a * b = c ^ 2) :
    ∃ a0 : ℤ, a = a0 ^ 2 ∨ a = -a0 ^ 2

Proof state:
case intro.intro
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
⊢ ∃ a0, a = a0 ^ 2 ∨ a = -a0 ^ 2

Tactic:
use d

Result:
case h
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
⊢ a = d ^ 2 ∨ a = -d ^ 2

Proof state:
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
⊢ IsUnit 1

Tactic:
exact isUnit_one

Result:
no goals

Proof state:
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
⊢ IsUnit (GCDMonoid.gcd a b)

Tactic:
rw [← coe_gcd, h, Int.ofNat_one]

Result:
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
⊢ IsUnit 1

Proof state:
case h.inr
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
hu' : u = -1
⊢ d ^ 2 * ↑u = d ^ 2 ∨ d ^ 2 * ↑u = -d ^ 2

Tactic:
rw [hu']

Result:
case h.inr
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
hu' : u = -1
⊢ d ^ 2 * ↑(-1) = d ^ 2 ∨ d ^ 2 * ↑(-1) = -d ^ 2

Proof state:
case h
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
⊢ a = d ^ 2 ∨ a = -d ^ 2

Tactic:
rw [← hu]

Result:
case h
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
⊢ d ^ 2 * ↑u = d ^ 2 ∨ d ^ 2 * ↑u = -d ^ 2

Proof state:
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
⊢ ∃ a0, a = a0 ^ 2 ∨ a = -a0 ^ 2

Tactic:
obtain ⟨d, ⟨u, hu⟩⟩ := exists_associated_pow_of_mul_eq_pow h' heq

Result:
case intro.intro
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
⊢ ∃ a0, a = a0 ^ 2 ∨ a = -a0 ^ 2

Proof state:
case h.inr
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
d : ℤ
u : ℤˣ
hu : d ^ 2 * ↑u = a
hu' : u = -1
⊢ d ^ 2 * ↑(-1) = d ^ 2 ∨ d ^ 2 * ↑(-1) = -d ^ 2

Tactic:
simp

Result:
no goals

Proof state:
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
⊢ ∃ a0, a = a0 ^ 2 ∨ a = -a0 ^ 2

Tactic:
have h' : IsUnit (GCDMonoid.gcd a b) := by
  rw [← coe_gcd, h, Int.ofNat_one]
  exact isUnit_one

Result:
a b c : ℤ
h : a.gcd b = 1
heq : a * b = c ^ 2
h' : IsUnit (GCDMonoid.gcd a b)
⊢ ∃ a0, a = a0 ^ 2 ∨ a = -a0 ^ 2
-- Mathlib/RingTheory/Multiplicity.lean
theorem dvd_iff_multiplicity_pos {a b : α} : 0 < multiplicity a b ↔ a ∣ b :=
  ⟨dvd_of_multiplicity_pos, fun hdvd => Nat.pos_of_ne_zero (by simpa [multiplicity_eq_zero])⟩

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
hdvd : a ∣ b
⊢ multiplicity a b ≠ 0

Tactic:
simpa [multiplicity_eq_zero]

Result:
no goals
-- Mathlib/NumberTheory/Ostrowski.lean
/-- There exists a minimal positive integer with absolute value smaller than 1. -/
lemma exists_minimal_nat_zero_lt_and_lt_one :
    ∃ p : ℕ, (0 < f p ∧ f p < 1) ∧ ∀ m : ℕ, 0 < f m ∧ f m < 1 → p ≤ m

Proof state:
case intro.intro
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
n : ℕ
hn1 : n ≠ 0
hn2 : f ↑n ≠ 1
P : Set ℕ := {m | 0 < f ↑m ∧ f ↑m < 1}
⊢ ∃ p, (0 < f ↑p ∧ f ↑p < 1) ∧ ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m

Tactic:
have hP : P.Nonempty :=
  ⟨n, map_pos_of_ne_zero f (Nat.cast_ne_zero.mpr hn1), lt_of_le_of_ne (bdd n) hn2⟩

Result:
case intro.intro
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
n : ℕ
hn1 : n ≠ 0
hn2 : f ↑n ≠ 1
P : Set ℕ := {m | 0 < f ↑m ∧ f ↑m < 1}
hP : P.Nonempty
⊢ ∃ p, (0 < f ↑p ∧ f ↑p < 1) ∧ ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m

Proof state:
case inr
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
hf_nontriv : ∀ (n : ℕ), n ≠ 0 → f ↑n = 1
n : ℕ
hn : n ≠ 0
⊢ f ↑n = AbsoluteValue.trivial ↑n

Tactic:
simp [hf_nontriv, hn]

Result:
no goals

Proof state:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
hf_nontriv : ∀ (n : ℕ), n ≠ 0 → f ↑n = 1
n : ℕ
⊢ f ↑n = AbsoluteValue.trivial ↑n

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Result:
case inl
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
hf_nontriv : ∀ (n : ℕ), n ≠ 0 → f ↑n = 1
⊢ f ↑0 = AbsoluteValue.trivial ↑0

case inr
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
hf_nontriv : ∀ (n : ℕ), n ≠ 0 → f ↑n = 1
n : ℕ
hn : n ≠ 0
⊢ f ↑n = AbsoluteValue.trivial ↑n

Proof state:
case inl
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
hf_nontriv : ∀ (n : ℕ), n ≠ 0 → f ↑n = 1
⊢ f ↑0 = AbsoluteValue.trivial ↑0

Tactic:
simp

Result:
no goals

Proof state:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
⊢ ∃ n, n ≠ 0 ∧ f ↑n ≠ 1

Tactic:
contrapose! hf_nontriv

Result:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
hf_nontriv : ∀ (n : ℕ), n ≠ 0 → f ↑n = 1
⊢ ¬f.IsNontrivial

Proof state:
case intro.intro
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
n : ℕ
hn1 : n ≠ 0
hn2 : f ↑n ≠ 1
⊢ ∃ p, (0 < f ↑p ∧ f ↑p < 1) ∧ ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m

Tactic:
set P := {m : ℕ | 0 < f ↑m ∧ f ↑m < 1}

Result:
case intro.intro
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
n : ℕ
hn1 : n ≠ 0
hn2 : f ↑n ≠ 1
P : Set ℕ := {m | 0 < f ↑m ∧ f ↑m < 1}
⊢ ∃ p, (0 < f ↑p ∧ f ↑p < 1) ∧ ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m

Proof state:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
hf_nontriv : ∀ (n : ℕ), n ≠ 0 → f ↑n = 1
⊢ ¬f.IsNontrivial

Tactic:
refine (isNontrivial_iff_ne_trivial f).not_left.mpr <| eq_on_nat_iff_eq.mp fun n ↦ ?_

Result:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
hf_nontriv : ∀ (n : ℕ), n ≠ 0 → f ↑n = 1
n : ℕ
⊢ f ↑n = AbsoluteValue.trivial ↑n

Proof state:
case intro.intro
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
n : ℕ
hn1 : n ≠ 0
hn2 : f ↑n ≠ 1
P : Set ℕ := {m | 0 < f ↑m ∧ f ↑m < 1}
hP : P.Nonempty
⊢ ∃ p, (0 < f ↑p ∧ f ↑p < 1) ∧ ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m

Tactic:
exact ⟨sInf P, Nat.sInf_mem hP, fun m hm ↦ Nat.sInf_le hm⟩

Result:
no goals
-- Mathlib/Order/GaloisConnection/Basic.lean
theorem l_sup_u [SemilatticeSup α] [SemilatticeSup β] (gi : GaloisInsertion l u) (a b : β) :
    l (u a ⊔ u b) = a ⊔ b :=
  calc
    l (u a ⊔ u b) = l (u a) ⊔ l (u b) := gi.gc.l_sup
    _ = a ⊔ b

Proof state:
α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
gi : GaloisInsertion l u
a b : β
⊢ l (u a) ⊔ l (u b) = a ⊔ b

Tactic:
simp only [gi.l_u_eq]

Result:
no goals
-- Mathlib/Order/Irreducible.lean
theorem SupPrime.ne_bot (ha : SupPrime a) : a ≠ ⊥

Proof state:
α : Type u_2
inst✝¹ : SemilatticeSup α
a : α
inst✝ : OrderBot α
ha : SupPrime a
⊢ a ≠ ⊥

Tactic:
rintro rfl

Result:
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
ha : SupPrime ⊥
⊢ False

Proof state:
α : Type u_2
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
ha : SupPrime ⊥
⊢ False

Tactic:
exact not_supPrime_bot ha

Result:
no goals
-- Mathlib/RingTheory/RingHom/Finite.lean
theorem RingHom.finite_localizationPreserves : RingHom.LocalizationPreserves @RingHom.Finite

Proof state:
R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
⊢ (IsLocalization.map S' f ⋯).Finite

Tactic:
letI := f.toAlgebra

Result:
R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this : Algebra R S := f.toAlgebra
⊢ (IsLocalization.map S' f ⋯).Finite

Proof state:
R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this✝⁴ : Algebra R S := f.toAlgebra
this✝³ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
f' : R' →+* S' := IsLocalization.map S' f ⋯
this✝² : Algebra R' S' := f'.toAlgebra
this✝¹ : IsScalarTower R R' S'
this✝ : IsScalarTower R S S'
this : IsLocalization (Algebra.algebraMapSubmonoid S M) S'
⊢ (IsLocalization.map S' f ⋯).Finite

Tactic:
have : Module.Finite R S := hf

Result:
R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this✝⁵ : Algebra R S := f.toAlgebra
this✝⁴ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
f' : R' →+* S' := IsLocalization.map S' f ⋯
this✝³ : Algebra R' S' := f'.toAlgebra
this✝² : IsScalarTower R R' S'
this✝¹ : IsScalarTower R S S'
this✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) S'
this : Module.Finite R S
⊢ (IsLocalization.map S' f ⋯).Finite

Proof state:
R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this : Algebra R S := f.toAlgebra
⊢ (IsLocalization.map S' f ⋯).Finite

Tactic:
letI := ((algebraMap S S').comp f).toAlgebra

Result:
R S : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_1
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization M R'
inst✝ : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this✝ : Algebra R S := f.toAlgebra
this : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
⊢ (IsLocalization.map S' f ⋯).Finite
-- Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean
theorem IsTerminal.hasTerminal {X : C} (h : IsTerminal X) : HasTerminal C :=
  { has_limit := fun F => HasLimit.mk ⟨⟨X, by aesop_cat, by simp⟩,
    isLimitChangeEmptyCone _ h _ (Iso.refl _)⟩ }

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
h : IsTerminal X
F : Discrete PEmpty.{1} ⥤ C
⊢ ∀ ⦃X_1 Y : Discrete PEmpty.{1}⦄ (f : X_1 ⟶ Y),
    ((Functor.const (Discrete PEmpty.{1})).obj X).map f ≫ id (Discrete.casesOn Y fun as => ⋯.elim) =
      id (Discrete.casesOn X_1 fun as => ⋯.elim) ≫ F.map f

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
h : IsTerminal X
F : Discrete PEmpty.{1} ⥤ C
⊢ (X_1 : Discrete PEmpty.{1}) → ((Functor.const (Discrete PEmpty.{1})).obj X).obj X_1 ⟶ F.obj X_1

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Computability/Partrec.lean
theorem nat_rec {f : α → ℕ} {g : α →. σ} {h : α → ℕ × σ →. σ} (hf : Computable f) (hg : Partrec g)
    (hh : Partrec₂ h) : Partrec fun a => (f a).rec (g a) fun y IH => IH.bind fun i => h a (y, i) :=
  (Nat.Partrec.prec' hf hg hh).of_eq fun n => by
    rcases e : decode (α := α) n with - | a <;> simp [e]
    induction' f a with m IH <;> simp
    rw [IH, Part.bind_map]
    congr; funext s
    simp [encodek]

Proof state:
case some.succ
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
m : ℕ
IH :
  Nat.rec (Part.map encode (g a))
      (fun y IH =>
        IH.bind fun i => (↑(Option.map (Prod.mk a ∘ Prod.mk y) (decode i))).bind fun a => Part.map encode (h a.1 a.2))
      m =
    Part.map encode (Nat.rec (g a) (fun y IH => IH.bind fun i => h a (y, i)) m)
⊢ ((Nat.rec (g a) (fun y IH => IH.bind fun i => h a (y, i)) m).bind fun y =>
      (↑(Option.map (Prod.mk a ∘ Prod.mk m) (decode (encode y)))).bind fun a => Part.map encode (h a.1 a.2)) =
    (Nat.rec (g a) (fun y IH => IH.bind fun i => h a (y, i)) m).bind fun y => Part.map encode (h a (m, y))

Tactic:
congr

Result:
case some.succ.e_g
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
m : ℕ
IH :
  Nat.rec (Part.map encode (g a))
      (fun y IH =>
        IH.bind fun i => (↑(Option.map (Prod.mk a ∘ Prod.mk y) (decode i))).bind fun a => Part.map encode (h a.1 a.2))
      m =
    Part.map encode (Nat.rec (g a) (fun y IH => IH.bind fun i => h a (y, i)) m)
⊢ (fun y => (↑(Option.map (Prod.mk a ∘ Prod.mk m) (decode (encode y)))).bind fun a => Part.map encode (h a.1 a.2)) =
    fun y => Part.map encode (h a (m, y))
-- Mathlib/Data/Finset/Sups.lean
lemma filter_infs_le [DecidableRel (α := α) (· ≤ ·)] (s t : Finset α) (a : α) :
    {b ∈ s ⊼ t | a ≤ b} = {b ∈ s | a ≤ b} ⊼ {b ∈ t | a ≤ b}

Proof state:
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : SemilatticeInf α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
s t : Finset α
a : α
⊢ filter (fun b => a ≤ b) (s ⊼ t) = filter (fun b => a ≤ b) s ⊼ filter (fun b => a ≤ b) t

Tactic:
simp only [← coe_inj, coe_filter, coe_infs, ← mem_coe, Set.sep_infs_le]

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
theorem inseparable_iff_closure_eq : (x ~ᵢ y) ↔ closure ({x} : Set X) = closure {y}

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ (x ~ᵢ y) ↔ closure {x} = closure {y}

Tactic:
simp only [inseparable_iff_specializes_and, specializes_iff_closure_subset, ← subset_antisymm_iff,
  eq_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Pasting.lean
theorem inr_inl_pushoutLeftPushoutInrIso_hom :
    pushout.inr f g ≫ pushout.inl (pushout.inr f g) g' ≫ (pushoutLeftPushoutInrIso f g g').hom =
      g' ≫ pushout.inr f (g ≫ g')

Proof state:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
g' : Z ⟶ W
inst✝¹ : HasPushout f g
inst✝ : HasPushout (pushout.inr f g) g'
⊢ pushout.inr f g ≫ pushout.inl (pushout.inr f g) g' ≫ (pushoutLeftPushoutInrIso f g g').hom =
    g' ≫ pushout.inr f (g ≫ g')

Tactic:
rw [← Category.assoc, ← Iso.eq_comp_inv, Category.assoc, inr_pushoutLeftPushoutInrIso_inv,
  pushout.condition]

Result:
no goals
-- Mathlib/Tactic/NormNum/Prime.lean
theorem MinFacHelper.one_lt {n k : ℕ} (h : MinFacHelper n k) : 1 < n

Proof state:
case inr.inl
k : ℕ
h✝ : MinFacHelper (succ 0) k
this : 2 < (succ 0).minFac
h : succ 0 > 0
⊢ 1 < succ 0

Tactic:
simp_all

Result:
no goals

Proof state:
case inl
k : ℕ
h : MinFacHelper 0 k
this : 2 < minFac 0
⊢ 1 < 0

Tactic:
contradiction

Result:
no goals

Proof state:
case inr.inr
n k : ℕ
h✝¹ : MinFacHelper n k
this : 2 < n.minFac
h✝ : n > 0
h : succ 0 < n
⊢ 1 < n

Tactic:
exact h

Result:
no goals

Proof state:
case inr
n k : ℕ
h✝ : MinFacHelper n k
this : 2 < n.minFac
h : n > 0
⊢ 1 < n

Tactic:
rcases (succ_le_of_lt h).eq_or_lt with rfl|h

Result:
case inr.inl
k : ℕ
h✝ : MinFacHelper (succ 0) k
this : 2 < (succ 0).minFac
h : succ 0 > 0
⊢ 1 < succ 0

case inr.inr
n k : ℕ
h✝¹ : MinFacHelper n k
this : 2 < n.minFac
h✝ : n > 0
h : succ 0 < n
⊢ 1 < n

Proof state:
n k : ℕ
h : MinFacHelper n k
⊢ 1 < n

Tactic:
have : 2 < minFac n := h.1.trans_le h.2.2

Result:
n k : ℕ
h : MinFacHelper n k
this : 2 < n.minFac
⊢ 1 < n

Proof state:
n k : ℕ
h : MinFacHelper n k
this : 2 < n.minFac
⊢ 1 < n

Tactic:
obtain rfl | h := n.eq_zero_or_pos

Result:
case inl
k : ℕ
h : MinFacHelper 0 k
this : 2 < minFac 0
⊢ 1 < 0

case inr
n k : ℕ
h✝ : MinFacHelper n k
this : 2 < n.minFac
h : n > 0
⊢ 1 < n
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma nonsingular_iff_of_Y_eq_negY {P : Fin 3 → F} (hPz : P z ≠ 0) (hy : P y = W.negY P) :
    W.Nonsingular P ↔ W.Equation P ∧ eval P W.polynomialX ≠ 0

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
⊢ 2 * P y + W.a₁ * P x * P z + W.a₃ * P z ^ 3 = P y - (-P y - W.a₁ * P x * P z - W.a₃ * P z ^ 3)

Tactic:
ring1

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
⊢ (eval P) W.polynomialY = P y - W.negY P

Tactic:
rw [negY, eval_polynomialY]

Result:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
⊢ 2 * P y + W.a₁ * P x * P z + W.a₃ * P z ^ 3 = P y - (-P y - W.a₁ * P x * P z - W.a₃ * P z ^ 3)

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
hy' : (eval P) W.polynomialY = P y - W.negY P
⊢ W.Nonsingular P ↔ W.Equation P ∧ (eval P) W.polynomialX ≠ 0

Tactic:
rw [nonsingular_iff_of_Z_ne_zero hPz, hy', hy, sub_self, ne_self_iff_false, or_false]

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
⊢ W.Nonsingular P ↔ W.Equation P ∧ (eval P) W.polynomialX ≠ 0

Tactic:
have hy' : eval P W.polynomialY = P y - W.negY P := by rw [negY, eval_polynomialY]; ring1

Result:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
hy' : (eval P) W.polynomialY = P y - W.negY P
⊢ W.Nonsingular P ↔ W.Equation P ∧ (eval P) W.polynomialX ≠ 0
-- Mathlib/Data/Set/Prod.lean
theorem mk_preimage_prod_left_eq_empty (hb : b ∉ t) : (fun a => (a, b)) ⁻¹' s ×ˢ t = ∅

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
b : β
hb : b ∉ t
⊢ (fun a => (a, b)) ⁻¹' s ×ˢ t = ∅

Tactic:
ext a

Result:
case h
α : Type u_1
β : Type u_2
s : Set α
t : Set β
b : β
hb : b ∉ t
a : α
⊢ a ∈ (fun a => (a, b)) ⁻¹' s ×ˢ t ↔ a ∈ ∅

Proof state:
case h
α : Type u_1
β : Type u_2
s : Set α
t : Set β
b : β
hb : b ∉ t
a : α
⊢ a ∈ (fun a => (a, b)) ⁻¹' s ×ˢ t ↔ a ∈ ∅

Tactic:
simp [hb]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/SignedHahn.lean
theorem restrictNonposSeq_disjoint : Pairwise (Disjoint on restrictNonposSeq s i)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h : n ≠ m
⊢ MeasureTheory.SignedMeasure.restrictNonposSeq s i n ∩ MeasureTheory.SignedMeasure.restrictNonposSeq s i m = ∅

Tactic:
rcases lt_or_gt_of_ne h with (h | h)

Result:
case inl
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h✝ : n ≠ m
h : n < m
⊢ MeasureTheory.SignedMeasure.restrictNonposSeq s i n ∩ MeasureTheory.SignedMeasure.restrictNonposSeq s i m = ∅

case inr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h✝ : n ≠ m
h : n > m
⊢ MeasureTheory.SignedMeasure.restrictNonposSeq s i n ∩ MeasureTheory.SignedMeasure.restrictNonposSeq s i m = ∅

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h : n ≠ m
⊢ (Disjoint on MeasureTheory.SignedMeasure.restrictNonposSeq s i) n m

Tactic:
rw [Function.onFun, Set.disjoint_iff_inter_eq_empty]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h : n ≠ m
⊢ MeasureTheory.SignedMeasure.restrictNonposSeq s i n ∩ MeasureTheory.SignedMeasure.restrictNonposSeq s i m = ∅

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
⊢ Pairwise (Disjoint on MeasureTheory.SignedMeasure.restrictNonposSeq s i)

Tactic:
intro n m h

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h : n ≠ m
⊢ (Disjoint on MeasureTheory.SignedMeasure.restrictNonposSeq s i) n m

Proof state:
case inr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h✝ : n ≠ m
h : n > m
⊢ MeasureTheory.SignedMeasure.restrictNonposSeq s i n ∩ MeasureTheory.SignedMeasure.restrictNonposSeq s i m = ∅

Tactic:
rw [Set.inter_comm, restrictNonposSeq_disjoint' h]

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n m : ℕ
h✝ : n ≠ m
h : n < m
⊢ MeasureTheory.SignedMeasure.restrictNonposSeq s i n ∩ MeasureTheory.SignedMeasure.restrictNonposSeq s i m = ∅

Tactic:
rw [restrictNonposSeq_disjoint' h]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem iInf_coe {ι} (p : ι → LieSubmodule R L M) : (↑(⨅ i, p i) : Set M) = ⋂ i, ↑(p i)

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
p : ι → LieSubmodule R L M
⊢ ↑(⨅ i, p i) = ⋂ i, ↑(p i)

Tactic:
rw [iInf, sInf_coe]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
p : ι → LieSubmodule R L M
⊢ ⋂ s ∈ range fun i => p i, ↑s = ⋂ i, ↑(p i)

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Sort u_1
p : ι → LieSubmodule R L M
⊢ ⋂ s ∈ range fun i => p i, ↑s = ⋂ i, ↑(p i)

Tactic:
simp only [Set.mem_range, Set.iInter_exists, Set.iInter_iInter_eq']

Result:
no goals
-- Mathlib/Combinatorics/Configuration.lean
theorem card_points [Fintype P] [Finite L] : Fintype.card P = order P L ^ 2 + order P L + 1

Proof state:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } :=
  { toFun := fun q => ⟨⟨mkLine ⋯, ⋯⟩, ⟨↑q, ⋯⟩⟩, invFun := fun lq => ⟨↑lq.snd, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
h1 : Fintype.card { q // q ≠ p } + 1 = Fintype.card P
⊢ ∀ (l : { l // p ∈ l }), Fintype.card { q // q ∈ ↑l ∧ q ≠ p } = order P L

Tactic:
intro l

Result:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } :=
  { toFun := fun q => ⟨⟨mkLine ⋯, ⋯⟩, ⟨↑q, ⋯⟩⟩, invFun := fun lq => ⟨↑lq.snd, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
h1 : Fintype.card { q // q ≠ p } + 1 = Fintype.card P
l : { l // p ∈ l }
⊢ Fintype.card { q // q ∈ ↑l ∧ q ≠ p } = order P L

Proof state:
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
⊢ Fintype.card P = order P L ^ 2 + order P L + 1

Tactic:
let ϕ : { q // q ≠ p } ≃ Σl : { l : L // p ∈ l }, { q // q ∈ l.1 ∧ q ≠ p } :=
  { toFun := fun q => ⟨⟨mkLine q.2, (mkLine_ax q.2).2⟩, q, (mkLine_ax q.2).1, q.2⟩
    invFun := fun lq => ⟨lq.2, lq.2.2.2⟩
    left_inv := fun q => Subtype.ext rfl
    right_inv := fun lq =>
      Sigma.subtype_ext
        (Subtype.ext
          ((eq_or_eq (mkLine_ax lq.2.2.2).1 (mkLine_ax lq.2.2.2).2 lq.2.2.1 lq.1.2).resolve_left
            lq.2.2.2))
        rfl }

Result:
case intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Fintype P
inst✝ : Finite L
val✝ : Fintype L
p : P
ϕ : { q // q ≠ p } ≃ (l : { l // p ∈ l }) × { q // q ∈ ↑l ∧ q ≠ p } :=
  { toFun := fun q => ⟨⟨mkLine ⋯, ⋯⟩, ⟨↑q, ⋯⟩⟩, invFun := fun lq => ⟨↑lq.snd, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
⊢ Fintype.card P = order P L ^ 2 + order P L + 1