harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicative.lean
theorem multiplicative_of_coprime (f : α → β) (a b : α) (h0 : f 0 = 0)
    (h1 : ∀ {x y}, IsUnit y → f (x * y) = f x * f y)
    (hpr : ∀ {p} (i : ℕ), Prime p → f (p ^ i) = f p ^ i)
    (hcp : ∀ {x y}, IsRelPrime x y → f (x * y) = f x * f y) :
    f (a * b) = f a * f b

Proof state:
case intro.intro.e_a.e_a
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * ↑ua = a
ub : αˣ
b_eq : (normalizedFactors b).prod * ↑ub = b
⊢ ∀ x ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
    x ∉ normalizedFactors b → id x ^ Multiset.count x (normalizedFactors b) = 1

Tactic:
intro p _ hpb

Result:
case intro.intro.e_a.e_a
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CancelCommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * ↑ua = a
ub : αˣ
b_eq : (normalizedFactors b).prod * ↑ub = b
p : α
a✝ : p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset
hpb : p ∉ normalizedFactors b
⊢ id p ^ Multiset.count p (normalizedFactors b) = 1
-- Mathlib/SetTheory/Game/PGame.lean
lemma Identical.add_right {x₁ x₂ y} : x₁ ≡ x₂ → x₁ + y ≡ x₂ + y :=
  match x₁, x₂, y with
  | mk x₁l x₁r x₁L x₁R, mk x₂l x₂r x₂L x₂R, mk yl yr yL yR => by
    intro h
    refine ⟨⟨?_, ?_⟩, ⟨?_, ?_⟩⟩ <;> rintro (_ | _) <;> try exact ⟨.inr _, h.add_right⟩
    · exact (h.1.1 _).elim (⟨.inl ·, ·.add_right⟩)
    · exact (h.1.2 _).elim (⟨.inl ·, ·.add_right⟩)
    · exact (h.2.1 _).elim (⟨.inl ·, ·.add_right⟩)
    · exact (h.2.2 _).elim (⟨.inl ·, ·.add_right⟩)
  termination_by (x₁, x₂, y)

Proof state:
x₁ x₂ y : PGame
x₁l x₁r : Type u_1
x₁L : x₁l → PGame
x₁R : x₁r → PGame
x₂l x₂r : Type u_1
x₂L : x₂l → PGame
x₂R : x₂r → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
⊢ mk x₁l x₁r x₁L x₁R ≡ mk x₂l x₂r x₂L x₂R → mk x₁l x₁r x₁L x₁R + mk yl yr yL yR ≡ mk x₂l x₂r x₂L x₂R + mk yl yr yL yR

Tactic:
intro h

Result:
x₁ x₂ y : PGame
x₁l x₁r : Type u_1
x₁L : x₁l → PGame
x₁R : x₁r → PGame
x₂l x₂r : Type u_1
x₂L : x₂l → PGame
x₂R : x₂r → PGame
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
h : mk x₁l x₁r x₁L x₁R ≡ mk x₂l x₂r x₂L x₂R
⊢ mk x₁l x₁r x₁L x₁R + mk yl yr yL yR ≡ mk x₂l x₂r x₂L x₂R + mk yl yr yL yR
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addX_of_X_eq' {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q)
    (hx : P x * Q z ^ 2 = Q x * P z ^ 2) :
    W'.addX P Q * (P z * Q z) ^ 2 = (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 2

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ W'.addX P Q * (P z * Q z) ^ 2 = (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 2

Tactic:
rw [addX_eq' hP hQ, addZ_of_X_eq hx]

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 2 + W'.a₁ * (P y * Q z ^ 3 - Q y * P z ^ 3) * P z * Q z * 0 -
          W'.a₂ * P z ^ 2 * Q z ^ 2 * 0 ^ 2 -
        P x * Q z ^ 2 * 0 ^ 2 -
      Q x * P z ^ 2 * 0 ^ 2 =
    (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 2

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 2 + W'.a₁ * (P y * Q z ^ 3 - Q y * P z ^ 3) * P z * Q z * 0 -
          W'.a₂ * P z ^ 2 * Q z ^ 2 * 0 ^ 2 -
        P x * Q z ^ 2 * 0 ^ 2 -
      Q x * P z ^ 2 * 0 ^ 2 =
    (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 2

Tactic:
ring1

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem contains_eq_containsKey [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α]
    {m : Raw₀ α β} (hm : Raw.WFImp m.1) {a : α} :
    m.contains a = containsKey a (toListModel m.1.buckets)

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
hm : Raw.WFImp m.val
a : α
⊢ m.contains a = containsKey a (toListModel m.val.buckets)

Tactic:
rw [contains_eq_containsₘ, containsₘ_eq_containsKey hm]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Spectrum.lean
/-- rank of a hermitian matrix is the number of nonzero eigenvalues of the hermitian matrix -/
lemma rank_eq_card_non_zero_eigs : A.rank = Fintype.card {i // hA.eigenvalues i ≠ 0}

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
⊢ A.rank = Fintype.card { i // hA.eigenvalues i ≠ 0 }

Tactic:
rw [rank_eq_rank_diagonal hA, Matrix.rank_diagonal]

Result:
no goals
-- Mathlib/Data/Complex/Norm.lean
@[simp] lemma norm_I : ‖I‖ = 1

Proof state:
⊢ ‖I‖ = 1

Tactic:
simp [norm]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem weightedSMul_nonneg (s : Set α) (x : ℝ) (hx : 0 ≤ x) : 0 ≤ weightedSMul μ s x

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
x : ℝ
hx : 0 ≤ x
⊢ 0 ≤ (weightedSMul μ s) x

Tactic:
simp only [weightedSMul, Algebra.id.smul_eq_mul, coe_smul', _root_.id, coe_id', Pi.smul_apply]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
x : ℝ
hx : 0 ≤ x
⊢ 0 ≤ (μ s).toReal * x

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
x : ℝ
hx : 0 ≤ x
⊢ 0 ≤ (μ s).toReal * x

Tactic:
exact mul_nonneg toReal_nonneg hx

Result:
no goals
-- Mathlib/Data/List/Infix.lean
theorem mem_tails : ∀ s t : List α, s ∈ tails t ↔ s <:+ t
  | s, [] => by
    simp only [tails, mem_singleton, suffix_nil]
  | s, a :: t => by
    simp only [tails, mem_cons, mem_tails s t]
    exact
      show s = a :: t ∨ s <:+ t ↔ s <:+ a :: t from
        ⟨fun o =>
          match s, t, o with
          | _, t, Or.inl rfl => suffix_rfl
          | s, _, Or.inr ⟨l, rfl⟩ => ⟨a :: l, rfl⟩,
          fun e =>
          match s, t, e with
          | _, t, ⟨[], rfl⟩ => Or.inl rfl
          | s, t, ⟨b :: l, he⟩ => List.noConfusion he fun _ lt => Or.inr ⟨l, lt⟩⟩

Proof state:
α : Type u_1
s : List α
a : α
t : List α
⊢ s = a :: t ∨ s <:+ t ↔ s <:+ a :: t

Tactic:
exact
  show s = a :: t ∨ s <:+ t ↔ s <:+ a :: t from
    ⟨fun o =>
      match s, t, o with
      | _, t, Or.inl rfl => suffix_rfl
      | s, _, Or.inr ⟨l, rfl⟩ => ⟨a :: l, rfl⟩,
      fun e =>
      match s, t, e with
      | _, t, ⟨[], rfl⟩ => Or.inl rfl
      | s, t, ⟨b :: l, he⟩ => List.noConfusion he fun _ lt => Or.inr ⟨l, lt⟩⟩

Result:
no goals

Proof state:
α : Type u_1
s : List α
⊢ s ∈ [].tails ↔ s <:+ []

Tactic:
simp only [tails, mem_singleton, suffix_nil]

Result:
no goals

Proof state:
α : Type u_1
s : List α
a : α
t : List α
⊢ s ∈ (a :: t).tails ↔ s <:+ a :: t

Tactic:
simp only [tails, mem_cons, mem_tails s t]

Result:
α : Type u_1
s : List α
a : α
t : List α
⊢ s = a :: t ∨ s <:+ t ↔ s <:+ a :: t
-- Mathlib/FieldTheory/AbelRuffini.lean
theorem gal_X_pow_sub_C_isSolvable_aux (n : ℕ) (a : F)
    (h : (X ^ n - 1 : F[X]).Splits (RingHom.id F)) : IsSolvable (X ^ n - C a).Gal

Proof state:
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ✝ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : b ^ n = (algebraMap F (X ^ n - C a).SplittingField) a
hb' : b ≠ 0
σ : (X ^ n - C a).Gal
⊢ ∃ c, σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c

Tactic:
have key : (σ b / b) ^ n = 1 := by rw [div_pow, ← map_pow, hb, σ.commutes, div_self ha']

Result:
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ✝ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : b ^ n = (algebraMap F (X ^ n - C a).SplittingField) a
hb' : b ≠ 0
σ : (X ^ n - C a).Gal
key : (σ b / b) ^ n = 1
⊢ ∃ c, σ b = b * (algebraMap F (X ^ n - C a).SplittingField) c

Proof state:
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
c : (X ^ n - C a).SplittingField
hc : c ^ n = 1
⊢ (aeval c) (Polynomial.map (RingHom.id F) (X ^ n - 1)) = 0

Tactic:
rwa [map_id, map_sub, sub_eq_zero, aeval_X_pow, aeval_one]

Result:
no goals

Proof state:
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : b ^ n = (algebraMap F (X ^ n - C a).SplittingField) a
hb' : b = 0
⊢ False

Tactic:
rw [hb', zero_pow hn] at hb

Result:
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : Splits (RingHom.id F) (X ^ n - 1)
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ τ : (X ^ n - C a).Gal
b : (X ^ n - C a).SplittingField
hb : 0 = (algebraMap F (X ^ n - C a).SplittingField) a
hb' : b = 0
⊢ False
-- Mathlib/GroupTheory/Submonoid/Inverses.lean
theorem leftInvEquiv_symm_eq_inv (x : S) : ((S.leftInvEquiv hS).symm x : M) = (x : M)⁻¹

Proof state:
M : Type u_1
inst✝ : CommGroup M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S
⊢ ↑((S.leftInvEquiv hS).symm x) = (↑x)⁻¹

Tactic:
rw [← mul_right_inj (x : M), mul_inv_cancel, mul_leftInvEquiv_symm]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Restrict.lean
lemma resLE_appLE {U : Y.Opens} {V : X.Opens} (e : V ≤ f ⁻¹ᵁ U)
    (O : U.toScheme.Opens) (W : V.toScheme.Opens) (e' : W ≤ resLE f U V e ⁻¹ᵁ O) :
    (f.resLE U V e).appLE O W e' =
      f.appLE (U.ι ''ᵁ O) (V.ι ''ᵁ W) ((le_preimage_resLE_iff f e O W).mp e')

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U).Opens
W : (↑V).Opens
e' : W ≤ resLE f U V e ⁻¹ᵁ O
⊢ app f (U.ι ''ᵁ O) ≫ X.presheaf.map (homOfLE ⋯).op ≫ X.presheaf.map (homOfLE ⋯).op ≫ X.presheaf.map (homOfLE ⋯).op =
    app f (U.ι ''ᵁ O) ≫ X.presheaf.map (homOfLE ⋯).op

Tactic:
rw [← X.presheaf.map_comp, ← X.presheaf.map_comp]

Result:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U).Opens
W : (↑V).Opens
e' : W ≤ resLE f U V e ⁻¹ᵁ O
⊢ app f (U.ι ''ᵁ O) ≫ X.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op ≫ (homOfLE ⋯).op) =
    app f (U.ι ''ᵁ O) ≫ X.presheaf.map (homOfLE ⋯).op

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U).Opens
W : (↑V).Opens
e' : W ≤ resLE f U V e ⁻¹ᵁ O
⊢ app f (U.ι ''ᵁ O) ≫ X.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op ≫ (homOfLE ⋯).op) =
    app f (U.ι ''ᵁ O) ≫ X.presheaf.map (homOfLE ⋯).op

Tactic:
rfl

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U).Opens
W : (↑V).Opens
e' : W ≤ resLE f U V e ⁻¹ᵁ O
⊢ appLE (resLE f U V e) O W e' = appLE f (U.ι ''ᵁ O) (V.ι ''ᵁ W) ⋯

Tactic:
simp only [appLE, resLE, comp_coeBase, Opens.map_comp_obj, comp_app, morphismRestrict_app',
  homOfLE_leOfHom, homOfLE_app, Category.assoc, Opens.toScheme_presheaf_map, Quiver.Hom.unop_op,
  opensFunctor_map_homOfLE]

Result:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U).Opens
W : (↑V).Opens
e' : W ≤ resLE f U V e ⁻¹ᵁ O
⊢ app f (U.ι ''ᵁ O) ≫ X.presheaf.map (homOfLE ⋯).op ≫ X.presheaf.map (homOfLE ⋯).op ≫ X.presheaf.map (homOfLE ⋯).op =
    app f (U.ι ''ᵁ O) ≫ X.presheaf.map (homOfLE ⋯).op
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem mod_injOn_Ico (n a : ℕ) : Set.InjOn (· % a) (Finset.Ico n (n + a))

Proof state:
case zero
a k : ℕ
hk : k ∈ ↑(range a)
l : ℕ
hl : l ∈ ↑(range a)
hkl : k % a = l % a
⊢ k = l

Tactic:
simp only [Finset.mem_range, Finset.mem_coe] at hk hl

Result:
case zero
a k l : ℕ
hkl : k % a = l % a
hk : k < a
hl : l < a
⊢ k = l

Proof state:
a n : ℕ
ih : Set.InjOn (fun x => x % a) ↑(Ico n (n + a))
k : ℕ
hk : k ∈ ↑((insert (n + a) (Ico n (n + a))).erase n)
l : ℕ
hl : l ∈ ↑((insert (n + a) (Ico n (n + a))).erase n)
hkl : k % a = l % a
⊢ a ≠ 0

Tactic:
rintro rfl

Result:
n k l : ℕ
ih : Set.InjOn (fun x => x % 0) ↑(Ico n (n + 0))
hk : k ∈ ↑((insert (n + 0) (Ico n (n + 0))).erase n)
hl : l ∈ ↑((insert (n + 0) (Ico n (n + 0))).erase n)
hkl : k % 0 = l % 0
⊢ False
-- Mathlib/Logic/Equiv/Basic.lean
theorem piCongrLeft'_symm (P : Sort*) (e : α ≃ β) :
    (piCongrLeft' (fun _ => P) e).symm = piCongrLeft' _ e.symm

Proof state:
α : Sort u_1
β : Sort u_4
P : Sort u_9
e : α ≃ β
⊢ (piCongrLeft' (fun x => P) e).symm = piCongrLeft' (fun a => P) e.symm

Tactic:
ext

Result:
case H.h
α : Sort u_1
β : Sort u_4
P : Sort u_9
e : α ≃ β
x✝¹ : β → P
x✝ : α
⊢ (piCongrLeft' (fun x => P) e).symm x✝¹ x✝ = (piCongrLeft' (fun a => P) e.symm) x✝¹ x✝

Proof state:
case H.h
α : Sort u_1
β : Sort u_4
P : Sort u_9
e : α ≃ β
x✝¹ : β → P
x✝ : α
⊢ (piCongrLeft' (fun x => P) e).symm x✝¹ x✝ = (piCongrLeft' (fun a => P) e.symm) x✝¹ x✝

Tactic:
simp [piCongrLeft']

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Polynomial.lean
lemma isCompact_image_comap_of_monic (f g : R[X]) (hg : g.Monic) :
    IsCompact (comap C '' (zeroLocus {g} \ zeroLocus {f}))

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
t : Finset R
ht : ⇑(comap C) '' (zeroLocus {g} \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ
⊢ IsCompact (⇑(comap C) '' (zeroLocus {g} \ zeroLocus {f}))

Tactic:
rw [ht, ← t.toSet.iUnion_of_singleton_coe, zeroLocus_iUnion, Set.compl_iInter]

Result:
case intro
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
t : Finset R
ht : ⇑(comap C) '' (zeroLocus {g} \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ
⊢ IsCompact (⋃ i, (zeroLocus {↑i})ᶜ)

Proof state:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
t : Finset R
ht : ⇑(comap C) '' (zeroLocus {g} \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ
x✝ : ↑↑t
⊢ IsCompact (zeroLocus {↑x✝})ᶜ

Tactic:
simpa using isCompact_basicOpen _

Result:
no goals

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
t : Finset R
ht : ⇑(comap C) '' (zeroLocus {g} \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ
⊢ IsCompact (⋃ i, (zeroLocus {↑i})ᶜ)

Tactic:
apply isCompact_iUnion

Result:
case intro.h
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
t : Finset R
ht : ⇑(comap C) '' (zeroLocus {g} \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ
⊢ ∀ (i : ↑↑t), IsCompact (zeroLocus {↑i})ᶜ

Proof state:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
⊢ IsCompact (⇑(comap C) '' (zeroLocus {g} \ zeroLocus {f}))

Tactic:
obtain ⟨t, ht⟩ := exists_image_comap_of_monic f g hg

Result:
case intro
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
t : Finset R
ht : ⇑(comap C) '' (zeroLocus {g} \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ
⊢ IsCompact (⇑(comap C) '' (zeroLocus {g} \ zeroLocus {f}))

Proof state:
case intro.h
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
t : Finset R
ht : ⇑(comap C) '' (zeroLocus {g} \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ
⊢ ∀ (i : ↑↑t), IsCompact (zeroLocus {↑i})ᶜ

Tactic:
exact fun _ ↦ by simpa using isCompact_basicOpen _

Result:
no goals
-- Mathlib/Order/Atoms.lean
theorem covBy_iff' {K L : A} :
    K ⋖ L ↔ K < L ∧ ∀ H g, K ≤ H → H ≤ L → g ∉ H → g ∈ L → H = K

Proof state:
A : Type u_4
B : Type u_5
inst✝ : SetLike A B
K L : A
x✝ : K < L
H : A
⊢ ¬(K < H → ¬H < L) ↔ ¬∀ (g : B), K ≤ H → H ≤ L → g ∉ H → g ∈ L → H = K

Tactic:
push_neg

Result:
A : Type u_4
B : Type u_5
inst✝ : SetLike A B
K L : A
x✝ : K < L
H : A
⊢ K < H ∧ H < L ↔ ∃ g, K ≤ H ∧ H ≤ L ∧ g ∉ H ∧ g ∈ L ∧ H ≠ K

Proof state:
A : Type u_4
B : Type u_5
inst✝ : SetLike A B
K L : A
⊢ K ⋖ L ↔ K < L ∧ ∀ (H : A) (g : B), K ≤ H → H ≤ L → g ∉ H → g ∈ L → H = K

Tactic:
refine and_congr_right fun _ ↦ forall_congr' fun H ↦ not_iff_not.mp ?_

Result:
A : Type u_4
B : Type u_5
inst✝ : SetLike A B
K L : A
x✝ : K < L
H : A
⊢ ¬(K < H → ¬H < L) ↔ ¬∀ (g : B), K ≤ H → H ≤ L → g ∉ H → g ∈ L → H = K

Proof state:
A : Type u_4
B : Type u_5
inst✝ : SetLike A B
K L : A
x✝ : K < L
H : A
⊢ (K ≤ H ∧ H ≤ L) ∧ K ≠ H ∧ ¬L ≤ H ↔ ∃ g, K ≤ H ∧ H ≤ L ∧ g ∉ H ∧ g ∈ L ∧ H ≠ K

Tactic:
simp_rw [exists_and_left, and_assoc, and_congr_right_iff, ← and_assoc, and_comm, exists_and_left,
  SetLike.not_le_iff_exists, ne_comm, implies_true]

Result:
no goals

Proof state:
A : Type u_4
B : Type u_5
inst✝ : SetLike A B
K L : A
x✝ : K < L
H : A
⊢ K < H ∧ H < L ↔ ∃ g, K ≤ H ∧ H ≤ L ∧ g ∉ H ∧ g ∈ L ∧ H ≠ K

Tactic:
rw [lt_iff_le_and_ne, lt_iff_le_not_le, and_and_and_comm]

Result:
A : Type u_4
B : Type u_5
inst✝ : SetLike A B
K L : A
x✝ : K < L
H : A
⊢ (K ≤ H ∧ H ≤ L) ∧ K ≠ H ∧ ¬L ≤ H ↔ ∃ g, K ≤ H ∧ H ≤ L ∧ g ∉ H ∧ g ∈ L ∧ H ≠ K
-- Mathlib/RingTheory/TensorProduct/Basic.lean
theorem productMap_eq_comp_map : productMap f g = (lmul' R).comp (TensorProduct.map f g)

Proof state:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : CommSemiring S
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R S
f : A →ₐ[R] S
g : B →ₐ[R] S
⊢ productMap f g = (lmul' R).comp (map f g)

Tactic:
ext <;> rfl

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem Ideal.pow_lt_self (I : Ideal A) (hI0 : I ≠ ⊥) (hI1 : I ≠ ⊤) (e : ℕ) (he : 2 ≤ e) :
    I ^ e < I

Proof state:
case h.e'_4
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI1 : I ≠ ⊤
e : ℕ
he : 2 ≤ e
⊢ I = I ^ 1

Tactic:
rw [pow_one]

Result:
no goals

Proof state:
case h.e'_4
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI1 : I ≠ ⊤
e : ℕ
he : 2 ≤ e
⊢ I = (fun x => I ^ x) 1

Tactic:
dsimp only

Result:
case h.e'_4
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI1 : I ≠ ⊤
e : ℕ
he : 2 ≤ e
⊢ I = I ^ 1

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI1 : I ≠ ⊤
e : ℕ
he : 2 ≤ e
⊢ I ^ e < I

Tactic:
convert I.pow_right_strictAnti hI0 hI1 he

Result:
case h.e'_4
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI1 : I ≠ ⊤
e : ℕ
he : 2 ≤ e
⊢ I = (fun x => I ^ x) 1
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem getElem?_set_eq_of_lt (a : α) {n} {l : List α} (h : n < length l) :
    (set l n a)[n]? = some a

Proof state:
α : Type u_1
a : α
n : Nat
l : List α
h : n < l.length
⊢ (l.set n a)[n]? = some a

Tactic:
rw [getElem?_set_self', getElem?_eq_getElem h]

Result:
α : Type u_1
a : α
n : Nat
l : List α
h : n < l.length
⊢ Function.const α a <$> some l[n] = some a

Proof state:
α : Type u_1
a : α
n : Nat
l : List α
h : n < l.length
⊢ Function.const α a <$> some l[n] = some a

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Nat/BinaryRec.lean
theorem bit_decide_mod_two_eq_one_shiftRight_one (n : Nat) : bit (n % 2 = 1) (n >>> 1) = n

Proof state:
n : Nat
⊢ (bif decide (n % 2 = 1) then fun x => 2 * x + 1 else fun x => 2 * x) (n / 2) = n

Tactic:
cases mod_two_eq_zero_or_one n with | _ h => simpa [h] using Nat.div_add_mod n 2

Result:
no goals

Proof state:
n : Nat
⊢ bit (decide (n % 2 = 1)) (n >>> 1) = n

Tactic:
simp only [bit, shiftRight_one]

Result:
n : Nat
⊢ (bif decide (n % 2 = 1) then fun x => 2 * x + 1 else fun x => 2 * x) (n / 2) = n

Proof state:
case inr
n : Nat
h : n % 2 = 1
⊢ (bif decide (n % 2 = 1) then fun x => 2 * x + 1 else fun x => 2 * x) (n / 2) = n

Tactic:
simpa [h] using Nat.div_add_mod n 2

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem ker_dualMap_eq_dualAnnihilator_range :
    LinearMap.ker f.dualMap = f.range.dualAnnihilator

Proof state:
case h
R : Type uR
inst✝⁴ : CommSemiring R
M₁ : Type uM₁
M₂ : Type uM₂
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
x✝ : Dual R M₂
⊢ x✝ ∈ ker f.dualMap ↔ x✝ ∈ (range f).dualAnnihilator

Tactic:
simp_rw [mem_ker, LinearMap.ext_iff, Submodule.mem_dualAnnihilator,
  ← SetLike.mem_coe, range_coe, Set.forall_mem_range]

Result:
case h
R : Type uR
inst✝⁴ : CommSemiring R
M₁ : Type uM₁
M₂ : Type uM₂
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
x✝ : Dual R M₂
⊢ (∀ (x : M₁), (f.dualMap x✝) x = 0 x) ↔ ∀ (i : M₁), x✝ (f i) = 0

Proof state:
R : Type uR
inst✝⁴ : CommSemiring R
M₁ : Type uM₁
M₂ : Type uM₂
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
⊢ ker f.dualMap = (range f).dualAnnihilator

Tactic:
ext

Result:
case h
R : Type uR
inst✝⁴ : CommSemiring R
M₁ : Type uM₁
M₂ : Type uM₂
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
x✝ : Dual R M₂
⊢ x✝ ∈ ker f.dualMap ↔ x✝ ∈ (range f).dualAnnihilator

Proof state:
case h
R : Type uR
inst✝⁴ : CommSemiring R
M₁ : Type uM₁
M₂ : Type uM₂
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
x✝ : Dual R M₂
⊢ (∀ (x : M₁), (f.dualMap x✝) x = 0 x) ↔ ∀ (i : M₁), x✝ (f i) = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma one_le_of_le_mul_left₀ [PosMulReflectLE α] (ha : 0 < a) (h : a ≤ a * b) : 1 ≤ b :=
  le_of_mul_le_mul_left (by simpa) ha

Proof state:
α : Type u_3
a b : α
inst✝³ : MulOneClass α
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
ha : 0 < a
h : a ≤ a * b
⊢ a * 1 ≤ a * b

Tactic:
simpa

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean
lemma Icc_add_one_left_eq_Ioc_of_not_isMax (ha : ¬ IsMax a) (b : α) : Icc (a + 1) b = Ioc a b

Proof state:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Add α
inst✝ : SuccAddOrder α
a : α
ha : ¬IsMax a
b : α
⊢ Icc (a + 1) b = Ioc a b

Tactic:
simpa [succ_eq_add_one] using Icc_succ_left_eq_Ioc_of_not_isMax ha b

Result:
no goals