harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem eq_pow_count_factors_of_dvd_pow {p a : Associates α}
    (hp : Irreducible p) {n : ℕ} (h : a ∣ p ^ n) : a = p ^ p.count a.factors

Proof state:
case h.e'_4
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
a✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
q : Associates α
hq : Irreducible q
h' : q ≠ p
⊢ 0 = q.count (p ^ n).factors

Tactic:
symm

Result:
case h.e'_4
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
a✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
q : Associates α
hq : Irreducible q
h' : q ≠ p
⊢ q.count (p ^ n).factors = 0

Proof state:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
a✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
eq_zero_of_ne : ∀ (q : Associates α), Irreducible q → q ≠ p → q.count a.factors = 0
q : Associates α
hq : Irreducible q
⊢ q.count a.factors = q.count (p ^ p.count a.factors).factors

Tactic:
rw [count_pow hp.ne_zero hq]

Result:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
a✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
eq_zero_of_ne : ∀ (q : Associates α), Irreducible q → q ≠ p → q.count a.factors = 0
q : Associates α
hq : Irreducible q
⊢ q.count a.factors = p.count a.factors * q.count p.factors

Proof state:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
a✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
⊢ ∀ (p_1 : Associates α), Irreducible p_1 → p_1.count a.factors = p_1.count (p ^ p.count a.factors).factors

Tactic:
have eq_zero_of_ne : ∀ q : Associates α, Irreducible q → q ≠ p → _ = 0 := fun q hq h' =>
  Nat.eq_zero_of_le_zero <| by
    convert count_le_count_of_le hph hq h
    symm
    rw [count_pow hp.ne_zero hq, count_eq_zero_of_ne hq hp h', mul_zero]

Result:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
a✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
eq_zero_of_ne : ∀ (q : Associates α), Irreducible q → q ≠ p → q.count a.factors = 0
⊢ ∀ (p_1 : Associates α), Irreducible p_1 → p_1.count a.factors = p_1.count (p ^ p.count a.factors).factors
-- Mathlib/Algebra/DirectSum/LinearMap.lean
lemma mapsTo_biSup_of_mapsTo {ι : Type*} {N : ι → Submodule R M}
    (s : Set ι) {f : Module.End R M} (hf : ∀ i, MapsTo f (N i) (N i)) :
    MapsTo f ↑(⨆ i ∈ s, N i) ↑(⨆ i ∈ s, N i)

Proof state:
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_4
N : ι → Submodule R M
s : Set ι
f : Module.End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
⊢ MapsTo ⇑f ↑(⨆ i ∈ s, N i) ↑(⨆ i ∈ s, N i)

Tactic:
replace hf : ∀ i, (N i).map f ≤ N i := fun i ↦ Submodule.map_le_iff_le_comap.mpr (hf i)

Result:
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_4
N : ι → Submodule R M
s : Set ι
f : Module.End R M
hf : ∀ (i : ι), Submodule.map f (N i) ≤ N i
⊢ MapsTo ⇑f ↑(⨆ i ∈ s, N i) ↑(⨆ i ∈ s, N i)

Proof state:
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_4
N : ι → Submodule R M
s : Set ι
f : Module.End R M
hf : ∀ (i : ι), Submodule.map f (N i) ≤ N i
⊢ MapsTo ⇑f ↑(⨆ i ∈ s, N i) ↑(⨆ i ∈ s, N i)

Tactic:
suffices (⨆ i ∈ s, N i).map f ≤ ⨆ i ∈ s, N i from Submodule.map_le_iff_le_comap.mp this

Result:
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_4
N : ι → Submodule R M
s : Set ι
f : Module.End R M
hf : ∀ (i : ι), Submodule.map f (N i) ≤ N i
⊢ Submodule.map f (⨆ i ∈ s, N i) ≤ ⨆ i ∈ s, N i

Proof state:
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_4
N : ι → Submodule R M
s : Set ι
f : Module.End R M
hf : ∀ (i : ι), Submodule.map f (N i) ≤ N i
⊢ Submodule.map f (⨆ i ∈ s, N i) ≤ ⨆ i ∈ s, N i

Tactic:
simpa only [Submodule.map_iSup] using iSup₂_mono <| fun i _ ↦ hf i

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Adjunction.lean
@[simp]
lemma localization_counit_app (X₂ : C₂) :
    (adj.localization L₁ W₁ L₂ W₂ G' F').counit.app (L₂.obj X₂) =
    G'.map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂) ≫
      (CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂) ≫
      L₂.map (adj.counit.app X₂)

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_8, u_1} C₁
inst✝⁶ : Category.{u_7, u_2} C₂
inst✝⁵ : Category.{u_6, u_3} D₁
inst✝⁴ : Category.{u_5, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
⊢ (adj.localization L₁ W₁ L₂ W₂ G' F').counit.app (L₂.obj X₂) =
    G'.map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂) ≫
      (CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)

Tactic:
apply Localization.η_app

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Colim.lean
/-- Assuming `HasExactColimitsOfShape J C`, this lemma rephrases the exactness
of the functor `colim : (J ⥤ C) ⥤ C` by saying that if `S : ShortComplex (J ⥤ C)`
is exact, then the short complex obtained by taking the colimits is exact,
where we allow the replacement of the chosen colimit cocones of the
colimit API by arbitrary colimit cocones. -/
lemma colim.exact_mapShortComplex :
    (mapShortComplex S hc₁ c₂ c₃ f g hf hg).Exact

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : HasExactColimitsOfShape J C
inst✝ : HasZeroMorphisms C
S : ShortComplex (J ⥤ C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
⊢ (mapShortComplex S hc₁ c₂ c₃ f g hf hg).Exact

Tactic:
refine (ShortComplex.exact_iff_of_iso ?_).2 (hS.map colim)

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : HasExactColimitsOfShape J C
inst✝ : HasZeroMorphisms C
S : ShortComplex (J ⥤ C)
hS : S.Exact
c₁ : Cocone S.X₁
hc₁ : IsColimit c₁
c₂ : Cocone S.X₂
hc₂ : IsColimit c₂
c₃ : Cocone S.X₃
hc₃ : IsColimit c₃
f : c₁.pt ⟶ c₂.pt
g : c₂.pt ⟶ c₃.pt
hf : ∀ (j : J), c₁.ι.app j ≫ f = S.f.app j ≫ c₂.ι.app j
hg : ∀ (j : J), c₂.ι.app j ≫ g = S.g.app j ≫ c₃.ι.app j
⊢ mapShortComplex S hc₁ c₂ c₃ f g hf hg ≅ S.map colim
-- Mathlib/FieldTheory/PurelyInseparable/PerfectClosure.lean
theorem LinearIndependent.map_pow_expChar_pow_of_isSeparable [Algebra.IsSeparable F E]
    (h : LinearIndependent F v) : LinearIndependent F (v · ^ q ^ n)

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝ : Algebra.IsSeparable F E
h : ∀ (s : Finset ι), LinearIndependent F (v ∘ Subtype.val)
halg : Algebra.IsAlgebraic F E
s : Finset ι
⊢ LinearIndependent F ((fun x => v x ^ q ^ n) ∘ Subtype.val)

Tactic:
let E' := adjoin F (s.image v : Set E)

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝ : Algebra.IsSeparable F E
h : ∀ (s : Finset ι), LinearIndependent F (v ∘ Subtype.val)
halg : Algebra.IsAlgebraic F E
s : Finset ι
E' : IntermediateField F E := adjoin F ↑(Finset.image v s)
⊢ LinearIndependent F ((fun x => v x ^ q ^ n) ∘ Subtype.val)
-- Mathlib/NumberTheory/ZetaValues.lean
theorem integral_bernoulliFun_eq_zero {k : ℕ} (hk : k ≠ 0) :
    ∫ x : ℝ in (0)..1, bernoulliFun k x = 0

Proof state:
k : ℕ
hk : k ≠ 0
⊢ bernoulliFun (k + 1) 1 / (↑k + 1) - bernoulliFun (k + 1) 0 / (↑k + 1) = 0

Tactic:
rw [bernoulliFun_eval_one]

Result:
k : ℕ
hk : k ≠ 0
⊢ (bernoulliFun (k + 1) 0 + if k + 1 = 1 then 1 else 0) / (↑k + 1) - bernoulliFun (k + 1) 0 / (↑k + 1) = 0

Proof state:
case pos
k : ℕ
hk : k ≠ 0
h : k + 1 = 1
⊢ (bernoulliFun (k + 1) 0 + 1) / (↑k + 1) - bernoulliFun (k + 1) 0 / (↑k + 1) = 0

Tactic:
exfalso

Result:
case pos
k : ℕ
hk : k ≠ 0
h : k + 1 = 1
⊢ False

Proof state:
k : ℕ
hk : k ≠ 0
⊢ (bernoulliFun (k + 1) 0 + if k + 1 = 1 then 1 else 0) / (↑k + 1) - bernoulliFun (k + 1) 0 / (↑k + 1) = 0

Tactic:
split_ifs with h

Result:
case pos
k : ℕ
hk : k ≠ 0
h : k + 1 = 1
⊢ (bernoulliFun (k + 1) 0 + 1) / (↑k + 1) - bernoulliFun (k + 1) 0 / (↑k + 1) = 0

case neg
k : ℕ
hk : k ≠ 0
h : ¬k + 1 = 1
⊢ (bernoulliFun (k + 1) 0 + 0) / (↑k + 1) - bernoulliFun (k + 1) 0 / (↑k + 1) = 0

Proof state:
case neg
k : ℕ
hk : k ≠ 0
h : ¬k + 1 = 1
⊢ (bernoulliFun (k + 1) 0 + 0) / (↑k + 1) - bernoulliFun (k + 1) 0 / (↑k + 1) = 0

Tactic:
simp

Result:
no goals

Proof state:
case pos
k : ℕ
hk : k ≠ 0
h : k + 1 = 1
⊢ False

Tactic:
exact hk (Nat.succ_inj'.mp h)

Result:
no goals

Proof state:
k : ℕ
hk : k ≠ 0
⊢ ∫ (x : ℝ) in 0 ..1, bernoulliFun k x = 0

Tactic:
rw [integral_eq_sub_of_hasDerivAt (fun x _ => antideriv_bernoulliFun k x)
    ((Polynomial.continuous _).intervalIntegrable _ _)]

Result:
k : ℕ
hk : k ≠ 0
⊢ bernoulliFun (k + 1) 1 / (↑k + 1) - bernoulliFun (k + 1) 0 / (↑k + 1) = 0
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem mkNormedAddGroupHom_norm_le' (f : V₁ →+ V₂) {C : ℝ} (h : ∀ x, ‖f x‖ ≤ C * ‖x‖) :
    ‖f.mkNormedAddGroupHom C h‖ ≤ max C 0 :=
  opNorm_le_bound _ (le_max_right _ _) fun x =>
    (h x).trans <| by gcongr; apply le_max_left

Proof state:
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : V₁ →+ V₂
C : ℝ
h : ∀ (x : V₁), ‖f x‖ ≤ C * ‖x‖
x : V₁
⊢ C * ‖x‖ ≤ (C ⊔ 0) * ‖x‖

Tactic:
gcongr

Result:
case h
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : V₁ →+ V₂
C : ℝ
h : ∀ (x : V₁), ‖f x‖ ≤ C * ‖x‖
x : V₁
⊢ C ≤ C ⊔ 0

Proof state:
case h
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : V₁ →+ V₂
C : ℝ
h : ∀ (x : V₁), ‖f x‖ ≤ C * ‖x‖
x : V₁
⊢ C ≤ C ⊔ 0

Tactic:
apply le_max_left

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem le_of_lt_add_one {x y : PartENat} (h : x < y + 1) : x ≤ y

Proof state:
case a
x : PartENat
n : ℕ
h : x < ↑n + 1
⊢ x ≤ ↑n

Tactic:
rcases ne_top_iff.mp (ne_top_of_lt h) with ⟨m, rfl⟩

Result:
case a.intro
n m : ℕ
h : ↑m < ↑n + 1
⊢ ↑m ≤ ↑n

Proof state:
x y : PartENat
h : x < y + 1
⊢ x ≤ y

Tactic:
induction' y using PartENat.casesOn with n

Result:
case a
x : PartENat
h : x < ⊤ + 1
⊢ x ≤ ⊤

case a
x : PartENat
n : ℕ
h : x < ↑n + 1
⊢ x ≤ ↑n

Proof state:
case a.intro.a
n m : ℕ
h : ↑m < ↑n + 1
⊢ m < n.succ

Tactic:
norm_cast at h

Result:
no goals

Proof state:
case a
x : PartENat
h : x < ⊤ + 1
⊢ x ≤ ⊤

Tactic:
apply le_top

Result:
no goals

Proof state:
case a.intro
n m : ℕ
h : ↑m < ↑n + 1
⊢ ↑m ≤ ↑n

Tactic:
norm_cast

Result:
case a.intro
n m : ℕ
h : ↑m < ↑n + 1
⊢ m ≤ n

Proof state:
case a.intro
n m : ℕ
h : ↑m < ↑n + 1
⊢ m ≤ n

Tactic:
apply Nat.le_of_lt_succ

Result:
case a.intro.a
n m : ℕ
h : ↑m < ↑n + 1
⊢ m < n.succ
-- Mathlib/Algebra/Field/Subfield/Basic.lean
theorem mem_iSup_of_directed {ι} [hι : Nonempty ι] {S : ι → Subfield K} (hS : Directed (· ≤ ·) S)
    {x : K} : (x ∈ ⨆ i, S i) ↔ ∃ i, x ∈ S i

Proof state:
K : Type u
inst✝ : DivisionRing K
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : K
s : Subfield K :=
  let __spread.0 := (⨆ i, (S i).toSubring).copy (⋃ i, ↑(S i).toSubring) ⋯;
  { toSubring := __spread.0, inv_mem' := ⋯ }
⊢ x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i

Tactic:
have : iSup S = s := le_antisymm
  (iSup_le fun i ↦ le_iSup (fun i ↦ (S i : Set K)) i) (Set.iUnion_subset fun _ ↦ le_iSup S _)

Result:
K : Type u
inst✝ : DivisionRing K
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : K
s : Subfield K :=
  let __spread.0 := (⨆ i, (S i).toSubring).copy (⋃ i, ↑(S i).toSubring) ⋯;
  { toSubring := __spread.0, inv_mem' := ⋯ }
this : iSup S = s
⊢ x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i

Proof state:
K : Type u
inst✝ : DivisionRing K
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : K
⊢ x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i

Tactic:
let s : Subfield K :=
  { __ := Subring.copy _ _ (Subring.coe_iSup_of_directed hS).symm
    inv_mem' := fun _ hx ↦ have ⟨i, hi⟩ := Set.mem_iUnion.mp hx
      Set.mem_iUnion.mpr ⟨i, (S i).inv_mem hi⟩ }

Result:
K : Type u
inst✝ : DivisionRing K
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : K
s : Subfield K :=
  let __spread.0 := (⨆ i, (S i).toSubring).copy (⋃ i, ↑(S i).toSubring) ⋯;
  { toSubring := __spread.0, inv_mem' := ⋯ }
⊢ x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i

Proof state:
K : Type u
inst✝ : DivisionRing K
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : K
s : Subfield K :=
  let __spread.0 := (⨆ i, (S i).toSubring).copy (⋃ i, ↑(S i).toSubring) ⋯;
  { toSubring := __spread.0, inv_mem' := ⋯ }
this : iSup S = s
⊢ x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i

Tactic:
exact this ▸ Set.mem_iUnion

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Ideal.lean
theorem matricesOver_strictMono_of_nonempty [Nonempty n] :
    StrictMono (matricesOver (R := R) n) :=
  matricesOver_monotone n |>.strictMono_of_injective <| fun I J eq => by
    ext x
    have : (∀ _ _, x ∈ I) ↔ (∀ _ _, x ∈ J) := congr((Matrix.of fun _ _ => x) ∈ $eq)
    simpa only [forall_const] using this

Proof state:
case h
R : Type u_1
inst✝³ : Semiring R
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
I J : Ideal R
eq : matricesOver n I = matricesOver n J
x : R
this : n → n → x ∈ I ↔ n → n → x ∈ J
⊢ x ∈ I ↔ x ∈ J

Tactic:
simpa only [forall_const] using this

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝³ : Semiring R
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
I J : Ideal R
eq : matricesOver n I = matricesOver n J
x : R
⊢ x ∈ I ↔ x ∈ J

Tactic:
have : (∀ _ _, x ∈ I) ↔ (∀ _ _, x ∈ J) := congr((Matrix.of fun _ _ => x) ∈ $eq)

Result:
case h
R : Type u_1
inst✝³ : Semiring R
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
I J : Ideal R
eq : matricesOver n I = matricesOver n J
x : R
this : n → n → x ∈ I ↔ n → n → x ∈ J
⊢ x ∈ I ↔ x ∈ J

Proof state:
R : Type u_1
inst✝³ : Semiring R
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
I J : Ideal R
eq : matricesOver n I = matricesOver n J
⊢ I = J

Tactic:
ext x

Result:
case h
R : Type u_1
inst✝³ : Semiring R
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
I J : Ideal R
eq : matricesOver n I = matricesOver n J
x : R
⊢ x ∈ I ↔ x ∈ J
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem map_attachWith {l : List α} {P : α → Prop} {H : ∀ (a : α), a ∈ l → P a}
    (f : { x // P x } → β) :
    (l.attachWith P H).map f =
      l.pmap (fun a (h : a ∈ l ∧ P a) => f ⟨a, H _ h.1⟩) (fun a h => ⟨h, H a h⟩)

Proof state:
case nil
α : Type u_1
β : Type u_2
P : α → Prop
f : { x // P x } → β
H : ∀ (a : α), a ∈ [] → P a
⊢ map f ([].attachWith P H) = pmap (fun a h => f ⟨a, ⋯⟩) [] ⋯

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
P : α → Prop
f : { x // P x } → β
x : α
xs : List α
ih : ∀ {H : ∀ (a : α), a ∈ xs → P a}, map f (xs.attachWith P H) = pmap (fun a h => f ⟨a, ⋯⟩) xs ⋯
H : ∀ (a : α), a ∈ x :: xs → P a
⊢ pmap (fun a h => f ⟨a, ⋯⟩) xs ⋯ = pmap (fun a h => f ⟨a, ⋯⟩) xs ⋯

Tactic:
apply pmap_congr_left

Result:
case cons.h
α : Type u_1
β : Type u_2
P : α → Prop
f : { x // P x } → β
x : α
xs : List α
ih : ∀ {H : ∀ (a : α), a ∈ xs → P a}, map f (xs.attachWith P H) = pmap (fun a h => f ⟨a, ⋯⟩) xs ⋯
H : ∀ (a : α), a ∈ x :: xs → P a
⊢ ∀ (a : α), a ∈ xs → ∀ (h₁ : a ∈ xs ∧ P a) (h₂ : a ∈ x :: xs ∧ P a), f ⟨a, ⋯⟩ = f ⟨a, ⋯⟩

Proof state:
α : Type u_1
β : Type u_2
l : List α
P : α → Prop
H : ∀ (a : α), a ∈ l → P a
f : { x // P x } → β
⊢ map f (l.attachWith P H) = pmap (fun a h => f ⟨a, ⋯⟩) l ⋯

Tactic:
induction l with
| nil => rfl
| cons x xs ih =>
  simp only [attachWith_cons, map_cons, ih, pmap, cons.injEq, true_and]
  apply pmap_congr_left
  simp

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
P : α → Prop
f : { x // P x } → β
x : α
xs : List α
ih : ∀ {H : ∀ (a : α), a ∈ xs → P a}, map f (xs.attachWith P H) = pmap (fun a h => f ⟨a, ⋯⟩) xs ⋯
H : ∀ (a : α), a ∈ x :: xs → P a
⊢ map f ((x :: xs).attachWith P H) = pmap (fun a h => f ⟨a, ⋯⟩) (x :: xs) ⋯

Tactic:
simp only [attachWith_cons, map_cons, ih, pmap, cons.injEq, true_and]

Result:
case cons
α : Type u_1
β : Type u_2
P : α → Prop
f : { x // P x } → β
x : α
xs : List α
ih : ∀ {H : ∀ (a : α), a ∈ xs → P a}, map f (xs.attachWith P H) = pmap (fun a h => f ⟨a, ⋯⟩) xs ⋯
H : ∀ (a : α), a ∈ x :: xs → P a
⊢ pmap (fun a h => f ⟨a, ⋯⟩) xs ⋯ = pmap (fun a h => f ⟨a, ⋯⟩) xs ⋯

Proof state:
case cons.h
α : Type u_1
β : Type u_2
P : α → Prop
f : { x // P x } → β
x : α
xs : List α
ih : ∀ {H : ∀ (a : α), a ∈ xs → P a}, map f (xs.attachWith P H) = pmap (fun a h => f ⟨a, ⋯⟩) xs ⋯
H : ∀ (a : α), a ∈ x :: xs → P a
⊢ ∀ (a : α), a ∈ xs → ∀ (h₁ : a ∈ xs ∧ P a) (h₂ : a ∈ x :: xs ∧ P a), f ⟨a, ⋯⟩ = f ⟨a, ⋯⟩

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
lemma sup_pow_add_le_pow_sup_pow {n m : ℕ} : (I ⊔ J) ^ (n + m) ≤ I ^ n ⊔ J ^ m

Proof state:
case a
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n m i : ℕ
hi : i ∈ Finset.range (n + m + 1)
⊢ I ^ i * J ^ (n + m - i) * ↑((n + m).choose i) ≤ I ^ n + J ^ m

Tactic:
by_cases hn : n ≤ i

Result:
case pos
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n m i : ℕ
hi : i ∈ Finset.range (n + m + 1)
hn : n ≤ i
⊢ I ^ i * J ^ (n + m - i) * ↑((n + m).choose i) ≤ I ^ n + J ^ m

case neg
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n m i : ℕ
hi : i ∈ Finset.range (n + m + 1)
hn : ¬n ≤ i
⊢ I ^ i * J ^ (n + m - i) * ↑((n + m).choose i) ≤ I ^ n + J ^ m

Proof state:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n m : ℕ
⊢ ((Finset.range (n + m + 1)).sup fun m_1 => I ^ m_1 * J ^ (n + m - m_1) * ↑((n + m).choose m_1)) ≤ I ^ n + J ^ m

Tactic:
apply Finset.sup_le

Result:
case a
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n m : ℕ
⊢ ∀ b ∈ Finset.range (n + m + 1), I ^ b * J ^ (n + m - b) * ↑((n + m).choose b) ≤ I ^ n + J ^ m

Proof state:
case a
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n m : ℕ
⊢ ∀ b ∈ Finset.range (n + m + 1), I ^ b * J ^ (n + m - b) * ↑((n + m).choose b) ≤ I ^ n + J ^ m

Tactic:
intros i hi

Result:
case a
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n m i : ℕ
hi : i ∈ Finset.range (n + m + 1)
⊢ I ^ i * J ^ (n + m - i) * ↑((n + m).choose i) ≤ I ^ n + J ^ m

Proof state:
case neg
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n m i : ℕ
hi : i ∈ Finset.range (n + m + 1)
hn : ¬n ≤ i
⊢ I ^ i * J ^ (n + m - i) * ↑((n + m).choose i) ≤ I ^ n + J ^ m

Tactic:
refine (Ideal.mul_le_right.trans (Ideal.mul_le_left.trans
  ((Ideal.pow_le_pow_right ?_).trans le_sup_right)))

Result:
case neg
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n m i : ℕ
hi : i ∈ Finset.range (n + m + 1)
hn : ¬n ≤ i
⊢ m ≤ n + m - i

Proof state:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n m : ℕ
⊢ (I ⊔ J) ^ (n + m) ≤ I ^ n ⊔ J ^ m

Tactic:
rw [← Ideal.add_eq_sup, ← Ideal.add_eq_sup, add_pow, Ideal.sum_eq_sup]

Result:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n m : ℕ
⊢ ((Finset.range (n + m + 1)).sup fun m_1 => I ^ m_1 * J ^ (n + m - m_1) * ↑((n + m).choose m_1)) ≤ I ^ n + J ^ m

Proof state:
case pos
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n m i : ℕ
hi : i ∈ Finset.range (n + m + 1)
hn : n ≤ i
⊢ I ^ i * J ^ (n + m - i) * ↑((n + m).choose i) ≤ I ^ n + J ^ m

Tactic:
exact (Ideal.mul_le_right.trans (Ideal.mul_le_right.trans
  ((Ideal.pow_le_pow_right hn).trans le_sup_left)))

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
n m i : ℕ
hi : i ∈ Finset.range (n + m + 1)
hn : ¬n ≤ i
⊢ m ≤ n + m - i

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Ring/Ext.lean
theorem ext ⦃inst₁ inst₂ : NonUnitalRing R⦄
    (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂])
    (h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) :
    inst₁ = inst₂

Proof state:
R : Type u
inst₁ inst₂ : NonUnitalRing R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ inst₁ = inst₂

Tactic:
have : inst₁.toNonUnitalNonAssocRing = inst₂.toNonUnitalNonAssocRing := by
  ext : 1 <;> assumption

Result:
R : Type u
inst₁ inst₂ : NonUnitalRing R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
this : toNonUnitalNonAssocRing = toNonUnitalNonAssocRing
⊢ inst₁ = inst₂

Proof state:
R : Type u
inst₁ inst₂ : NonUnitalRing R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ toNonUnitalNonAssocRing = toNonUnitalNonAssocRing

Tactic:
ext : 1 <;> assumption

Result:
no goals

Proof state:
case mk
R : Type u
inst₂ : NonUnitalRing R
toNonUnitalNonAssocRing✝ : NonUnitalNonAssocRing R
mul_assoc✝ : ∀ (a b c : R), a * b * c = a * (b * c)
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
this : toNonUnitalNonAssocRing = toNonUnitalNonAssocRing
⊢ mk mul_assoc✝ = inst₂

Tactic:
cases inst₂

Result:
case mk.mk
R : Type u
toNonUnitalNonAssocRing✝¹ : NonUnitalNonAssocRing R
mul_assoc✝¹ : ∀ (a b c : R), a * b * c = a * (b * c)
toNonUnitalNonAssocRing✝ : NonUnitalNonAssocRing R
mul_assoc✝ : ∀ (a b c : R), a * b * c = a * (b * c)
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
this : toNonUnitalNonAssocRing = toNonUnitalNonAssocRing
⊢ mk mul_assoc✝¹ = mk mul_assoc✝

Proof state:
R : Type u
inst₁ inst₂ : NonUnitalRing R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
this : toNonUnitalNonAssocRing = toNonUnitalNonAssocRing
⊢ inst₁ = inst₂

Tactic:
cases inst₁

Result:
case mk
R : Type u
inst₂ : NonUnitalRing R
toNonUnitalNonAssocRing✝ : NonUnitalNonAssocRing R
mul_assoc✝ : ∀ (a b c : R), a * b * c = a * (b * c)
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
this : toNonUnitalNonAssocRing = toNonUnitalNonAssocRing
⊢ mk mul_assoc✝ = inst₂

Proof state:
case mk.mk
R : Type u
toNonUnitalNonAssocRing✝¹ : NonUnitalNonAssocRing R
mul_assoc✝¹ : ∀ (a b c : R), a * b * c = a * (b * c)
toNonUnitalNonAssocRing✝ : NonUnitalNonAssocRing R
mul_assoc✝ : ∀ (a b c : R), a * b * c = a * (b * c)
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
this : toNonUnitalNonAssocRing = toNonUnitalNonAssocRing
⊢ mk mul_assoc✝¹ = mk mul_assoc✝

Tactic:
congr

Result:
no goals