harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/Additive/DoublingConst.lean
/-- If `A` has small doubling, then it has small difference, with the constant squared.

This is a consequence of the Ruzsa triangle inequality. -/
@[to_additive
"If `A` has small doubling, then it has small difference, with the constant squared.

This is a consequence of the Ruzsa triangle inequality."]
lemma divConst_le_mulConst_sq : δₘ[A] ≤ σₘ[A] ^ 2

Proof state:
case inl
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
⊢ δₘ[∅] ≤ σₘ[∅] ^ 2

Tactic:
simp

Result:
no goals

Proof state:
case inr
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ δₘ[A] * (↑(#A) * ↑(#A)) ≤ σₘ[A] ^ 2 * (↑(#A) * ↑(#A))

Tactic:
calc
  _ = #(A / A) * (#A : ℚ≥0) := by rw [← mul_assoc, divConst_mul_card]
  _ ≤ #(A * A) * #(A * A) := by norm_cast; exact ruzsa_triangle_inequality_div_mul_mul ..
  _ = _ := by rw [← mulConst_mul_card]; ring

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ 0 < ↑(#A) * ↑(#A)

Tactic:
positivity

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ δₘ[A] * (↑(#A) * ↑(#A)) = ↑(#(A / A)) * ↑(#A)

Tactic:
rw [← mul_assoc, divConst_mul_card]

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ ↑(#(A * A)) * ↑(#(A * A)) = σₘ[A] ^ 2 * (↑(#A) * ↑(#A))

Tactic:
rw [← mulConst_mul_card]

Result:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ σₘ[A] * ↑(#A) * (σₘ[A] * ↑(#A)) = σₘ[A] ^ 2 * (↑(#A) * ↑(#A))

Proof state:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ #(A / A) * #A ≤ #(A * A) * #(A * A)

Tactic:
exact ruzsa_triangle_inequality_div_mul_mul ..

Result:
no goals

Proof state:
case inr
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ δₘ[A] ≤ σₘ[A] ^ 2

Tactic:
refine le_of_mul_le_mul_right ?_ (by positivity : (0 : ℚ≥0) < #A * #A)

Result:
case inr
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ δₘ[A] * (↑(#A) * ↑(#A)) ≤ σₘ[A] ^ 2 * (↑(#A) * ↑(#A))

Proof state:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ σₘ[A] * ↑(#A) * (σₘ[A] * ↑(#A)) = σₘ[A] ^ 2 * (↑(#A) * ↑(#A))

Tactic:
ring

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ ↑(#(A / A)) * ↑(#A) ≤ ↑(#(A * A)) * ↑(#(A * A))

Tactic:
norm_cast

Result:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ #(A / A) * #A ≤ #(A * A) * #(A * A)

Proof state:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
⊢ δₘ[A] ≤ σₘ[A] ^ 2

Tactic:
obtain rfl | hA' := A.eq_empty_or_nonempty

Result:
case inl
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
⊢ δₘ[∅] ≤ σₘ[∅] ^ 2

case inr
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ δₘ[A] ≤ σₘ[A] ^ 2
-- Mathlib/Data/PNat/Xgcd.lean
theorem finish_v (hr : u.r = 0) : u.finish.v = u.v

Proof state:
u : XgcdType
hr : u.r = 0
⊢ u.finish.v = u.v

Tactic:
let ha : u.r + u.b * u.q = u.a := u.rq_eq

Result:
u : XgcdType
hr : u.r = 0
ha : u.r + ↑u.b * u.q = ↑u.a := rq_eq u
⊢ u.finish.v = u.v

Proof state:
case fst
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
this : u.wp + 1 = ↑u.w
⊢ (u.wp + 1) * ↑u.b + ((u.wp + 1) * u.qp + u.x) * ↑u.b = ↑u.w * ↑u.a + u.x * ↑u.b

Tactic:
rw [this, ← ha, u.qp_eq hr]

Result:
case fst
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
this : u.wp + 1 = ↑u.w
⊢ ↑u.w * ↑u.b + (↑u.w * u.qp + u.x) * ↑u.b = ↑u.w * (↑u.b * (u.qp + 1)) + u.x * ↑u.b

Proof state:
case snd
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
⊢ u.finish.v.2 = u.v.2

Tactic:
change u.y * u.b + (u.y * u.qp + u.z) * u.b = u.y * u.a + u.z * u.b

Result:
case snd
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
⊢ u.y * ↑u.b + (u.y * u.qp + ↑u.z) * ↑u.b = u.y * ↑u.a + ↑u.z * ↑u.b

Proof state:
case fst
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
this : u.wp + 1 = ↑u.w
⊢ ↑u.w * ↑u.b + (↑u.w * u.qp + u.x) * ↑u.b = ↑u.w * (↑u.b * (u.qp + 1)) + u.x * ↑u.b

Tactic:
ring

Result:
no goals

Proof state:
case snd
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
⊢ u.y * ↑u.b + (u.y * u.qp + ↑u.z) * ↑u.b = u.y * ↑u.a + ↑u.z * ↑u.b

Tactic:
rw [← ha, u.qp_eq hr]

Result:
case snd
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
⊢ u.y * ↑u.b + (u.y * u.qp + ↑u.z) * ↑u.b = u.y * (↑u.b * (u.qp + 1)) + ↑u.z * ↑u.b

Proof state:
case snd
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
⊢ u.y * ↑u.b + (u.y * u.qp + ↑u.z) * ↑u.b = u.y * (↑u.b * (u.qp + 1)) + ↑u.z * ↑u.b

Tactic:
ring

Result:
no goals

Proof state:
case fst
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
⊢ (u.wp + 1) * ↑u.b + ((u.wp + 1) * u.qp + u.x) * ↑u.b = ↑u.w * ↑u.a + u.x * ↑u.b

Tactic:
have : u.wp + 1 = u.w := rfl

Result:
case fst
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
this : u.wp + 1 = ↑u.w
⊢ (u.wp + 1) * ↑u.b + ((u.wp + 1) * u.qp + u.x) * ↑u.b = ↑u.w * ↑u.a + u.x * ↑u.b

Proof state:
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
⊢ u.finish.v = u.v

Tactic:
ext

Result:
case fst
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
⊢ u.finish.v.1 = u.v.1

case snd
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
⊢ u.finish.v.2 = u.v.2

Proof state:
u : XgcdType
hr : u.r = 0
ha : u.r + ↑u.b * u.q = ↑u.a := rq_eq u
⊢ u.finish.v = u.v

Tactic:
rw [hr, zero_add] at ha

Result:
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
⊢ u.finish.v = u.v

Proof state:
case fst
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
⊢ u.finish.v.1 = u.v.1

Tactic:
change (u.wp + 1) * u.b + ((u.wp + 1) * u.qp + u.x) * u.b = u.w * u.a + u.x * u.b

Result:
case fst
u : XgcdType
hr : u.r = 0
ha : ↑u.b * u.q = ↑u.a
⊢ (u.wp + 1) * ↑u.b + ((u.wp + 1) * u.qp + u.x) * ↑u.b = ↑u.w * ↑u.a + u.x * ↑u.b
-- Mathlib/Data/List/Cycle.lean
theorem next_ne_head_ne_getLast (h : x ∈ l) (y : α) (h : x ∈ y :: l) (hy : x ≠ y)
    (hx : x ≠ getLast (y :: l) (cons_ne_nil _ _)) :
    next (y :: l) x h = next l x (by simpa [hy] using h)

Proof state:
case x_mem
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h✝ : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x ≠ (y :: l).getLast ⋯
⊢ l ≠ []

Tactic:
exact ne_nil_of_mem (by assumption)

Result:
no goals

Proof state:
case x_mem
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h✝ : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x ≠ (y :: l).getLast ⋯
⊢ x ∈ l

Tactic:
rwa [getLast_cons] at hx

Result:
case x_mem
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h✝ : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x ≠ (y :: l).getLast ⋯
⊢ l ≠ []

Proof state:
case x_ne
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h✝ : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x ≠ (y :: l).getLast ⋯
⊢ x ≠ l.getLast ⋯

Tactic:
rwa [getLast_cons] at hx

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h✝ : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x ≠ (y :: l).getLast ⋯
⊢ x ∈ l

Tactic:
simpa [hy] using h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h✝ : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x ≠ (y :: l).getLast ⋯
⊢ ?m.9287 ∈ l

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h✝ : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x ≠ (y :: l).getLast ⋯
⊢ (y :: l).next x h = l.next x ⋯

Tactic:
rw [next, next, nextOr_cons_of_ne _ _ _ _ hy, nextOr_eq_nextOr_of_mem_of_ne]

Result:
case x_mem
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h✝ : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x ≠ (y :: l).getLast ⋯
⊢ x ∈ l

case x_ne
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h✝ : x ∈ l
y : α
h : x ∈ y :: l
hy : x ≠ y
hx : x ≠ (y :: l).getLast ⋯
⊢ x ≠ l.getLast ⋯
-- Mathlib/Data/Multiset/Range.lean
theorem range_succ (n : ℕ) : range (succ n) = n ::ₘ range n

Proof state:
n : ℕ
⊢ range n.succ = n ::ₘ range n

Tactic:
rw [range, List.range_succ, ← coe_add, Multiset.add_comm, range, coe_singleton, singleton_add]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldrM_push [Monad m] (f : α → β → m β) (init : β) (arr : Vector α n) (a : α) :
    (arr.push a).foldrM f init = f a init >>= arr.foldrM f

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
a : α
arr : Array α
⊢ foldrM f init ({ toArray := arr, size_toArray := ⋯ }.push a) = do
    let b ← f a init
    foldrM f b { toArray := arr, size_toArray := ⋯ }

Tactic:
simp [Array.foldrM_push]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝ : Monad m
f : α → β → m β
init : β
arr : Vector α n
a : α
⊢ foldrM f init (arr.push a) = do
    let b ← f a init
    foldrM f b arr

Tactic:
rcases arr with ⟨arr, rfl⟩

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
a : α
arr : Array α
⊢ foldrM f init ({ toArray := arr, size_toArray := ⋯ }.push a) = do
    let b ← f a init
    foldrM f b { toArray := arr, size_toArray := ⋯ }
-- Mathlib/Algebra/MvPolynomial/Monad.lean
theorem vars_bind₁ [DecidableEq τ] (f : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) :
    (bind₁ f φ).vars ⊆ φ.vars.biUnion fun i => (f i).vars

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq τ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ (φ.support.biUnion fun i => ((bind₁ f) ((monomial i) (coeff i φ))).vars) =
    φ.support.biUnion fun d => (C (coeff d φ) * ∏ i ∈ d.support, f i ^ d i).vars

Tactic:
simp only [bind₁_monomial]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem C_surjective {R : Type*} [CommSemiring R] (σ : Type*) [IsEmpty σ] :
    Function.Surjective (C : R → MvPolynomial σ R)

Proof state:
R : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : IsEmpty σ
⊢ Surjective ⇑C

Tactic:
refine fun p => ⟨p.toFun 0, Finsupp.ext fun a => ?_⟩

Result:
R : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : IsEmpty σ
p : MvPolynomial σ R
a : σ →₀ ℕ
⊢ (C (p.toFun 0)) a = p a

Proof state:
R : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : IsEmpty σ
p : MvPolynomial σ R
a : σ →₀ ℕ
⊢ p.toFun 0 = p 0

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : IsEmpty σ
p : MvPolynomial σ R
a : σ →₀ ℕ
⊢ (C (p.toFun 0)) a = p a

Tactic:
simp only [C_apply, ← single_eq_monomial, (Finsupp.ext isEmptyElim (α := σ) : a = 0),
  single_eq_same]

Result:
R : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : IsEmpty σ
p : MvPolynomial σ R
a : σ →₀ ℕ
⊢ p.toFun 0 = p 0
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem IsNormal.apply_of_isLimit {f : Ordinal.{u} → Ordinal.{v}} (H : IsNormal f) {o : Ordinal}
    (ho : IsLimit o) : f o = ⨆ a : Iio o, f a

Proof state:
f : Ordinal.{u} → Ordinal.{v}
H : IsNormal f
o : Ordinal.{u}
ho : o.IsLimit
⊢ f o = ⨆ a, f ↑a

Tactic:
have : Nonempty (Iio o) := ⟨0, ho.pos⟩

Result:
f : Ordinal.{u} → Ordinal.{v}
H : IsNormal f
o : Ordinal.{u}
ho : o.IsLimit
this : Nonempty ↑(Iio o)
⊢ f o = ⨆ a, f ↑a

Proof state:
f : Ordinal.{u} → Ordinal.{v}
H : IsNormal f
o : Ordinal.{u}
ho : o.IsLimit
this : Nonempty ↑(Iio o)
⊢ f o = ⨆ a, f ↑a

Tactic:
rw [← H.map_iSup, ho.iSup_Iio]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findSome?_append {l₁ l₂ : Array α} : (l₁ ++ l₂).findSome? f = (l₁.findSome? f).or (l₂.findSome? f)

Proof state:
case mk
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
l₂ : Array α
toList✝ : List α
⊢ findSome? f ({ toList := toList✝ } ++ l₂) = (findSome? f { toList := toList✝ }).or (findSome? f l₂)

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
toList✝¹ toList✝ : List α
⊢ findSome? f ({ toList := toList✝¹ } ++ { toList := toList✝ }) =
    (findSome? f { toList := toList✝¹ }).or (findSome? f { toList := toList✝ })

Proof state:
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
l₁ l₂ : Array α
⊢ findSome? f (l₁ ++ l₂) = (findSome? f l₁).or (findSome? f l₂)

Tactic:
cases l₁

Result:
case mk
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
l₂ : Array α
toList✝ : List α
⊢ findSome? f ({ toList := toList✝ } ++ l₂) = (findSome? f { toList := toList✝ }).or (findSome? f l₂)

Proof state:
case mk.mk
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
toList✝¹ toList✝ : List α
⊢ findSome? f ({ toList := toList✝¹ } ++ { toList := toList✝ }) =
    (findSome? f { toList := toList✝¹ }).or (findSome? f { toList := toList✝ })

Tactic:
simp [List.findSome?_append]

Result:
no goals
-- Mathlib/Algebra/Ring/NegOnePow.lean
@[simp]
lemma negOnePow_neg (n : ℤ) : (-n).negOnePow = n.negOnePow

Proof state:
n : ℤ
⊢ (-n).negOnePow = n.negOnePow

Tactic:
dsimp [negOnePow]

Result:
n : ℤ
⊢ (-1) ^ (-n) = (-1) ^ n

Proof state:
n : ℤ
⊢ (-1) ^ (-n) = (-1) ^ n

Tactic:
simp only [zpow_neg, ← inv_zpow, inv_neg, inv_one]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem continuous_edist : Continuous fun p : α × α => edist p.1 p.2

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
⊢ 2 ≠ ⊤

Tactic:
decide

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
⊢ ∀ (x y : α × α), edist x.1 x.2 ≤ edist y.1 y.2 + 2 * edist x y

Tactic:
rintro ⟨x, y⟩ ⟨x', y'⟩

Result:
case mk.mk
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist (x, y).1 (x, y).2 ≤ edist (x', y').1 (x', y').2 + 2 * edist (x, y) (x', y')

Proof state:
case mk.mk
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist (x, y).1 (x, y).2 ≤ edist (x', y').1 (x', y').2 + 2 * edist (x, y) (x', y')

Tactic:
calc
  edist x y ≤ edist x x' + edist x' y' + edist y' y := edist_triangle4 _ _ _ _
  _ = edist x' y' + (edist x x' + edist y y') := by simp only [edist_comm]; ac_rfl
  _ ≤ edist x' y' + (edist (x, y) (x', y') + edist (x, y) (x', y')) :=
    (add_le_add_left (add_le_add (le_max_left _ _) (le_max_right _ _)) _)
  _ = edist x' y' + 2 * edist (x, y) (x', y') := by rw [← mul_two, mul_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist x x' + edist x' y' + edist y y' = edist x' y' + (edist x x' + edist y y')

Tactic:
ac_rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist x x' + edist x' y' + edist y' y = edist x' y' + (edist x x' + edist y y')

Tactic:
simp only [edist_comm]

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist x x' + edist x' y' + edist y y' = edist x' y' + (edist x x' + edist y y')

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist x' y' + (edist (x, y) (x', y') + edist (x, y) (x', y')) = edist x' y' + 2 * edist (x, y) (x', y')

Tactic:
rw [← mul_two, mul_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
⊢ Continuous fun p => edist p.1 p.2

Tactic:
apply continuous_of_le_add_edist 2 (by decide)

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
⊢ ∀ (x y : α × α), edist x.1 x.2 ≤ edist y.1 y.2 + 2 * edist x y
-- Mathlib/Order/SupClosed.lean
@[simp] lemma latticeClosure_prod (s : Set α) (t : Set β) :
    latticeClosure (s ×ˢ t) = latticeClosure s ×ˢ latticeClosure t

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : DistribLattice α
inst✝ : DistribLattice β
s : Set α
t : Set β
⊢ supClosure (infClosure (s ×ˢ t)) = supClosure (infClosure s) ×ˢ supClosure (infClosure t)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : DistribLattice α
inst✝ : DistribLattice β
s : Set α
t : Set β
⊢ latticeClosure (s ×ˢ t) = latticeClosure s ×ˢ latticeClosure t

Tactic:
simp_rw [← supClosure_infClosure]

Result:
α : Type u_3
β : Type u_4
inst✝¹ : DistribLattice α
inst✝ : DistribLattice β
s : Set α
t : Set β
⊢ supClosure (infClosure (s ×ˢ t)) = supClosure (infClosure s) ×ˢ supClosure (infClosure t)
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem norm_comp_le_of_le {g : NormedAddGroupHom V₂ V₃} {C₁ C₂ : ℝ} (hg : ‖g‖ ≤ C₂)
    (hf : ‖f‖ ≤ C₁) : ‖g.comp f‖ ≤ C₂ * C₁ :=
  le_trans (norm_comp_le g f) <| by gcongr; exact le_trans (norm_nonneg _) hg

Proof state:
case b0
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
C₁ C₂ : ℝ
hg : ‖g‖ ≤ C₂
hf : ‖f‖ ≤ C₁
⊢ 0 ≤ C₂

Tactic:
exact le_trans (norm_nonneg _) hg

Result:
no goals

Proof state:
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
C₁ C₂ : ℝ
hg : ‖g‖ ≤ C₂
hf : ‖f‖ ≤ C₁
⊢ ‖g‖ * ‖f‖ ≤ C₂ * C₁

Tactic:
gcongr

Result:
case b0
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
C₁ C₂ : ℝ
hg : ‖g‖ ≤ C₂
hf : ‖f‖ ≤ C₁
⊢ 0 ≤ C₂
-- Mathlib/Order/WithBot.lean
lemma WithBot.le_toDual_iff {x : WithTop αᵒᵈ} {y : WithBot α} :
    x ≤ WithBot.toDual y ↔ y ≤ WithTop.ofDual x

Proof state:
α : Type u_1
inst✝ : LE α
x : WithTop αᵒᵈ
y : WithBot α
⊢ x ≤ WithBot.toDual y ↔ y ≤ WithTop.ofDual x

Tactic:
cases x <;> cases y <;> simp [le_toDual]

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem Filter.comap_cocompact_le {f : X → Y} (hf : Continuous f) :
    (Filter.cocompact Y).comap f ≤ Filter.cocompact X

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
⊢ comap f (cocompact Y) ≤ cocompact X

Tactic:
rw [(Filter.hasBasis_cocompact.comap f).le_basis_iff Filter.hasBasis_cocompact]

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
⊢ ∀ (i' : Set X), IsCompact i' → ∃ i, IsCompact i ∧ f ⁻¹' iᶜ ⊆ i'ᶜ

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
t : Set X
ht : IsCompact t
⊢ ∃ i, IsCompact i ∧ f ⁻¹' iᶜ ⊆ tᶜ

Tactic:
refine ⟨f '' t, ht.image hf, ?_⟩

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
t : Set X
ht : IsCompact t
⊢ f ⁻¹' (f '' t)ᶜ ⊆ tᶜ

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
⊢ ∀ (i' : Set X), IsCompact i' → ∃ i, IsCompact i ∧ f ⁻¹' iᶜ ⊆ i'ᶜ

Tactic:
intro t ht

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
t : Set X
ht : IsCompact t
⊢ ∃ i, IsCompact i ∧ f ⁻¹' iᶜ ⊆ tᶜ

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
t : Set X
ht : IsCompact t
⊢ f ⁻¹' (f '' t)ᶜ ⊆ tᶜ

Tactic:
simpa using t.subset_preimage_image f

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem digits_ofDigits (b : ℕ) (h : 1 < b) (L : List ℕ) (w₁ : ∀ l ∈ L, l < b)
    (w₂ : ∀ h : L ≠ [], L.getLast h ≠ 0) : digits b (ofDigits b L) = L

Proof state:
case cons
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : (d :: L).getLast ⋯ ≠ 0
⊢ d :: b.digits (ofDigits b L) = d :: L

Tactic:
rw [ih]

Result:
case cons.w₁
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : (d :: L).getLast ⋯ ≠ 0
⊢ ∀ l ∈ L, l < b

case cons.w₂
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : (d :: L).getLast ⋯ ≠ 0
⊢ ∀ (h : L ≠ []), L.getLast h ≠ 0

Proof state:
case pos
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : (d :: L).getLast ⋯ ≠ 0
h' : L = []
⊢ d ≠ 0 ∨ ofDigits b L ≠ 0

Tactic:
rcases h' with rfl

Result:
case pos
b : ℕ
h : 1 < b
d : ℕ
ih : (∀ l ∈ [], l < b) → (∀ (h : [] ≠ []), [].getLast h ≠ 0) → b.digits (ofDigits b []) = []
w₁ : ∀ l ∈ [d], l < b
w₂ : [d].getLast ⋯ ≠ 0
⊢ d ≠ 0 ∨ ofDigits b [] ≠ 0

Proof state:
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : ∀ (h : d :: L ≠ []), (d :: L).getLast h ≠ 0
⊢ d :: L ≠ []

Tactic:
simp

Result:
no goals

Proof state:
case cons
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : ∀ (h : d :: L ≠ []), (d :: L).getLast h ≠ 0
⊢ b.digits (d + b * ofDigits b L) = d :: L

Tactic:
replace w₂ := w₂ (by simp)

Result:
case cons
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : (d :: L).getLast ⋯ ≠ 0
⊢ b.digits (d + b * ofDigits b L) = d :: L

Proof state:
case cons
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : ∀ (h : d :: L ≠ []), (d :: L).getLast h ≠ 0
⊢ b.digits (ofDigits b (d :: L)) = d :: L

Tactic:
dsimp [ofDigits]

Result:
case cons
b : ℕ
h : 1 < b
d : ℕ
L : List ℕ
ih : (∀ l ∈ L, l < b) → (∀ (h : L ≠ []), L.getLast h ≠ 0) → b.digits (ofDigits b L) = L
w₁ : ∀ l ∈ d :: L, l < b
w₂ : ∀ (h : d :: L ≠ []), (d :: L).getLast h ≠ 0
⊢ b.digits (d + b * ofDigits b L) = d :: L

Proof state:
case pos
b : ℕ
h : 1 < b
d : ℕ
ih : (∀ l ∈ [], l < b) → (∀ (h : [] ≠ []), [].getLast h ≠ 0) → b.digits (ofDigits b []) = []
w₁ : ∀ l ∈ [d], l < b
w₂ : [d].getLast ⋯ ≠ 0
⊢ d ≠ 0 ∨ ofDigits b [] ≠ 0

Tactic:
left

Result:
case pos.h
b : ℕ
h : 1 < b
d : ℕ
ih : (∀ l ∈ [], l < b) → (∀ (h : [] ≠ []), [].getLast h ≠ 0) → b.digits (ofDigits b []) = []
w₁ : ∀ l ∈ [d], l < b
w₂ : [d].getLast ⋯ ≠ 0
⊢ d ≠ 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Bootstrap.lean
theorem append_assoc (as bs cs : Array α) : as ++ bs ++ cs = as ++ (bs ++ cs)

Proof state:
α : Type u_1
as bs cs : Array α
⊢ as ++ bs ++ cs = as ++ (bs ++ cs)

Tactic:
apply ext'

Result:
case h
α : Type u_1
as bs cs : Array α
⊢ (as ++ bs ++ cs).toList = (as ++ (bs ++ cs)).toList

Proof state:
case h
α : Type u_1
as bs cs : Array α
⊢ (as ++ bs ++ cs).toList = (as ++ (bs ++ cs)).toList

Tactic:
simp only [toList_append, List.append_assoc]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Restrict.lean
theorem isPullback_morphismRestrict {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) :
    IsPullback (f ∣_ U) (f ⁻¹ᵁ U).ι U.ι f

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (pullbackRestrictIsoRestrict (𝟙 X ≫ f) U).inv ≫ pullback.fst f (Y.ofRestrict ⋯) = ((𝟙 X ≫ f) ⁻¹ᵁ U).ι ≫ 𝟙 X

Tactic:
erw [pullbackRestrictIsoRestrict_inv_fst]

Result:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ ((𝟙 X ≫ f) ⁻¹ᵁ U).ι = ((𝟙 X ≫ f) ⁻¹ᵁ U).ι ≫ 𝟙 X

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ IsPullback ((pullbackRestrictIsoRestrict f U).inv ≫ pullback.snd f U.ι) (f ⁻¹ᵁ U).ι U.ι f

Tactic:
rw [← Category.id_comp f]

Result:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ IsPullback ((pullbackRestrictIsoRestrict (𝟙 X ≫ f) U).inv ≫ pullback.snd (𝟙 X ≫ f) U.ι) ((𝟙 X ≫ f) ⁻¹ᵁ U).ι U.ι
    (𝟙 X ≫ f)

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ ((𝟙 X ≫ f) ⁻¹ᵁ U).ι = ((𝟙 X ≫ f) ⁻¹ᵁ U).ι ≫ 𝟙 X

Tactic:
rw [Category.comp_id]

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ IsPullback ((pullbackRestrictIsoRestrict (𝟙 X ≫ f) U).inv ≫ pullback.snd (𝟙 X ≫ f) U.ι) ((𝟙 X ≫ f) ⁻¹ᵁ U).ι U.ι
    (𝟙 X ≫ f)

Tactic:
refine
  (IsPullback.of_horiz_isIso ⟨?_⟩).paste_horiz
    (IsPullback.of_hasPullback f (Y.ofRestrict U.isOpenEmbedding)).flip

Result:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (pullbackRestrictIsoRestrict (𝟙 X ≫ f) U).inv ≫ pullback.fst f (Y.ofRestrict ⋯) = ((𝟙 X ≫ f) ⁻¹ᵁ U).ι ≫ 𝟙 X

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ IsPullback (f ∣_ U) (f ⁻¹ᵁ U).ι U.ι f

Tactic:
delta morphismRestrict

Result:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ IsPullback ((pullbackRestrictIsoRestrict f U).inv ≫ pullback.snd f U.ι) (f ⁻¹ᵁ U).ι U.ι f