mathlib-initiative/mathlib-tactics huggingface dataset:
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
x✝⁵ :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)}
      [inst_2 : AddCommGroup N'] [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.lTensor M f = 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)} [inst_2 : AddCommGroup N']
    [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.lTensor M f = 0 ↔ f = 0
N : Type (max u v)
x✝⁴ : AddCommGroup N
x✝³ : Module R N
x✝² : Subsingleton (M ⊗[R] N)
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry (LinearMap.lTensor M LinearMap.id)) x✝¹) x✝ = ((AlgebraTensorModule.curry 0) x✝¹) x✝

Tactic:
;

Goal state after:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝⁵ :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)}
      [inst_2 : AddCommGroup N'] [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.lTensor M f = 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)} [inst_2 : AddCommGroup N']
    [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.lTensor M f = 0 ↔ f = 0
N : Type (max u v)
x✝⁴ : AddCommGroup N
x✝³ : Module R N
x✝² : Subsingleton (M ⊗[R] N)
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry (LinearMap.lTensor M LinearMap.id)) x✝¹) x✝ = ((AlgebraTensorModule.curry 0) x✝¹) x✝
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
x✝⁵ :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)}
      [inst_2 : AddCommGroup N'] [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.rTensor M f = 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)} [inst_2 : AddCommGroup N']
    [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.rTensor M f = 0 ↔ f = 0
N : Type (max u v)
x✝⁴ : AddCommGroup N
x✝³ : Module R N
x✝² : Subsingleton (N ⊗[R] M)
x✝¹ : N
x✝ : M
⊢ ((AlgebraTensorModule.curry (LinearMap.rTensor M LinearMap.id)) x✝¹) x✝ = ((AlgebraTensorModule.curry 0) x✝¹) x✝

Tactic:
;

Goal state after:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝⁵ :
  Flat R M ∧
    ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)}
      [inst_2 : AddCommGroup N'] [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.rTensor M f = 0 ↔ f = 0
flat : Flat R M
Z :
  ∀ {N : Type (max u v)} [inst : AddCommGroup N] [inst_1 : Module R N] {N' : Type (max u v)} [inst_2 : AddCommGroup N']
    [inst_3 : Module R N'] (f : N →ₗ[R] N'), LinearMap.rTensor M f = 0 ↔ f = 0
N : Type (max u v)
x✝⁴ : AddCommGroup N
x✝³ : Module R N
x✝² : Subsingleton (N ⊗[R] M)
x✝¹ : N
x✝ : M
⊢ ((AlgebraTensorModule.curry (LinearMap.rTensor M LinearMap.id)) x✝¹) x✝ = ((AlgebraTensorModule.curry 0) x✝¹) x✝
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
⊢ 1 ∉ J

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
⊢ 1 ∉ J
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
x₁ x₂ : S ⊗[R] T
t₁ : T
r₁ : R
a₁ : S
hr₁ : r₁ • t₁ ∉ J
e₁ : 1 ⊗ₜ[R] (r₁ • t₁) * x₁ = a₁ ⊗ₜ[R] t₁
t₂ : T
r₂ : R
a₂ : S
hr₂ : r₂ • t₂ ∉ J
e₂ : 1 ⊗ₜ[R] (r₂ • t₂) * x₂ = a₂ ⊗ₜ[R] t₂
⊢ (r₁ • r₂) • t₁ • t₂ = (r₁ • t₁) • r₂ • t₂

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
x₁ x₂ : S ⊗[R] T
t₁ : T
r₁ : R
a₁ : S
hr₁ : r₁ • t₁ ∉ J
e₁ : 1 ⊗ₜ[R] (r₁ • t₁) * x₁ = a₁ ⊗ₜ[R] t₁
t₂ : T
r₂ : R
a₂ : S
hr₂ : r₂ • t₂ ∉ J
e₂ : 1 ⊗ₜ[R] (r₂ • t₂) * x₂ = a₂ ⊗ₜ[R] t₂
⊢ (r₁ • r₂) • t₁ • t₂ = (r₁ • t₁) • r₂ • t₂
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
S : Type u_2
inst✝⁵ : CommRing S
T : Type u_3
inst✝⁴ : CommRing T
S' : Type u_4
inst✝³ : CommRing S'
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R S'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
this✝ : Algebra S S' := f.toAlgebra
this : IsScalarTower R S S'
⊢ Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T) =
    (↑(Algebra.TensorProduct.cancelBaseChange R S S S' T)).comp Algebra.TensorProduct.includeRight

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
S : Type u_2
inst✝⁵ : CommRing S
T : Type u_3
inst✝⁴ : CommRing T
S' : Type u_4
inst✝³ : CommRing S'
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R S'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
this✝ : Algebra S S' := f.toAlgebra
this : IsScalarTower R S S'
⊢ Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T) =
    (↑(Algebra.TensorProduct.cancelBaseChange R S S S' T)).comp Algebra.TensorProduct.includeRight
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
S : Type u_2
inst✝⁵ : CommRing S
T : Type u_3
inst✝⁴ : CommRing T
S' : Type u_4
inst✝³ : CommRing S'
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R S'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
this✝ : Algebra S S' := f.toAlgebra
this : IsScalarTower R S S'
x✝ : T
⊢ ((AlgHom.restrictScalars R (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T))).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            ((↑(Algebra.TensorProduct.cancelBaseChange R S S S' T)).comp Algebra.TensorProduct.includeRight)).comp
        Algebra.TensorProduct.includeRight)
      x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
S : Type u_2
inst✝⁵ : CommRing S
T : Type u_3
inst✝⁴ : CommRing T
S' : Type u_4
inst✝³ : CommRing S'
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra R S'
f : S →ₐ[R] S'
Hf : f.SurjectiveOnStalks
this✝ : Algebra S S' := f.toAlgebra
this : IsScalarTower R S S'
x✝ : T
⊢ ((AlgHom.restrictScalars R (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T))).comp
        Algebra.TensorProduct.includeRight)
      x✝ =
    ((AlgHom.restrictScalars R
            ((↑(Algebra.TensorProduct.cancelBaseChange R S S S' T)).comp Algebra.TensorProduct.includeRight)).comp
        Algebra.TensorProduct.includeRight)
      x✝
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
I : Ideal R
inst✝ : I.IsPrime
x : I.ResidueField
⊢ ∃ x_1, x * (algebraMap (R ⧸ I) I.ResidueField) ↑x_1.2 = (algebraMap (R ⧸ I) I.ResidueField) x_1.1

Tactic:
obtain ⟨x, rfl⟩ := IsLocalRing.residue_surjective x

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
I : Ideal R
inst✝ : I.IsPrime
x : Localization.AtPrime I
⊢ ∃ x_1,
    (IsLocalRing.residue (Localization.AtPrime I)) x * (algebraMap (R ⧸ I) I.ResidueField) ↑x_1.2 =
      (algebraMap (R ⧸ I) I.ResidueField) x_1.1
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hac : a ≤ c
hbc : b ≤ c
⊢ (↑a).1 * (↑c).1 + (↑a).2 * ((↑b).1 * (↑c).1) = (↑a).1 + (↑a).2 * (↑b).1

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hac : a ≤ c
hbc : b ≤ c
⊢ (↑a).1 * (↑c).1 + (↑a).2 * ((↑b).1 * (↑c).1) = (↑a).1 + (↑a).2 * (↑b).1
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case inl
ι : Type u_3
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
x✝¹ x✝ : (i : ι) × PrimeSpectrum (R i)
i : ι
p q : PrimeSpectrum (R i)
eq : sigmaToPi R ⟨i, p⟩ = sigmaToPi R ⟨i, q⟩
⊢ p = q

Tactic:
;

Goal state after:
case inl
ι : Type u_3
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
x✝¹ x✝ : (i : ι) × PrimeSpectrum (R i)
i : ι
p q : PrimeSpectrum (R i)
eq : sigmaToPi R ⟨i, p⟩ = sigmaToPi R ⟨i, q⟩
⊢ p = q
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hab : a ≤ b
hac : a ≤ c
⊢ (↑a).1 * (↑b).1 * (↑c).1 = (↑a).1

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hab : a ≤ b
hac : a ≤ c
⊢ (↑a).1 * (↑b).1 * (↑c).1 = (↑a).1
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
I : Ideal A
inst✝ : I.IsPrime
x✝ : A
⊢ ((mapₐ I I (AlgHom.id R A) ⋯).comp (IsScalarTower.toAlgHom R A I.ResidueField)) x✝ =
    ((AlgHom.id R I.ResidueField).comp (IsScalarTower.toAlgHom R A I.ResidueField)) x✝

Tactic:
;

Goal state after:
R : Type u_1
A : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
I : Ideal A
inst✝ : I.IsPrime
x✝ : A
⊢ ((mapₐ I I (AlgHom.id R A) ⋯).comp (IsScalarTower.toAlgHom R A I.ResidueField)) x✝ =
    ((AlgHom.id R I.ResidueField).comp (IsScalarTower.toAlgHom R A I.ResidueField)) x✝
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case pos
ι : Type u_3
R : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
val✝ : Fintype ι
e : ι → (i : ι) → R i := fun i ↦ Function.update 1 i 0
H : ∏ i, e i = 0
i : ι
hi : e i ∈ p.asIdeal
h₁ : Function.Surjective ⇑(Pi.evalRingHom R i) := RingHomSurjective.is_surjective
x : (i : ι) → R i
hx : x ∈ ker (Pi.evalRingHom R i)
⊢ x i = (x * e i) i

Tactic:
;

Goal state after:
case pos
ι : Type u_3
R : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
val✝ : Fintype ι
e : ι → (i : ι) → R i := fun i ↦ Function.update 1 i 0
H : ∏ i, e i = 0
i : ι
hi : e i ∈ p.asIdeal
h₁ : Function.Surjective ⇑(Pi.evalRingHom R i) := RingHomSurjective.is_surjective
x : (i : ι) → R i
hx : x ∈ ker (Pi.evalRingHom R i)
⊢ x i = (x * e i) i
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b : { a // IsIdempotentElem a }
⊢ ↑a * ↑a * ↑b = ↑a * ↑b

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b : { a // IsIdempotentElem a }
⊢ ↑a * ↑a * ↑b = ↑a * ↑b
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b : { a // IsIdempotentElem a }
⊢ ↑a * (↑b * ↑b) = ↑a * ↑b

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b : { a // IsIdempotentElem a }
⊢ ↑a * (↑b * ↑b) = ↑a * ↑b
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b c : { a // IsIdempotentElem a }
hab : ↑a * ↑b = ↑a
hac : ↑a * ↑c = ↑a
⊢ ↑a * ↑b * ↑c = ↑a

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b c : { a // IsIdempotentElem a }
hab : ↑a * ↑b = ↑a
hac : ↑a * ↑c = ↑a
⊢ ↑a * ↑b * ↑c = ↑a
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : { a // IsIdempotentElem a }
⊢ ↑a * ↑a + ↑a * ↑b - ↑a * (↑a * ↑b) = ↑a

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : { a // IsIdempotentElem a }
⊢ ↑a * ↑a + ↑a * ↑b - ↑a * (↑a * ↑b) = ↑a
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
⊢ (∃ x, I ≤ x.asIdeal ∧ comap f x = p) → Ideal.comap f I ≤ p.asIdeal

Tactic:
rintro ⟨p, hp, rfl⟩ a ha
    exact hp ha

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : { a // IsIdempotentElem a }
⊢ ↑b * ↑a + ↑b * ↑b - ↑b * (↑a * ↑b) = ↑b

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : { a // IsIdempotentElem a }
⊢ ↑b * ↑a + ↑b * ↑b - ↑b * (↑a * ↑b) = ↑b
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b c : { a // IsIdempotentElem a }
hac : a ≤ c
hbc : b ≤ c
⊢ ↑a * ↑c + ↑b * ↑c - ↑a * (↑b * ↑c) = ↑a + ↑b - ↑a * ↑b

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b c : { a // IsIdempotentElem a }
hac : a ≤ c
hbc : b ≤ c
⊢ ↑a * ↑c + ↑b * ↑c - ↑a * (↑b * ↑c) = ↑a + ↑b - ↑a * ↑b
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this : map (algebraMap R (Localization.AtPrime p)) p ≤ (map (algebraMap R (Localization.AtPrime p)) I).radical
n : ℕ
a : ↥I
b t : ↥p.primeCompl
ht : ↑t * (x ^ n * ↑b) = ↑t * ↑a
⊢ (x * (↑t * ↑b)) ^ (n + 1) = ↑t ^ n * ↑b ^ n * x * (↑t * (x ^ n * ↑b))

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this : map (algebraMap R (Localization.AtPrime p)) p ≤ (map (algebraMap R (Localization.AtPrime p)) I).radical
n : ℕ
a : ↥I
b t : ↥p.primeCompl
ht : ↑t * (x ^ n * ↑b) = ↑t * ↑a
⊢ (x * (↑t * ↑b)) ^ (n + 1) = ↑t ^ n * ↑b ^ n * x * (↑t * (x ^ n * ↑b))
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : { a // IsIdempotentElem a }
⊢ 1 = ↑⊤

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommRing R
a : { a // IsIdempotentElem a }
⊢ 1 = ↑⊤
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 : α → α → α
eq_inf : inf = min
a✝ : α
⊢ le a✝ a✝

Tactic:
;

Goal state after:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ : α
⊢ le a✝ a✝
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 : α → α → α
eq_inf : inf = min
a✝ b✝ c✝ : α
hab : le a✝ b✝
hbc : le b✝ c✝
⊢ le a✝ c✝

Tactic:
;

Goal state after:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ c✝ : α
hab : le a✝ b✝
hbc : le b✝ c✝
⊢ le a✝ c✝
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 : α → α → α
eq_inf : inf = min
a✝ b✝ c✝ : α
hab : a✝ ≤ b✝
hbc : b✝ ≤ c✝
⊢ a✝ ≤ c✝

Tactic:
;

Goal state after:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ c✝ : α
hab : a✝ ≤ b✝
hbc : b✝ ≤ c✝
⊢ a✝ ≤ c✝
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 : α → α → α
eq_inf : inf = min
a✝ b✝ : α
hab : le a✝ b✝
hba : le b✝ a✝
⊢ a✝ = b✝

Tactic:
;

Goal state after:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ : α
hab : le a✝ b✝
hba : le b✝ a✝
⊢ a✝ = b✝
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 : α → α → α
eq_inf : inf = min
a✝ b✝ : α
hab : a✝ ≤ b✝
hba : b✝ ≤ a✝
⊢ a✝ = b✝

Tactic:
;

Goal state after:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ : α
hab : a✝ ≤ b✝
hba : b✝ ≤ a✝
⊢ a✝ = b✝
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 : α → α → α
eq_inf : inf = min
a✝ b✝ : α
⊢ le a✝ (sup a✝ b✝)

Tactic:
;

Goal state after:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ : α
⊢ le a✝ (sup a✝ b✝)
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 : α → α → α
eq_inf : inf = min
a✝ b✝ : α
⊢ le b✝ (sup a✝ b✝)

Tactic:
;

Goal state after:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ : α
⊢ le b✝ (sup a✝ b✝)
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 : α → α → α
eq_inf : inf = min
a✝ b✝ c✝ : α
hac : le a✝ c✝
hbc : le b✝ c✝
⊢ le (sup a✝ b✝) c✝

Tactic:
;

Goal state after:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ c✝ : α
hac : le a✝ c✝
hbc : le b✝ c✝
⊢ le (sup a✝ b✝) c✝
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 : α → α → α
eq_inf : inf = min
a✝ b✝ c✝ : α
hac : a✝ ≤ c✝
hbc : b✝ ≤ c✝
⊢ sup a✝ b✝ ≤ c✝

Tactic:
;

Goal state after:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ c✝ : α
hac : a✝ ≤ c✝
hbc : b✝ ≤ c✝
⊢ sup a✝ b✝ ≤ c✝
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 : α → α → α
eq_inf : inf = min
a✝ b✝ : α
⊢ le (inf a✝ b✝) a✝

Tactic:
;

Goal state after:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ : α
⊢ le (inf a✝ b✝) a✝
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 : α → α → α
eq_inf : inf = min
a✝ b✝ : α
⊢ le (inf a✝ b✝) b✝

Tactic:
;

Goal state after:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ : α
⊢ le (inf a✝ b✝) b✝
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 : α → α → α
eq_inf : inf = min
a✝ b✝ c✝ : α
hac : le a✝ b✝
hbc : le a✝ c✝
⊢ le a✝ (inf b✝ c✝)

Tactic:
;

Goal state after:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ c✝ : α
hac : le a✝ b✝
hbc : le a✝ c✝
⊢ le a✝ (inf b✝ c✝)
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 : α → α → α
eq_inf : inf = min
a✝ b✝ c✝ : α
hac : a✝ ≤ b✝
hbc : a✝ ≤ c✝
⊢ a✝ ≤ inf b✝ c✝

Tactic:
;

Goal state after:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ c✝ : α
hac : a✝ ≤ b✝
hbc : a✝ ≤ c✝
⊢ a✝ ≤ inf b✝ c✝
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 : α → α → α
eq_inf : inf = min
x✝ y✝ z✝ : α
⊢ (x✝ ⊔ y✝) ⊓ (x✝ ⊔ z✝) ≤ x✝ ⊔ y✝ ⊓ z✝

Tactic:
;

Goal state after:
α : Type u
c : DistribLattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
x✝ y✝ z✝ : α
⊢ (x✝ ⊔ y✝) ⊓ (x✝ ⊔ z✝) ≤ x✝ ⊔ y✝ ⊓ z✝
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 : α → α → α
eq_himp : himp = HImp.himp
⊢ ∀ (x y : α), x ≤ y ↔ le x y

Tactic:
;

Goal state after:
α : 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 : α → α → α
eq_himp : himp = HImp.himp
⊢ ∀ (x y : α), x ≤ y ↔ le x y
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 : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
⊢ ∀ (x y : α), x ≤ y ↔ le x y

Tactic:
;

Goal state after:
α : 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 : α → α → α
eq_sdiff : sdiff = SDiff.sdiff
⊢ ∀ (x y : α), x ≤ y ↔ le x y
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 : α → α
eq_compl : compl = Compl.compl
⊢ ∀ (x y : α), x ≤ y ↔ le x y

Tactic:
;

Goal state after:
α : 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 : α → α
eq_compl : compl = Compl.compl
⊢ ∀ (x y : α), x ≤ y ↔ le x y
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 : α → α
eq_hnot : hnot = HNot.hnot
⊢ ∀ (x y : α), x ≤ y ↔ le x y

Tactic:
;

Goal state after:
α : 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 : α → α
eq_hnot : hnot = HNot.hnot
⊢ ∀ (x y : α), x ≤ y ↔ le x y
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 : α → α → α
eq_inf : inf = min
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
a✝ : α
⊢ a✝ ≤ top

Tactic:
;

Goal state after:
α : 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 : α → α → α
eq_inf : inf = min
sSup : Set α → α
eq_sSup : sSup = SupSet.sSup
sInf : Set α → α
eq_sInf : sInf = InfSet.sInf
a✝ : α
⊢ a✝ ≤ top