mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A
y : B
h : IsIntegral R y
⊢ IsIntegral A (x ⊗ₜ[R] y)

Tactic:
← mul_one x,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A
y : B
h : IsIntegral R y
⊢ IsIntegral A ((x * 1) ⊗ₜ[R] y)
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
k n : ℕ
r : R
i : ℕ
hnik : ¬n = i + k
hkn : k ≤ n
⊢ 0 = if n - k = i then ↑(n.choose k) * r else 0

Tactic:
rw [← tsub_eq_iff_eq_add_of_le hkn] at hnik
      rw [if_neg hnik]

Goal state after:
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k : ℕ
⊢ ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]

Tactic:
induction k with
  | zero => rw [hasseDeriv_zero, factorial_zero, iterate_zero, one_smul, LinearMap.id_coe]
  | succ k ih => ?_
  ext f n : 2
  rw [iterate_succ_apply', ← ih]
  simp only [LinearMap.smul_apply, coeff_smul, LinearMap.map_smul_of_tower, coeff_derivative,
    hasseDeriv_coeff, ← @choose_symm_add _ k]
  simp only [nsmul_eq_mul, factorial_succ, mul_assoc, succ_eq_add_one, ← add_assoc,
    add_right_comm n 1 k, ← cast_succ]
  rw [← (cast_commute (n + 1) (f.coeff (n + k + 1))).eq]
  simp only [← mul_assoc]
  norm_cast
  congr 2
  rw [mul_comm (k + 1) _, mul_assoc, mul_assoc]
  congr 1
  have : n + k + 1 = n + (k + 1) := by apply add_assoc
  rw [← choose_symm_of_eq_add this, choose_succ_right_eq, mul_comm]
  congr
  rw [add_assoc, add_tsub_cancel_left]

Goal state after:
Module: Mathlib.Algebra.Polynomial.HasseDeriv

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
this : ((hasseDeriv f.natDegree) f).natDegree ≤ 0
⊢ C (↑((0 + f.natDegree).choose f.natDegree) * f.coeff (0 + f.natDegree)) = C f.leadingCoeff

Tactic:
zero_add,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
this : ((hasseDeriv f.natDegree) f).natDegree ≤ 0
⊢ C (↑(f.natDegree.choose f.natDegree) * f.coeff f.natDegree) = C f.leadingCoeff
Module: Mathlib.RingTheory.Polynomial.IntegralNormalization

Goal state before:
pp: case inl
R : Type u
inst✝¹ : Semiring R
A : Type u_1
inst✝ : Semiring A
p : R[X]
f : R →+* A
z : A
hz : eval₂ f z p = 0
h₁ : Commute (f p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
inj : ∀ (x : R), f x = 0 → x = 0
h : p.natDegree = 0
⊢ eval₂ f (f p.leadingCoeff * z) p.integralNormalization = 0

Tactic:
by_cases h0 : coeff p 0 = 0

Goal state after:
case pos
R : Type u
inst✝¹ : Semiring R
A : Type u_1
inst✝ : Semiring A
p : R[X]
f : R →+* A
z : A
hz : eval₂ f z p = 0
h₁ : Commute (f p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
inj : ∀ (x : R), f x = 0 → x = 0
h : p.natDegree = 0
h0 : p.coeff 0 = 0
⊢ eval₂ f (f p.leadingCoeff * z) p.integralNormalization = 0

case neg
R : Type u
inst✝¹ : Semiring R
A : Type u_1
inst✝ : Semiring A
p : R[X]
f : R →+* A
z : A
hz : eval₂ f z p = 0
h₁ : Commute (f p.leadingCoeff) z
h₂ : ∀ {r r' : R}, Commute (f r) (f r')
inj : ∀ (x : R), f x = 0 → x = 0
h : p.natDegree = 0
h0 : ¬p.coeff 0 = 0
⊢ eval₂ f (f p.leadingCoeff * z) p.integralNormalization = 0
Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra

Goal state before:
pp: R : Type u_1
M : Type u_2
A : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : CommMonoid M
a : A
p : R[M]
a✝ : M
⊢ ((scalarTensorEquiv R A) (a ⊗ₜ[R] p)).coeff a✝ = (a • (mapAlgHom M (ofId R A)) p).coeff a✝

Tactic:
simp [scalarTensorEquiv]

Goal state after:
R : Type u_1
M : Type u_2
A : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : CommMonoid M
a : A
p : R[M]
a✝ : M
⊢ p.coeff a✝ • a = a * (algebraMap R A) (p.coeff a✝)
Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra

Goal state before:
pp: R : Type u_1
M : Type u_2
A : Type u_5
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : CommMonoid M
m : M
a : A
⊢ (scalarTensorEquiv R A).symm (single m a) = a ⊗ₜ[R] single m 1

Tactic:
simp [scalarTensorEquiv]

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : DivisionRing S
inst✝ : Algebra R S
x : S
int : IsIntegral R x
h0 : x ≠ 0
⊢ x⁻¹ ∈ R[x]

Tactic:
have : FiniteDimensional R (R[x]) := .of_fg int.fg_adjoin_singleton

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : DivisionRing S
inst✝ : Algebra R S
x : S
int : IsIntegral R x
h0 : x ≠ 0
this : FiniteDimensional R ↥R[x]
⊢ x⁻¹ ∈ R[x]
Module: Mathlib.RingTheory.Ideal.GoingUp

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
⊢ Function.Injective
    ⇑(quotientMap (map (mapRingHom (Quotient.mk (comap C P))) P) (mapRingHom (Quotient.mk (comap C P))) ⋯)

Tactic:
by
  refine quotientMap_injective' (le_of_eq ?_)
  rw [comap_map_of_surjective (mapRingHom (Ideal.Quotient.mk (P.comap (C : R →+* R[X]))))
      (map_surjective (Ideal.Quotient.mk (P.comap (C : R →+* R[X]))) Ideal.Quotient.mk_surjective)]
  refine le_antisymm (sup_le le_rfl ?_) (le_sup_of_le_left le_rfl)
  refine fun p hp =>
    polynomial_mem_ideal_of_coeff_mem_ideal P p fun n => Ideal.Quotient.eq_zero_iff_mem.mp ?_
  simpa only [coeff_map, coe_mapRingHom] using! ext_iff.mp (Ideal.mem_bot.mp (mem_comap.mp hp)) n

Goal state after:
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing Sₘ
inst✝⁴ : Algebra R S
inst✝³ : Algebra S Sₘ
inst✝² : Algebra R Sₘ
inst✝¹ : IsScalarTower R S Sₘ
r : S
hr : IsIntegral R r
inst✝ : Away r Sₘ
x : S
a : ↥(Submonoid.powers r)
hx : IsIntegral R (mk' Sₘ x a)
⊢ ∃ n, IsIntegral R (r ^ n * x)

Tactic:
refine IsLocalization.Away.exists_isIntegral_mul_of_isIntegral_algebraMap (Sₘ := Sₘ) hr ?_
  obtain ⟨_, ⟨n, rfl⟩⟩ := a
  convert! (hr.pow n).algebraMap.mul hx
  exact (mk'_spec'_mk ..).symm

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
⊢ ∃ y, y ≠ 0 ∧ ∀ z ∈ s, IsIntegral R (y • z)

Tactic:
have := Algebra.IsAlgebraic.nontrivial R A
  choose r hr int using fun x ↦ (alg.1 x).exists_integral_multiple
  refine ⟨∏ x ∈ s, r x, Finset.prod_ne_zero_iff.mpr fun _ _ ↦ hr _, fun _ h ↦ ?_⟩
  classical rw [← Finset.prod_erase_mul _ _ h, mul_smul]
  exact (int _).smul _

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h✝ : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : (C y * X).leadingCoeff ^ p.natDegree = 0
hy0 : y ≠ 0
⊢ False

pp: R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h✝ : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : (p.comp (C y * X)).coeff (p.natDegree * (C y * X).natDegree) = 0
hy0 : y ≠ 0
⊢ (C y * X).natDegree ≠ 0

Tactic:
leadingCoeff_C_mul_X

Goal state after:
R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h✝ : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : y ^ p.natDegree = 0
hy0 : y ≠ 0
⊢ False

R : Type u_1
A : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h✝ : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : (p.comp (C y * X)).coeff (p.natDegree * (C y * X).natDegree) = 0
hy0 : y ≠ 0
⊢ (C y * X).natDegree ≠ 0
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case refine_1.refine_1
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
⊢ q'.natDegree ≤ q.natDegree + N

Tactic:
refine natDegree_sum_le_of_forall_le _ _ fun i hi ↦ ?_

Goal state after:
case refine_1.refine_1
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
a✝ : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun x ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun i r ↦ X ^ i * reflect N r
this : ∀ (i : ℕ), (aeval t) (reflect N (q.coeff i)) = t ^ N * (aeval s) (q.coeff i)
i : ℕ
hi : i ∈ q.support
⊢ ((fun i r ↦ X ^ i * reflect N r) i (q.coeff i)).natDegree ≤ q.natDegree + N
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N1 : Type u_1
inst✝⁵ : AddCommGroup N1
inst✝⁴ : Module R N1
N2 : Type u_2
inst✝³ : AddCommGroup N2
inst✝² : Module R N2
N3 : Type u_3
inst✝¹ : AddCommGroup N3
inst✝ : Module R N3
l12 : N1 →ₗ[R] N2
l23 : N2 →ₗ[R] N3
fl : FaithfullyFlat R M
ex : Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
complex : l12.range ≤ l23.ker
H : Type u_2 := ↥l23.ker ⧸ (Submodule.inclusion complex).range
triv_coh : Subsingleton H
⊢ l23.ker = l12.range

Tactic:
by
    rw [Submodule.Quotient.subsingleton_iff, Submodule.range_inclusion,
      Submodule.comap_subtype_eq_top] at triv_coh
    exact le_antisymm triv_coh complex

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ s ⊆ zeroLocus Set.univ ↔ s = ∅

Tactic:
zeroLocus_univ,

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ s ⊆ ∅ ↔ s = ∅
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t t' : Set (PrimeSpectrum R)
⊢ vanishingIdeal t ⊔ vanishingIdeal t' ≤ vanishingIdeal (t ∩ t')

Tactic:
by
  intro r
  rw [Submodule.mem_sup, mem_vanishingIdeal]
  rintro ⟨f, hf, g, hg, rfl⟩ x ⟨hxt, hxt'⟩
  rw [mem_vanishingIdeal] at hf hg
  apply Submodule.add_mem <;> solve_by_elim

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ IsMax x ↔ x.asIdeal.IsMaximal

Tactic:
by
  refine ⟨fun hx ↦ ⟨⟨x.2.ne_top, fun I hI ↦ ?_⟩⟩, fun hx y e ↦ (hx.eq_of_le y.2.ne_top e).ge⟩
  by_contra e
  obtain ⟨m, hm, hm'⟩ := Ideal.exists_le_maximal I e
  exact hx.not_lt (show x < ⟨m, hm.isPrime⟩ from hI.trans_le hm')

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
J : Ideal ((i : ι) → R i) :=
  let __spread.0 := AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom;
  { toAddSubmonoid := __spread.0, smul_mem' := ⋯ }
I : Ideal ((i : ι) → R i)
max : I.IsMaximal
le : J ≤ I
x✝ : { asIdeal := I, isPrime := ⋯ } ∈ Set.range (sigmaToPi R)
i : ι
p : PrimeSpectrum (R i)
eq : sigmaToPi R ⟨i, p⟩ = { asIdeal := I, isPrime := ⋯ }
this : ⇑(DFinsupp.single i 1) ∉ { asIdeal := I, isPrime := ⋯ }.asIdeal
⊢ False

Tactic:
exact this (le ⟨.single i 1, rfl⟩)

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal S
⊢ (comap f I).minimalPrimes = comap f '' I.minimalPrimes

Tactic:
ext J
  constructor
  · intro H
    obtain ⟨p, h, rfl⟩ := Ideal.exists_minimalPrimes_comap_eq f J H
    exact ⟨p, h, rfl⟩
  · rintro ⟨J, hJ, rfl⟩
    exact Ideal.minimalPrimes_comap_of_surjective hf hJ

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
h h' : LE α
c : OrderTop α
top : α
⊢ Top α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
h h' : LE α
c : OrderBot α
bot : α
⊢ Bot α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
h h' : LE α
c : BoundedOrder α
top : α
⊢ Top α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
h h' : LE α
c : BoundedOrder α
top : α
eq_top : top = ⊤
bot : α
⊢ Bot α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : Lattice α
le : α → α → Prop
⊢ LE α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
⊢ Max α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
⊢ Min α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : DistribLattice α
le : α → α → Prop
⊢ LE α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
⊢ Max α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
⊢ Min α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : GeneralizedHeytingAlgebra α
le : α → α → Prop
⊢ LE α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : GeneralizedHeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
⊢ Top α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : GeneralizedHeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
sup : α → α → α
⊢ Max α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : GeneralizedHeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
⊢ Min α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : GeneralizedHeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
himp : α → α → α
⊢ HImp α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Bijective ⇑f
⊢ (mapPiLocalization f hf).comp ↑(toPiLocalization R) = (toPiLocalization S).comp f

Tactic:
ext r I
  change Localization.localRingHom _ _ _ rfl (algebraMap _ _ r) = algebraMap _ _ (f r)
  simp_rw [← IsLocalization.mk'_one (M := (I.1.comap f).primeCompl), Localization.localRingHom_mk',
    ← IsLocalization.mk'_one (M := I.1.primeCompl), Submonoid.coe_one, map_one f]
  rfl

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : GeneralizedCoheytingAlgebra α
le : α → α → Prop
⊢ LE α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : GeneralizedCoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
bot : α
⊢ Bot α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : GeneralizedCoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
bot : α
eq_bot : bot = ⊥
sup : α → α → α
⊢ Max α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : GeneralizedCoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
⊢ Min α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : GeneralizedCoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
⊢ SDiff α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : HeytingAlgebra α
le : α → α → Prop
⊢ LE α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : HeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
⊢ Top α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : HeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
⊢ Bot α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : HeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
⊢ Max α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : HeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
⊢ Min α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : HeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
himp : α → α → α
⊢ HImp α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : HeytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
himp : α → α → α
eq_himp : himp = HImp.himp
compl : α → α
⊢ Compl α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CoheytingAlgebra α
le : α → α → Prop
⊢ LE α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
⊢ Top α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
⊢ Bot α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
⊢ Max α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
⊢ Min α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
⊢ SDiff α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CoheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
⊢ HNot α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : BiheytingAlgebra α
le : α → α → Prop
⊢ LE α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : BiheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
⊢ Top α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : BiheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
⊢ Bot α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : BiheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
⊢ Max α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : BiheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
⊢ Min α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : BiheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
⊢ SDiff α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : BiheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
⊢ HNot α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : BiheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
eq_hnot : hnot = HNot.hnot
himp : α → α → α
⊢ HImp α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : BiheytingAlgebra α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
sdiff : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
hnot : α → α
eq_hnot : hnot = HNot.hnot
himp : α → α → α
eq_himp : himp = HImp.himp
compl : α → α
⊢ Compl α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CompleteLattice α
le : α → α → Prop
⊢ LE α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
⊢ Top α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
⊢ Bot α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
⊢ Max α

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : CompleteLattice α
le : α → α → Prop
eq_le : le = LE.le
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
⊢ Min α

Tactic:
by infer_instance

Goal state after: