harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/SuccPred/Limit.lean
theorem isSuccLimit_iff [OrderBot α] : IsSuccLimit a ↔ a ≠ ⊥ ∧ IsSuccPrelimit a

Proof state:
α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
⊢ IsSuccLimit a ↔ a ≠ ⊥ ∧ IsSuccPrelimit a

Tactic:
rw [IsSuccLimit, isMin_iff_eq_bot]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_mul_div_cancel (a b c : G) : a * c * (b / c) = a * b

Proof state:
G : Type u_3
inst✝ : CommGroup G
a b c : G
⊢ a * c * (b / c) = a * b

Tactic:
rw [mul_assoc, mul_div_cancel]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_ofReal_im (x : ℝ) : (cos x).im = 0

Proof state:
x : ℝ
⊢ (cos ↑x).im = 0

Tactic:
rw [← ofReal_cos_ofReal_re, ofReal_im]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_range_succ_comm (f : ℕ → β) (n : ℕ) :
    (∏ x ∈ range (n + 1), f x) = f n * ∏ x ∈ range n, f x

Proof state:
β : Type u_4
inst✝ : CommMonoid β
f : ℕ → β
n : ℕ
⊢ ∏ x ∈ range (n + 1), f x = f n * ∏ x ∈ range n, f x

Tactic:
rw [range_succ, prod_insert not_mem_range_self]

Result:
no goals
-- Mathlib/Algebra/AddConstMap/Basic.lean
theorem map_sub_nat' [AddGroupWithOne G] [AddGroup H] [AddConstMapClass F G H 1 b]
    (f : F) (x : G) (n : ℕ) : f (x - n) = f x - n • b

Proof state:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
b : H
inst✝² : AddGroupWithOne G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H 1 b
f : F
x : G
n : ℕ
⊢ f (x - ↑n) = f x - n • b

Tactic:
simpa using map_sub_nsmul f x n

Result:
no goals
-- Mathlib/RingTheory/Binomial.lean
theorem choose_zero_succ (R) [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R] [BinomialRing R]
    (n : ℕ) : choose (0 : R) (n + 1) = 0

Proof state:
R : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
n : ℕ
⊢ choose 0 (n + 1) = 0

Tactic:
rw [choose, Nat.cast_succ, zero_sub, neg_add, neg_add_cancel_right, multichoose_succ_neg_natCast]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem subsingleton_of_einfsep_eq_top (hs : s.einfsep = ∞) : s.Subsingleton

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → edist x y = ⊤
⊢ s.Subsingleton

Tactic:
exact fun _ hx _ hy => of_not_not fun hxy => edist_ne_top _ _ (hs _ hx _ hy hxy)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hs : s.einfsep = ⊤
⊢ s.Subsingleton

Tactic:
rw [einfsep_top] at hs

Result:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → edist x y = ⊤
⊢ s.Subsingleton
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx?_append :
    (xs ++ ys : List α).findIdx? p =
      (xs.findIdx? p).or ((ys.findIdx? p).map fun i => i + xs.length)

Proof state:
case cons.isFalse
α : Type u_1
ys : List α
p : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : findIdx? p (tail✝ ++ ys) = (findIdx? p tail✝).or (Option.map (fun i => i + tail✝.length) (findIdx? p ys))
h✝ : p head✝ = false
⊢ (Option.map (fun i => i + 1) (findIdx? p tail✝)).or
      (Option.map ((fun i => i + 1) ∘ fun i => i + tail✝.length) (findIdx? p ys)) =
    (Option.map (fun i => i + 1) (findIdx? p tail✝)).or (Option.map (fun i => i + (tail✝.length + 1)) (findIdx? p ys))

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
xs ys : List α
p : α → Bool
⊢ findIdx? p (xs ++ ys) = (findIdx? p xs).or (Option.map (fun i => i + xs.length) (findIdx? p ys))

Tactic:
induction xs with simp
| cons _ _ _ => split <;> simp_all [Option.map_or', Option.map_map]; rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
ys : List α
p : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : findIdx? p (tail✝ ++ ys) = (findIdx? p tail✝).or (Option.map (fun i => i + tail✝.length) (findIdx? p ys))
⊢ (if p head✝ = true then some 0 else Option.map (fun i => i + 1) (findIdx? p (tail✝ ++ ys))) =
    (if p head✝ = true then some 0 else Option.map (fun i => i + 1) (findIdx? p tail✝)).or
      (Option.map (fun i => i + (tail✝.length + 1)) (findIdx? p ys))

Tactic:
split <;> simp_all [Option.map_or', Option.map_map]

Result:
case cons.isFalse
α : Type u_1
ys : List α
p : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : findIdx? p (tail✝ ++ ys) = (findIdx? p tail✝).or (Option.map (fun i => i + tail✝.length) (findIdx? p ys))
h✝ : p head✝ = false
⊢ (Option.map (fun i => i + 1) (findIdx? p tail✝)).or
      (Option.map ((fun i => i + 1) ∘ fun i => i + tail✝.length) (findIdx? p ys)) =
    (Option.map (fun i => i + 1) (findIdx? p tail✝)).or (Option.map (fun i => i + (tail✝.length + 1)) (findIdx? p ys))
-- Mathlib/Data/Rel.lean
theorem inv_bot : (⊥ : Rel α β).inv = (⊥ : Rel β α)

Proof state:
α : Type u_1
β : Type u_2
⊢ ⊥.inv = ⊥

Tactic:
simp [Bot.bot, inv, Function.flip_def]

Result:
no goals
-- Mathlib/Algebra/Group/Support.lean
theorem mulSupport_mulSingle [DecidableEq B] :
    mulSupport (mulSingle a b) = if b = 1 then ∅ else {a}

Proof state:
A : Type u_1
B : Type u_2
inst✝² : DecidableEq A
inst✝¹ : One B
a : A
b : B
inst✝ : DecidableEq B
⊢ mulSupport (mulSingle a b) = if b = 1 then ∅ else {a}

Tactic:
split_ifs with h <;> simp [h]

Result:
no goals
-- Mathlib/Algebra/Category/AlgebraCat/Basic.lean
lemma hom_inv_apply {A B : AlgebraCat.{v} R} (e : A ≅ B) (x : B) : e.hom (e.inv x) = x

Proof state:
R : Type u
inst✝ : CommRing R
A B : AlgebraCat R
e : A ≅ B
x : ↑B
⊢ (ConcreteCategory.hom (e.inv ≫ e.hom)) x = x

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
A B : AlgebraCat R
e : A ≅ B
x : ↑B
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) x) = x

Tactic:
rw [← comp_apply]

Result:
R : Type u
inst✝ : CommRing R
A B : AlgebraCat R
e : A ≅ B
x : ↑B
⊢ (ConcreteCategory.hom (e.inv ≫ e.hom)) x = x
-- Mathlib/Data/Int/WithZero.lean
theorem toNNReal_le_one_iff {e : ℝ≥0} {m : ℤₘ₀} (he : 1 < e) :
    toNNReal (ne_zero_of_lt he) m ≤ 1 ↔ m ≤ 1

Proof state:
e : ℝ≥0
m : ℤₘ₀
he : 1 < e
⊢ (toNNReal ⋯) m ≤ 1 ↔ m ≤ 1

Tactic:
have : 1 = (toNNReal (ne_zero_of_lt he)) 1 := rfl

Result:
e : ℝ≥0
m : ℤₘ₀
he : 1 < e
this : 1 = (toNNReal ⋯) 1
⊢ (toNNReal ⋯) m ≤ 1 ↔ m ≤ 1

Proof state:
e : ℝ≥0
m : ℤₘ₀
he : 1 < e
this : 1 = (toNNReal ⋯) 1
⊢ (toNNReal ⋯) m ≤ 1 ↔ m ≤ 1

Tactic:
simp_rw [this]

Result:
e : ℝ≥0
m : ℤₘ₀
he : 1 < e
this : 1 = (toNNReal ⋯) 1
⊢ (toNNReal ⋯) m ≤ (toNNReal ⋯) 1 ↔ m ≤ 1

Proof state:
e : ℝ≥0
m : ℤₘ₀
he : 1 < e
this : 1 = (toNNReal ⋯) 1
⊢ (toNNReal ⋯) m ≤ (toNNReal ⋯) 1 ↔ m ≤ 1

Tactic:
exact StrictMono.le_iff_le (toNNReal_strictMono he)

Result:
no goals
-- Mathlib/Data/DFinsupp/Multiset.lean
theorem toDFinsupp_le_toDFinsupp : toDFinsupp s ≤ toDFinsupp t ↔ s ≤ t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ toDFinsupp s ≤ toDFinsupp t ↔ s ≤ t

Tactic:
simp [Multiset.le_iff_count, DFinsupp.le_def]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Basic.lean
lemma shiftFunctorCompIsoId_zero_zero_inv_app (X : C) :
    (shiftFunctorCompIsoId C 0 0 (add_zero 0)).inv.app X =
      (shiftFunctorZero C A).inv.app X ≫ ((shiftFunctorZero C A).inv.app X)⟦0⟧'

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
⊢ (shiftFunctorCompIsoId C 0 0 ⋯).inv.app X =
    (shiftFunctorZero C A).inv.app X ≫ (shiftFunctor C 0).map ((shiftFunctorZero C A).inv.app X)

Tactic:
simp [shiftFunctorCompIsoId, shiftFunctorAdd'_zero_add_hom_app]

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem hasSum_geometric_of_lt_one {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) :
    HasSum (fun n : ℕ ↦ r ^ n) (1 - r)⁻¹ :=
  have : r ≠ 1 := ne_of_lt h₂
  have : Tendsto (fun n ↦ (r ^ n - 1) * (r - 1)⁻¹) atTop (𝓝 ((0 - 1) * (r - 1)⁻¹)) :=
    ((tendsto_pow_atTop_nhds_zero_of_lt_one h₁ h₂).sub tendsto_const_nhds).mul tendsto_const_nhds
  (hasSum_iff_tendsto_nat_of_nonneg (pow_nonneg h₁) _).mpr <| by
    simp_all [neg_inv, geom_sum_eq, div_eq_mul_inv]

Proof state:
r : ℝ
h₁ : 0 ≤ r
h₂ : r < 1
this✝ : r ≠ 1
this : Tendsto (fun n => (r ^ n - 1) * (r - 1)⁻¹) atTop (𝓝 ((0 - 1) * (r - 1)⁻¹))
⊢ Tendsto (fun n => ∑ i ∈ Finset.range n, r ^ i) atTop (𝓝 (1 - r)⁻¹)

Tactic:
simp_all [neg_inv, geom_sum_eq, div_eq_mul_inv]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem opNorm_smul_le (c : 𝕜') (f : ContinuousMultilinearMap 𝕜 E G) : ‖c • f‖ ≤ ‖c‖ * ‖f‖ :=
  (c • f).opNorm_le_bound (mul_nonneg (norm_nonneg _) (opNorm_nonneg _)) fun m ↦ by
    rw [smul_apply, norm_smul, mul_assoc]
    exact mul_le_mul_of_nonneg_left (le_opNorm _ _) (norm_nonneg _)

Proof state:
𝕜 : 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 ι
𝕜' : Type u_1
inst✝² : NormedField 𝕜'
inst✝¹ : NormedSpace 𝕜' G
inst✝ : SMulCommClass 𝕜 𝕜' G
c : 𝕜'
f : ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
⊢ ‖(c • f) m‖ ≤ ‖c‖ * ‖f‖ * ∏ i : ι, ‖m i‖

Tactic:
rw [smul_apply, norm_smul, mul_assoc]

Result:
𝕜 : 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 ι
𝕜' : Type u_1
inst✝² : NormedField 𝕜'
inst✝¹ : NormedSpace 𝕜' G
inst✝ : SMulCommClass 𝕜 𝕜' G
c : 𝕜'
f : ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
⊢ ‖c‖ * ‖f m‖ ≤ ‖c‖ * (‖f‖ * ∏ i : ι, ‖m i‖)

Proof state:
𝕜 : 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 ι
𝕜' : Type u_1
inst✝² : NormedField 𝕜'
inst✝¹ : NormedSpace 𝕜' G
inst✝ : SMulCommClass 𝕜 𝕜' G
c : 𝕜'
f : ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
⊢ ‖c‖ * ‖f m‖ ≤ ‖c‖ * (‖f‖ * ∏ i : ι, ‖m i‖)

Tactic:
exact mul_le_mul_of_nonneg_left (le_opNorm _ _) (norm_nonneg _)

Result:
no goals
-- Mathlib/Algebra/Module/Presentation/Basic.lean
@[simp]
lemma ofQuotient_fromQuotient : (ofQuotient relations).fromQuotient = .id

Proof state:
A : Type u
inst✝ : Ring A
relations : Relations A
⊢ (ofQuotient relations).fromQuotient = LinearMap.id

Tactic:
aesop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey?_eraseKey_self [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α}
    (hl : DistinctKeys l) : getKey? k (eraseKey k l) = none

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k : α
hl : DistinctKeys l
⊢ getKey? k (eraseKey k l) = none

Tactic:
simp [getKey?_eq_getEntry?, getEntry?_eraseKey_self hl]

Result:
no goals
-- Mathlib/CategoryTheory/Enriched/FunctorCategory.lean
@[reassoc (attr := simp)]
lemma enrichedComp_π (j : J) :
    enrichedComp V F₁ F₂ F₃ ≫ end_.π _ j =
      (end_.π (diagram V F₁ F₂) j ⊗ end_.π (diagram V F₂ F₃) j) ≫ eComp V _ _ _

Proof state:
V : Type u₁
inst✝⁷ : Category.{v₁, u₁} V
inst✝⁶ : MonoidalCategory V
C : Type u₂
inst✝⁵ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁴ : Category.{v₃, u₃} J
inst✝³ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ : J ⥤ C
inst✝² : HasEnrichedHom V F₁ F₂
inst✝¹ : HasEnrichedHom V F₂ F₃
inst✝ : HasEnrichedHom V F₁ F₃
j : J
⊢ enrichedComp V F₁ F₂ F₃ ≫ end_.π (diagram V F₁ F₃) j =
    (end_.π (diagram V F₁ F₂) j ⊗ end_.π (diagram V F₂ F₃) j) ≫
      eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₃.obj j)

Tactic:
simp [enrichedComp]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
theorem Colorable.cliqueFree {n m : ℕ} (hc : G.Colorable n) (hm : n < m) :
    G.CliqueFree m

Proof state:
V : Type u
G : SimpleGraph V
n m : ℕ
hc : G.Colorable n
hm : n < m
⊢ G.CliqueFree m

Tactic:
by_contra h

Result:
V : Type u
G : SimpleGraph V
n m : ℕ
hc : G.Colorable n
hm : n < m
h : ¬G.CliqueFree m
⊢ False

Proof state:
V : Type u
G : SimpleGraph V
n m : ℕ
hc : G.Colorable n
hm : n < m
h : ¬G.CliqueFree m
⊢ False

Tactic:
simp only [CliqueFree, isNClique_iff, not_forall, Classical.not_not] at h

Result:
V : Type u
G : SimpleGraph V
n m : ℕ
hc : G.Colorable n
hm : n < m
h : ∃ x, G.IsClique ↑x ∧ x.card = m
⊢ False

Proof state:
V : Type u
G : SimpleGraph V
n m : ℕ
hc : G.Colorable n
hm : n < m
h : ∃ x, G.IsClique ↑x ∧ x.card = m
⊢ False

Tactic:
obtain ⟨s, h, rfl⟩ := h

Result:
case intro.intro
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
s : Finset V
h : G.IsClique ↑s
hm : n < s.card
⊢ False

Proof state:
case intro.intro
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
s : Finset V
h : G.IsClique ↑s
hm : n < s.card
⊢ False

Tactic:
exact Nat.lt_le_asymm hm (h.card_le_of_colorable hc)

Result:
no goals
-- Mathlib/Algebra/Group/Defs.lean
theorem div_self' (a : G) : a / a = 1

Proof state:
G : Type u_1
inst✝ : Group G
a : G
⊢ a / a = 1

Tactic:
rw [div_eq_mul_inv, mul_inv_cancel a]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem whiskerLeft_rightUnitor_inv (X Y : C) :
    X ◁ (ρ_ Y).inv = (ρ_ (X ⊗ Y)).inv ≫ (α_ X Y (𝟙_ C)).hom :=
  eq_of_inv_eq_inv (by simp)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ inv (X ◁ (ρ_ Y).inv) = inv ((ρ_ (X ⊗ Y)).inv ≫ (α_ X Y (𝟙_ C)).hom)

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean
theorem infinite_iff_in_eventualRange {K : (Finset V)ᵒᵖ} (C : G.componentComplFunctor.obj K) :
    C.supp.Infinite ↔ C ∈ G.componentComplFunctor.eventualRange K

Proof state:
V : Type u
G : SimpleGraph V
K : (Finset V)ᵒᵖ
C : G.componentComplFunctor.obj K
⊢ (∀ (L : Finset V) (h : Opposite.unop K ⊆ L), ∃ D, ComponentCompl.hom h D = C) ↔
    ∀ (i : (Finset V)ᵒᵖ) (i_1 : i ⟶ K), ∃ y, ComponentCompl.hom ⋯ y = C

Tactic:
exact
  ⟨fun h Lop KL => h Lop.unop (le_of_op_hom KL), fun h L KL =>
    h (Opposite.op L) (opHomOfLE KL)⟩

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
K : (Finset V)ᵒᵖ
C : G.componentComplFunctor.obj K
⊢ (ComponentCompl.supp C).Infinite ↔ C ∈ G.componentComplFunctor.eventualRange K

Tactic:
simp only [C.infinite_iff_in_all_ranges, CategoryTheory.Functor.eventualRange, Set.mem_iInter,
  Set.mem_range, componentComplFunctor_map]

Result:
V : Type u
G : SimpleGraph V
K : (Finset V)ᵒᵖ
C : G.componentComplFunctor.obj K
⊢ (∀ (L : Finset V) (h : Opposite.unop K ⊆ L), ∃ D, ComponentCompl.hom h D = C) ↔
    ∀ (i : (Finset V)ᵒᵖ) (i_1 : i ⟶ K), ∃ y, ComponentCompl.hom ⋯ y = C
-- Mathlib/Algebra/Lie/EngelSubalgebra.lean
lemma mem_engel_iff (x y : L) :
    y ∈ engel R x ↔ ∃ n : ℕ, ((ad R L x) ^ n) y = 0 :=
  (Module.End.mem_maxGenEigenspace _ _ _).trans <| by simp only [zero_smul, sub_zero]

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x y : L
⊢ (∃ k, (((ad R L) x - 0 • 1) ^ k) y = 0) ↔ ∃ n, ((ad R L) x ^ n) y = 0

Tactic:
simp only [zero_smul, sub_zero]

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem one_lt_rootMultiplicity_iff_isRoot_gcd
    [GCDMonoid R[X]] {p : R[X]} {t : R} (h : p ≠ 0) :
    1 < p.rootMultiplicity t ↔ (gcd p (derivative p)).IsRoot t

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : GCDMonoid R[X]
p : R[X]
t : R
h : p ≠ 0
⊢ 1 < rootMultiplicity t p ↔ (gcd p (derivative p)).IsRoot t

Tactic:
simp_rw [one_lt_rootMultiplicity_iff_isRoot h, ← dvd_iff_isRoot, dvd_gcd_iff]

Result:
no goals
-- Mathlib/Order/PrimeIdeal.lean
theorem I_isProper : IsProper IF.I

Proof state:
P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
w : P
h : w ∈ ↑IF.F
⊢ w ∉ IF.I

Tactic:
rwa [← IF.compl_I_eq_F] at h

Result:
no goals

Proof state:
case intro
P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
w : P
h : w ∈ ↑IF.F
⊢ IF.I.IsProper

Tactic:
apply isProper_of_not_mem (_ : w ∉ IF.I)

Result:
P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
w : P
h : w ∈ ↑IF.F
⊢ w ∉ IF.I

Proof state:
P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
⊢ IF.I.IsProper

Tactic:
obtain ⟨w, h⟩ := IF.F.nonempty

Result:
case intro
P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
w : P
h : w ∈ ↑IF.F
⊢ IF.I.IsProper
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma baseChange_polynomial : (W'.baseChange B).toProjective.polynomial =
    MvPolynomial.map f (W'.baseChange A).toProjective.polynomial

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (baseChange W' B).toProjective.polynomial = (MvPolynomial.map ↑f) (baseChange W' A).toProjective.polynomial

Tactic:
rw [← map_polynomial, map_baseChange]

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/Basic.lean
theorem map_ne_one [Nontrivial B] {R : Type*} [Semiring R] [Nontrivial R] (f : A →+* R) :
    (minpoly A x).map f ≠ 1

Proof state:
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Algebra A B
x : B
inst✝² : Nontrivial B
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : A →+* R
⊢ map f (minpoly A x) ≠ 1

Tactic:
by_cases hx : IsIntegral A x

Result:
case pos
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Algebra A B
x : B
inst✝² : Nontrivial B
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : A →+* R
hx : IsIntegral A x
⊢ map f (minpoly A x) ≠ 1

case neg
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Algebra A B
x : B
inst✝² : Nontrivial B
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : A →+* R
hx : ¬IsIntegral A x
⊢ map f (minpoly A x) ≠ 1

Proof state:
case neg
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Algebra A B
x : B
inst✝² : Nontrivial B
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : A →+* R
hx : ¬IsIntegral A x
⊢ map f (minpoly A x) ≠ 1

Tactic:
rw [eq_zero hx, Polynomial.map_zero]

Result:
case neg
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Algebra A B
x : B
inst✝² : Nontrivial B
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : A →+* R
hx : ¬IsIntegral A x
⊢ 0 ≠ 1

Proof state:
case pos
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Algebra A B
x : B
inst✝² : Nontrivial B
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : A →+* R
hx : IsIntegral A x
⊢ map f (minpoly A x) ≠ 1

Tactic:
exact mt ((monic hx).eq_one_of_map_eq_one f) (ne_one A x)

Result:
no goals

Proof state:
case neg
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Ring B
inst✝³ : Algebra A B
x : B
inst✝² : Nontrivial B
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : A →+* R
hx : ¬IsIntegral A x
⊢ 0 ≠ 1

Tactic:
exact zero_ne_one

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/VectorSpace.lean
theorem LinearMap.exists_extend {p : Submodule K V} (f : p →ₗ[K] V') :
    ∃ g : V →ₗ[K] V', g.comp p.subtype = f :=
  let ⟨g, hg⟩ := p.subtype.exists_leftInverse_of_injective p.ker_subtype
  ⟨f.comp g, by rw [LinearMap.comp_assoc, hg, f.comp_id]⟩

Proof state:
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
p : Submodule K V
f : ↥p →ₗ[K] V'
g : V →ₗ[K] ↥p
hg : g ∘ₗ p.subtype = id
⊢ (f ∘ₗ g) ∘ₗ p.subtype = f

Tactic:
rw [LinearMap.comp_assoc, hg, f.comp_id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem Const.wfImp_getThenInsertIfNew? {β : Type v} [BEq α] [Hashable α] [EquivBEq α]
    [LawfulHashable α] {m : Raw₀ α (fun _ => β)} {a : α} {b : β} (h : Raw.WFImp m.1) :
    Raw.WFImp (Const.getThenInsertIfNew? m a b).2.1

Proof state:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
a : α
b : β
h : Raw.WFImp m.val
⊢ Raw.WFImp (getThenInsertIfNew? m a b).snd.val

Tactic:
rw [getThenInsertIfNew?_eq_insertIfNewₘ]

Result:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
a : α
b : β
h : Raw.WFImp m.val
⊢ Raw.WFImp (m.insertIfNewₘ a b).val

Proof state:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
a : α
b : β
h : Raw.WFImp m.val
⊢ Raw.WFImp (m.insertIfNewₘ a b).val

Tactic:
exact wfImp_insertIfNewₘ h

Result:
no goals
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem prod_univ_add {M : Type*} [CommMonoid M] {a b : ℕ} (f : Fin (a + b) → M) :
    (∏ i : Fin (a + b), f i) = (∏ i : Fin a, f (castAdd b i)) * ∏ i : Fin b, f (natAdd a i)

Proof state:
M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
⊢ ∀ (x : Fin (a + b)), f x = f (finSumFinEquiv.toFun (finSumFinEquiv.symm x))

Tactic:
intro x

Result:
M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
x : Fin (a + b)
⊢ f x = f (finSumFinEquiv.toFun (finSumFinEquiv.symm x))

Proof state:
M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
⊢ ∏ x : Fin a ⊕ Fin b, f (finSumFinEquiv.toFun x) = (∏ i : Fin a, f (castAdd b i)) * ∏ i : Fin b, f (natAdd a i)

Tactic:
apply Fintype.prod_sum_type

Result:
no goals

Proof state:
M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
⊢ ∏ i : Fin (a + b), f i = (∏ i : Fin a, f (castAdd b i)) * ∏ i : Fin b, f (natAdd a i)

Tactic:
rw [Fintype.prod_equiv finSumFinEquiv.symm f fun i => f (finSumFinEquiv.toFun i)]

Result:
M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
⊢ ∏ x : Fin a ⊕ Fin b, f (finSumFinEquiv.toFun x) = (∏ i : Fin a, f (castAdd b i)) * ∏ i : Fin b, f (natAdd a i)

M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
⊢ ∀ (x : Fin (a + b)), f x = f (finSumFinEquiv.toFun (finSumFinEquiv.symm x))

Proof state:
M : Type u_3
inst✝ : CommMonoid M
a b : ℕ
f : Fin (a + b) → M
x : Fin (a + b)
⊢ f x = f (finSumFinEquiv.toFun (finSumFinEquiv.symm x))

Tactic:
simp only [Equiv.toFun_as_coe, Equiv.apply_symm_apply]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
theorem null_iff_toMeasure_null (ν : ProbabilityMeasure Ω) (s : Set Ω) :
    ν s = 0 ↔ (ν : Measure Ω) s = 0 :=
  ⟨fun h ↦ by rw [← ennreal_coeFn_eq_coeFn_toMeasure, h, ENNReal.coe_zero],
   fun h ↦ congrArg ENNReal.toNNReal h⟩

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
ν : ProbabilityMeasure Ω
s : Set Ω
h : ν s = 0
⊢ ↑ν s = 0

Tactic:
rw [← ennreal_coeFn_eq_coeFn_toMeasure, h, ENNReal.coe_zero]

Result:
no goals
-- Mathlib/Data/Rel.lean
theorem image_eq (f : α → β) (s : Set α) : f '' s = (Function.graph f).image s

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ f '' s = (Function.graph f).image s

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem Bool.or_eq_of_eq_true_left {a b : Bool} (h : a = true) : (a || b) = true

Proof state:
a b : Bool
h : a = true
⊢ (a || b) = true

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
lemma le_posPart {a : A} (ha : IsSelfAdjoint a

Proof state:
A : Type u_1
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ a ≤ a⁺

Tactic:
simpa [posPart_sub_negPart a] using sub_le_self a⁺ (negPart_nonneg a)

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem orderOf_one : orderOf (1 : G) = 1

Proof state:
G : Type u_1
inst✝ : Monoid G
⊢ orderOf 1 = 1

Tactic:
rw [orderOf, ← minimalPeriod_id (x := (1 : G)), ← one_mul_eq_id]

Result:
no goals
-- Mathlib/RingTheory/Localization/NumDen.lean
theorem eq_zero_of_num_eq_zero {x : K} (h : num A x = 0) : x = 0 :=
  (num_mul_den_eq_num_iff_eq' (A := A)).mp (by rw [zero_mul, h, RingHom.map_zero])

Proof state:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
h : num A x = 0
⊢ 0 * (algebraMap A K) ↑(den A x) = (algebraMap A K) (num A x)

Tactic:
rw [zero_mul, h, RingHom.map_zero]

Result:
no goals