harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Digits.lean
/-- The core implementation of `Nat.repr` returns a String with length less than or equal to the
number of digits in the decimal number (represented by `e`). For example, the decimal string
representation of any number less than 1000 (10 ^ 3) has a length less than or equal to 3. -/
lemma repr_length (n e : Nat) : 0 < e → n < 10 ^ e → (Nat.repr n).length <= e

Proof state:
e n : ℕ
e0 : 0 < e
he : n + 1 < 10 ^ e
hterm : ¬n.succ / 10 = 0
⊢ (toDigitsCore 10 (n + 1 + 1) (n + 1) []).length ≤ e

Tactic:
exact toDigitsCore_length 10 (by decide) (Nat.succ n + 1) (Nat.succ n) e he e0

Result:
no goals

Proof state:
e n : ℕ
e0 : 0 < e
he : n + 1 < 10 ^ e
hterm : n.succ / 10 = 0
⊢ (toDigitsCore 10 (n + 1 + 1) (n + 1) []).length ≤ e

Tactic:
simp only [hterm, Nat.toDigitsCore]

Result:
e n : ℕ
e0 : 0 < e
he : n + 1 < 10 ^ e
hterm : n.succ / 10 = 0
⊢ (if True then [((n + 1) % 10).digitChar]
      else
        if True then [(0 % 10).digitChar, ((n + 1) % 10).digitChar]
        else toDigitsCore 10 n (0 / 10) [(0 % 10).digitChar, ((n + 1) % 10).digitChar]).length ≤
    e

Proof state:
case succ
e n : ℕ
⊢ 0 < e → n + 1 < 10 ^ e → (n + 1).repr.length ≤ e

Tactic:
intro e0 he

Result:
case succ
e n : ℕ
e0 : 0 < e
he : n + 1 < 10 ^ e
⊢ (n + 1).repr.length ≤ e

Proof state:
case succ
e n : ℕ
e0 : 0 < e
he : n + 1 < 10 ^ e
⊢ (n + 1).repr.length ≤ e

Tactic:
simp only [Nat.repr, Nat.toDigits, String.length, List.asString]

Result:
case succ
e n : ℕ
e0 : 0 < e
he : n + 1 < 10 ^ e
⊢ (toDigitsCore 10 (n + 1 + 1) (n + 1) []).length ≤ e

Proof state:
n e : ℕ
⊢ 0 < e → n < 10 ^ e → n.repr.length ≤ e

Tactic:
cases n with
  (intro e0 he; simp only [Nat.repr, Nat.toDigits, String.length, List.asString])
| zero => assumption
| succ n =>
  if hterm : n.succ / 10 = 0 then
    simp only [hterm, Nat.toDigitsCore]; assumption
  else
    exact toDigitsCore_length 10 (by decide) (Nat.succ n + 1) (Nat.succ n) e he e0

Result:
no goals

Proof state:
e n : ℕ
e0 : 0 < e
he : n + 1 < 10 ^ e
hterm : n.succ / 10 = 0
⊢ (if True then [((n + 1) % 10).digitChar]
      else
        if True then [(0 % 10).digitChar, ((n + 1) % 10).digitChar]
        else toDigitsCore 10 n (0 / 10) [(0 % 10).digitChar, ((n + 1) % 10).digitChar]).length ≤
    e

Tactic:
assumption

Result:
no goals

Proof state:
e n : ℕ
e0 : 0 < e
he : n + 1 < 10 ^ e
hterm : ¬n.succ / 10 = 0
⊢ 2 ≤ 10

Tactic:
decide

Result:
no goals

Proof state:
case succ
e n : ℕ
e0 : 0 < e
he : n + 1 < 10 ^ e
⊢ (toDigitsCore 10 (n + 1 + 1) (n + 1) []).length ≤ e

Tactic:
if hterm : n.succ / 10 = 0 then
  simp only [hterm, Nat.toDigitsCore]; assumption
else
  exact toDigitsCore_length 10 (by decide) (Nat.succ n + 1) (Nat.succ n) e he e0

Result:
no goals

Proof state:
case zero
e : ℕ
e0 : 0 < e
he : 0 < 10 ^ e
⊢ (toDigitsCore 10 (0 + 1) 0 []).length ≤ e

Tactic:
assumption

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
theorem comp (hg : IsClosedMap g) (hf : IsClosedMap f) : IsClosedMap (g ∘ f)

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsClosedMap g
hf : IsClosedMap f
s : Set X
hs : IsClosed s
⊢ IsClosed (g ∘ f '' s)

Tactic:
rw [image_comp]

Result:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsClosedMap g
hf : IsClosedMap f
s : Set X
hs : IsClosed s
⊢ IsClosed (g '' (f '' s))

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsClosedMap g
hf : IsClosedMap f
⊢ IsClosedMap (g ∘ f)

Tactic:
intro s hs

Result:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsClosedMap g
hf : IsClosedMap f
s : Set X
hs : IsClosed s
⊢ IsClosed (g ∘ f '' s)

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsClosedMap g
hf : IsClosedMap f
s : Set X
hs : IsClosed s
⊢ IsClosed (g '' (f '' s))

Tactic:
exact hg _ (hf _ hs)

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
lemma ceil_le_mul (hb : 1 < b) (hba : ⌈(b - 1)⁻¹⌉₊ / b ≤ a) : ⌈a⌉₊ ≤ b * a

Proof state:
case inl
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
b : α
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉₊ / b ≤ ↑⌈(b - 1)⁻¹⌉₊ / b
⊢ ↑⌈↑⌈(b - 1)⁻¹⌉₊ / b⌉₊ ≤ b * (↑⌈(b - 1)⁻¹⌉₊ / b)

Tactic:
rw [mul_div_cancel₀, cast_le, ceil_le]

Result:
case inl
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
b : α
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉₊ / b ≤ ↑⌈(b - 1)⁻¹⌉₊ / b
⊢ ↑⌈(b - 1)⁻¹⌉₊ / b ≤ ↑⌈(b - 1)⁻¹⌉₊

case inl.hb
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
b : α
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉₊ / b ≤ ↑⌈(b - 1)⁻¹⌉₊ / b
⊢ b ≠ 0

Proof state:
case inl
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
b : α
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉₊ / b ≤ ↑⌈(b - 1)⁻¹⌉₊ / b
⊢ ↑⌈(b - 1)⁻¹⌉₊ / b ≤ ↑⌈(b - 1)⁻¹⌉₊

Tactic:
exact _root_.div_le_self (by positivity) hb.le

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
b : α
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉₊ / b ≤ ↑⌈(b - 1)⁻¹⌉₊ / b
⊢ 0 ≤ ↑⌈(b - 1)⁻¹⌉₊

Tactic:
positivity

Result:
no goals

Proof state:
case inl.hb
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
b : α
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉₊ / b ≤ ↑⌈(b - 1)⁻¹⌉₊ / b
⊢ b ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
case inr
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb : 1 < b
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b ≤ a
hba : ↑⌈(b - 1)⁻¹⌉₊ / b < a
⊢ ↑⌈a⌉₊ ≤ b * a

Tactic:
exact (ceil_lt_mul hb hba).le

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉₊ / b ≤ a
⊢ ↑⌈a⌉₊ ≤ b * a

Tactic:
obtain rfl | hba := hba.eq_or_lt

Result:
case inl
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
b : α
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉₊ / b ≤ ↑⌈(b - 1)⁻¹⌉₊ / b
⊢ ↑⌈↑⌈(b - 1)⁻¹⌉₊ / b⌉₊ ≤ b * (↑⌈(b - 1)⁻¹⌉₊ / b)

case inr
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a b : α
hb : 1 < b
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b ≤ a
hba : ↑⌈(b - 1)⁻¹⌉₊ / b < a
⊢ ↑⌈a⌉₊ ≤ b * a
-- Mathlib/Order/WithBot.lean
@[simp] protected lemma not_lt_bot (a : WithBot α) : ¬a < ⊥

Proof state:
α : Type u_1
inst✝ : LT α
a : WithBot α
⊢ ¬a < ⊥

Tactic:
simp [lt_def]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem inv_lt_iff_one_lt_mul' : a⁻¹ < b ↔ 1 < a * b :=
  (mul_lt_mul_iff_left a).symm.trans <| by rw [mul_inv_cancel]

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b : α
⊢ a * a⁻¹ < a * b ↔ 1 < a * b

Tactic:
rw [mul_inv_cancel]

Result:
no goals
-- Mathlib/Data/Nat/Bitwise.lean
@[simp]
lemma bitwise_zero_right (n : Nat) : bitwise f n 0 = if f true false then n else 0

Proof state:
f : Bool → Bool → Bool
n : ℕ
⊢ (if n = 0 then if f false true = true then 0 else 0
    else
      if 0 = 0 then if f true false = true then n else 0
      else
        let n' := n / 2;
        let m' := 0 / 2;
        let b₁ := n % 2 = 1;
        let b₂ := 0 % 2 = 1;
        let r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    if f true false = true then n else 0

Tactic:
simp only [ite_self, decide_false, Nat.zero_div, ite_true, ite_eq_right_iff]

Result:
f : Bool → Bool → Bool
n : ℕ
⊢ n = 0 → 0 = if f true false = true then n else 0

Proof state:
case refl
f : Bool → Bool → Bool
⊢ 0 = if f true false = true then 0 else 0

Tactic:
split_ifs <;> rfl

Result:
no goals

Proof state:
f : Bool → Bool → Bool
n : ℕ
⊢ bitwise f n 0 = if f true false = true then n else 0

Tactic:
unfold bitwise

Result:
f : Bool → Bool → Bool
n : ℕ
⊢ (if n = 0 then if f false true = true then 0 else 0
    else
      if 0 = 0 then if f true false = true then n else 0
      else
        let n' := n / 2;
        let m' := 0 / 2;
        let b₁ := n % 2 = 1;
        let b₂ := 0 % 2 = 1;
        let r := bitwise f n' m';
        if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) =
    if f true false = true then n else 0

Proof state:
f : Bool → Bool → Bool
n : ℕ
⊢ n = 0 → 0 = if f true false = true then n else 0

Tactic:
rintro ⟨⟩

Result:
case refl
f : Bool → Bool → Bool
⊢ 0 = if f true false = true then 0 else 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem mem_set (l : List α) (n : Nat) (h : n < l.length) (a : α) :
    a ∈ l.set n a

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

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : List α
n : Nat
h : n < l.length
a : α
⊢ a ∈ l.set n a

Tactic:
simp [mem_iff_getElem]

Result:
α : Type u_1
l : List α
n : Nat
h : n < l.length
a : α
⊢ ∃ i h, (l.set n a)[i] = a

Proof state:
α : Type u_1
l : List α
n : Nat
h : n < l.length
a : α
⊢ n < l.length

Tactic:
simpa using h

Result:
no goals

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

Tactic:
exact ⟨n, (by simpa using h), by simp⟩

Result:
no goals
-- Mathlib/Algebra/Group/Even.lean
@[to_additive (attr := simp) Even.zsmul_left]
lemma Even.isSquare_zpow [Group α] {n : ℤ} : Even n → ∀ a : α, IsSquare (a ^ n)

Proof state:
α : Type u_2
inst✝ : Group α
n : ℤ
⊢ Even n → ∀ (a : α), IsSquare (a ^ n)

Tactic:
rintro ⟨m, rfl⟩ a

Result:
case intro
α : Type u_2
inst✝ : Group α
m : ℤ
a : α
⊢ IsSquare (a ^ (m + m))

Proof state:
case intro
α : Type u_2
inst✝ : Group α
m : ℤ
a : α
⊢ IsSquare (a ^ (m + m))

Tactic:
exact ⟨a ^ m, zpow_add _ _ _⟩

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
lemma ringEquivCongr_trans {a b c : ℕ} (hab : a = b) (hbc : b = c) :
    (ringEquivCongr hab).trans (ringEquivCongr hbc) = ringEquivCongr (hab.trans hbc)

Proof state:
a b c : ℕ
hab : a = b
hbc : b = c
⊢ (ringEquivCongr hab).trans (ringEquivCongr hbc) = ringEquivCongr ⋯

Tactic:
subst hab hbc

Result:
a : ℕ
⊢ (ringEquivCongr ⋯).trans (ringEquivCongr ⋯) = ringEquivCongr ⋯

Proof state:
a : ℕ
⊢ (ringEquivCongr ⋯).trans (ringEquivCongr ⋯) = ringEquivCongr ⋯

Tactic:
cases a <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/BinomialHeap/Lemmas.lean
theorem Heap.findMin_val : ((s : Heap α).findMin le k res).val = s.headD le res.val :=
  match s with
  | .nil => rfl
  | .cons r a c s => by rw [findMin, headD]; split <;> apply findMin_val

Proof state:
α : Type u_1
s✝ : Heap α
le : α → α → Bool
k : Heap α → Heap α
res : FindMin α
r : Nat
a : α
c : HeapNode α
s : Heap α
⊢ (findMin le k (cons r a c s) res).val = headD le res.val (cons r a c s)

Tactic:
rw [findMin, headD]

Result:
α : Type u_1
s✝ : Heap α
le : α → α → Bool
k : Heap α → Heap α
res : FindMin α
r : Nat
a : α
c : HeapNode α
s : Heap α
⊢ (findMin le (k ∘ cons r a c) s
        (if le res.val a = true then res else { before := k, val := a, node := c, next := s })).val =
    headD le (if le res.val a = true then res.val else a) s

Proof state:
α : Type u_1
s✝ : Heap α
le : α → α → Bool
k : Heap α → Heap α
res : FindMin α
r : Nat
a : α
c : HeapNode α
s : Heap α
⊢ (findMin le (k ∘ cons r a c) s
        (if le res.val a = true then res else { before := k, val := a, node := c, next := s })).val =
    headD le (if le res.val a = true then res.val else a) s

Tactic:
split <;> apply findMin_val

Result:
no goals
-- Mathlib/CategoryTheory/Dialectica/Basic.lean
theorem comp_le_lemma {X Y Z : Dial C} (F : Dial.Hom X Y) (G : Dial.Hom Y Z) :
    (Subobject.pullback π(π₁, π(π₁, prod.map F.f (𝟙 _) ≫ G.F) ≫ F.F)).obj X.rel ≤
    (Subobject.pullback (prod.map (F.f ≫ G.f) (𝟙 Z.tgt))).obj Z.rel

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y Z : Dial C
F : X.Hom Y
G : Y.Hom Z
⊢ (Subobject.pullback π(π₁, π(π₁, prod.map F.f (𝟙 Z.tgt) ≫ G.F) ≫ F.F)).obj X.rel ≤
    (Subobject.pullback (prod.map (F.f ≫ G.f) (𝟙 Z.tgt))).obj Z.rel

Tactic:
refine
  le_trans ?_ <| ((Subobject.pullback (π(π₁, prod.map F.f (𝟙 _) ≫ G.F))).monotone F.le).trans <|
  le_trans ?_ <| ((Subobject.pullback (prod.map F.f (𝟙 Z.tgt))).monotone G.le).trans ?_
  <;> simp [← Subobject.pullback_comp]

Result:
no goals
-- Mathlib/NumberTheory/Bernoulli.lean
theorem bernoulli_one : bernoulli 1 = -1 / 2

Proof state:
⊢ bernoulli 1 = -1 / 2

Tactic:
norm_num [bernoulli]

Result:
no goals
-- Mathlib/Analysis/Polynomial/CauchyBound.lean
@[simp]
lemma cauchyBound_C (x : K) : cauchyBound (C x) = 1

Proof state:
K : Type u_1
inst✝ : NormedDivisionRing K
x : K
⊢ (C x).cauchyBound = 1

Tactic:
simp [cauchyBound]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem flatten_eq_nil_iff {L : List (List α)} : L.flatten = [] ↔ ∀ l ∈ L, l = []

Proof state:
α : Type u_1
L : List (List α)
⊢ L.flatten = [] ↔ ∀ (l : List α), l ∈ L → l = []

Tactic:
induction L <;> simp_all

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
theorem X_dvd_sub_C : X ∣ p - C (p.coeff 0)

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ X ∣ p - C (p.coeff 0)

Tactic:
simp [X_dvd_iff, coeff_C]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.sdiv_udiv (x y : BitVec w) :
    x.sdiv y =
      bif x.getLsbD (w - 1) then
        bif y.getLsbD (w - 1) then
          (-x) / (-y)
        else
          -((-x) / y)
      else
        bif y.getLsbD (w - 1) then
          -(x / (-y))
        else
          x / y

Proof state:
w : Nat
x y : BitVec w
⊢ (match x.msb, y.msb with
    | false, false => x.udiv y
    | false, true => -x.udiv (-y)
    | true, false => -(-x).udiv y
    | true, true => (-x).udiv (-y)) =
    bif x.msb then bif y.msb then -x / -y else -(-x / y) else bif y.msb then -(x / -y) else x / y

Tactic:
cases x.msb <;> cases y.msb <;> simp

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
⊢ x.sdiv y =
    bif x.getLsbD (w - 1) then bif y.getLsbD (w - 1) then -x / -y else -(-x / y)
    else bif y.getLsbD (w - 1) then -(x / -y) else x / y

Tactic:
rw [BitVec.sdiv_eq, ← BitVec.msb_eq_getLsbD_last, ← BitVec.msb_eq_getLsbD_last]

Result:
w : Nat
x y : BitVec w
⊢ (match x.msb, y.msb with
    | false, false => x.udiv y
    | false, true => -x.udiv (-y)
    | true, false => -(-x).udiv y
    | true, true => (-x).udiv (-y)) =
    bif x.msb then bif y.msb then -x / -y else -(-x / y) else bif y.msb then -(x / -y) else x / y
-- Mathlib/CategoryTheory/Shift/Adjunction.lean
/-- Given an adjunction `adj : F ⊣ G`, `a` in `A` and commutation isomorphisms
`e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a` and
`e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a`, compatibility of `e₁` and `e₂` with the
unit of the adjunction `adj` implies compatibility with the counit of `adj`.
-/
lemma compatibilityCounit_of_compatibilityUnit (h : CompatibilityUnit adj e₁ e₂) :
    CompatibilityCounit adj e₁ e₂

Proof state:
case a
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
eq :
  (shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)) ≫ G.map (e₁.inv.app (G.obj Y)) =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y))
⊢ adj.unit.app (G.obj ((shiftFunctor D a).obj Y)) ≫ G.map (adj.counit.app ((shiftFunctor D a).obj Y)) =
    e₂.hom.app Y ≫
      ((shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)) ≫ G.map (e₁.inv.app (G.obj Y))) ≫
        G.map (e₁.hom.app (G.obj Y) ≫ (shiftFunctor D a).map (adj.counit.app Y))

Tactic:
simp only [assoc, ← Functor.map_comp, Iso.inv_hom_id_app_assoc]

Result:
case a
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
eq :
  (shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)) ≫ G.map (e₁.inv.app (G.obj Y)) =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y))
⊢ adj.unit.app (G.obj ((shiftFunctor D a).obj Y)) ≫ G.map (adj.counit.app ((shiftFunctor D a).obj Y)) =
    e₂.hom.app Y ≫
      (shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫
        e₂.inv.app (F.obj (G.obj Y)) ≫ G.map ((shiftFunctor D a).map (adj.counit.app Y))

Proof state:
case a
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
eq :
  (shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)) ≫ G.map (e₁.inv.app (G.obj Y)) =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y))
⊢ adj.unit.app (G.obj ((shiftFunctor D a).obj Y)) ≫ G.map (adj.counit.app ((shiftFunctor D a).obj Y)) =
    e₂.hom.app Y ≫
      (shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫ (shiftFunctor C a).map (G.map (adj.counit.app Y)) ≫ e₂.inv.app Y

Tactic:
simp only [right_triangle_components, ← Functor.map_comp_assoc, Functor.map_id, id_comp,
  Iso.hom_inv_id_app, Functor.comp_obj]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToFun_smul_left' (hT : DominatedFinMeasAdditive μ T C)
    (hT' : DominatedFinMeasAdditive μ T' C') (c : ℝ)
    (h_smul : ∀ s, MeasurableSet s → μ s < ∞ → T' s = c • T s) (f : α → E) :
    setToFun μ T' hT' f = c • setToFun μ T hT f

Proof state:
case neg
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s
f : α → E
hf : ¬Integrable f μ
⊢ setToFun μ T' hT' f = c • setToFun μ T hT f

Tactic:
simp_rw [setToFun_undef _ hf, smul_zero]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s
f : α → E
⊢ setToFun μ T' hT' f = c • setToFun μ T hT f

Tactic:
by_cases hf : Integrable f μ

Result:
case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s
f : α → E
hf : Integrable f μ
⊢ setToFun μ T' hT' f = c • setToFun μ T hT f

case neg
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s
f : α → E
hf : ¬Integrable f μ
⊢ setToFun μ T' hT' f = c • setToFun μ T hT f

Proof state:
case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s
f : α → E
hf : Integrable f μ
⊢ setToFun μ T' hT' f = c • setToFun μ T hT f

Tactic:
simp_rw [setToFun_eq _ hf, L1.setToL1_smul_left' hT hT' c h_smul]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Verschiebung.lean
theorem verschiebung_injective : Function.Injective (verschiebung : 𝕎 R → 𝕎 R)

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
⊢ ∀ (a : 𝕎 R), verschiebung a = 0 → a = 0

Tactic:
intro w h

Result:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
w : 𝕎 R
h : verschiebung w = 0
⊢ w = 0

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
w : 𝕎 R
h : verschiebung w = 0
⊢ w = 0

Tactic:
ext n

Result:
case h
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
w : 𝕎 R
h : verschiebung w = 0
n : ℕ
⊢ w.coeff n = coeff 0 n

Proof state:
case h
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
w : 𝕎 R
h : verschiebung w = 0
n : ℕ
⊢ w.coeff n = coeff 0 n

Tactic:
rw [← verschiebung_coeff_succ, h]

Result:
case h
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
w : 𝕎 R
h : verschiebung w = 0
n : ℕ
⊢ coeff 0 n.succ = coeff 0 n

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
⊢ Function.Injective ⇑verschiebung

Tactic:
rw [injective_iff_map_eq_zero]

Result:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
⊢ ∀ (a : 𝕎 R), verschiebung a = 0 → a = 0

Proof state:
case h
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
w : 𝕎 R
h : verschiebung w = 0
n : ℕ
⊢ coeff 0 n.succ = coeff 0 n

Tactic:
simp only [zero_coeff]

Result:
no goals
-- Mathlib/RingTheory/Binomial.lean
theorem choose_one_right' (r : R) : choose r 1 = r ^ 1

Proof state:
R : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : BinomialRing R
r : R
⊢ choose r 1 = r ^ 1

Tactic:
rw [choose, Nat.cast_one, sub_add_cancel, multichoose_one_right']

Result:
no goals
-- Mathlib/Topology/MetricSpace/Antilipschitz.lean
theorem comp {Kg : ℝ≥0} {g : β → γ} (hg : AntilipschitzWith Kg g) {Kf : ℝ≥0} {f : α → β}
    (hf : AntilipschitzWith Kf f) : AntilipschitzWith (Kf * Kg) (g ∘ f) := fun x y =>
  calc
    edist x y ≤ Kf * edist (f x) (f y) := hf x y
    _ ≤ Kf * (Kg * edist (g (f x)) (g (f y))) := mul_left_mono (hg _ _)
    _ = _

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
Kg : ℝ≥0
g : β → γ
hg : AntilipschitzWith Kg g
Kf : ℝ≥0
f : α → β
hf : AntilipschitzWith Kf f
x y : α
⊢ ↑Kf * (↑Kg * edist (g (f x)) (g (f y))) = ↑Kf * (↑Kg * edist ((g ∘ f) x) ((g ∘ f) y))

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
Kg : ℝ≥0
g : β → γ
hg : AntilipschitzWith Kg g
Kf : ℝ≥0
f : α → β
hf : AntilipschitzWith Kf f
x y : α
⊢ ↑Kf * (↑Kg * edist (g (f x)) (g (f y))) = ↑(Kf * Kg) * edist ((g ∘ f) x) ((g ∘ f) y)

Tactic:
rw [ENNReal.coe_mul, mul_assoc]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
Kg : ℝ≥0
g : β → γ
hg : AntilipschitzWith Kg g
Kf : ℝ≥0
f : α → β
hf : AntilipschitzWith Kf f
x y : α
⊢ ↑Kf * (↑Kg * edist (g (f x)) (g (f y))) = ↑Kf * (↑Kg * edist ((g ∘ f) x) ((g ∘ f) y))