harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem log_inv (x : ℝ) : log x⁻¹ = -log x

Proof state:
x : ℝ
⊢ log x⁻¹ = -log x

Tactic:
by_cases hx : x = 0

Result:
case pos
x : ℝ
hx : x = 0
⊢ log x⁻¹ = -log x

case neg
x : ℝ
hx : ¬x = 0
⊢ log x⁻¹ = -log x

Proof state:
case neg
x : ℝ
hx : ¬x = 0
⊢ log x⁻¹ = -log x

Tactic:
rw [← exp_eq_exp, exp_log_eq_abs (inv_ne_zero hx), exp_neg, exp_log_eq_abs hx, abs_inv]

Result:
no goals

Proof state:
case pos
x : ℝ
hx : x = 0
⊢ log x⁻¹ = -log x

Tactic:
simp [hx]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey?_insertMany_empty_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
    {l : List (α × β)} {k : α}
    (h : (l.map Prod.fst).contains k = false) :
    (insertMany (empty : Raw₀ α (fun _ => β)) l).1.getKey? k = none

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List (α × β)
k : α
h : (List.map Prod.fst l).contains k = false
⊢ empty.getKey? k = none

Tactic:
apply getKey?_empty

Result:
no goals

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List (α × β)
k : α
h : (List.map Prod.fst l).contains k = false
⊢ (insertMany empty l).val.getKey? k = none

Tactic:
rw [getKey?_insertMany_list_of_contains_eq_false _ Raw.WF.empty₀ h]

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List (α × β)
k : α
h : (List.map Prod.fst l).contains k = false
⊢ empty.getKey? k = none
-- Mathlib/Algebra/Lie/CartanExists.lean
lemma exists_isCartanSubalgebra_engel_of_finrank_le_card (h : finrank K L ≤ #K) :
    ∃ x : L, IsCartanSubalgebra (engel K x)

Proof state:
case a
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
h : ↑(finrank K L) ≤ #K
x : L
hx : IsRegular K x
y✝ : L
hy✝ : y✝ ∈ engel K x
Ex : ↑{x_1 | ∃ z ∈ engel K x, engel K z = x_1} := ⟨engel K x, ⋯⟩
y : L
hy : y ∈ engel K x
hyx : ⟨engel K y, ⋯⟩ ≤ Ex
this : finrank K ↥(engel K x) ≤ finrank K ↥(engel K y)
⊢ (engel K y).toSubmodule = (engel K x).toSubmodule

Tactic:
exact Submodule.eq_of_le_of_finrank_le hyx this

Result:
no goals

Proof state:
case intro
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
h : ↑(finrank K L) ≤ #K
x : L
hx : IsRegular K x
⊢ ∃ x, (engel K x).IsCartanSubalgebra

Tactic:
use x

Result:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
h : ↑(finrank K L) ≤ #K
x : L
hx : IsRegular K x
⊢ (engel K x).IsCartanSubalgebra

Proof state:
case h.h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
h : ↑(finrank K L) ≤ #K
x : L
hx : IsRegular K x
y : L
hy : y ∈ engel K x
⊢ engel K x ≤ engel K y

Tactic:
set Ex : {engel K z | z ∈ engel K x} := ⟨engel K x, x, self_mem_engel _ _, rfl⟩

Result:
case h.h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
h : ↑(finrank K L) ≤ #K
x : L
hx : IsRegular K x
y : L
hy : y ∈ engel K x
Ex : ↑{x_1 | ∃ z ∈ engel K x, engel K z = x_1} := ⟨engel K x, ⋯⟩
⊢ engel K x ≤ engel K y

Proof state:
case h.h.mk.intro.intro
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
h : ↑(finrank K L) ≤ #K
x : L
hx : IsRegular K x
y✝ : L
hy✝ : y✝ ∈ engel K x
Ex : ↑{x_1 | ∃ z ∈ engel K x, engel K z = x_1} := ⟨engel K x, ⋯⟩
y : L
hy : y ∈ engel K x
hyx : ⟨engel K y, ⋯⟩ ≤ Ex
⊢ rank K L ≤ finrank K ↥(engel K y)

Tactic:
apply rank_le_finrank_engel

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/SmoothingSeminorm.lean
theorem isNonarchimedean_smoothingFun (hμ1 : μ 1 ≤ 1) (hna : IsNonarchimedean μ) :
    IsNonarchimedean (smoothingFun μ)

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
mu : ℕ → ℕ := fun n => _root_.mu μ hn n
nu : ℕ → ℕ := fun n => n - mu n
hnu : nu = fun n => n - mu n
hmu_le : ∀ (n : ℕ), mu n ≤ n
hmu_bdd : ∀ (n : ℕ), ↑(mu n) / ↑n ∈ Set.Icc 0 1
hs : Bornology.IsBounded (Set.Icc 0 1)
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n => ↑(mu n) / ↑n) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
⊢ ∀ (b : ℕ), 1 ≤ b → 1 - ↑(mu (ψ b)) / ↑(ψ b) = ↑(nu (ψ b)) / ↑(ψ b)

Tactic:
intro m hm

Result:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
mu : ℕ → ℕ := fun n => _root_.mu μ hn n
nu : ℕ → ℕ := fun n => n - mu n
hnu : nu = fun n => n - mu n
hmu_le : ∀ (n : ℕ), mu n ≤ n
hmu_bdd : ∀ (n : ℕ), ↑(mu n) / ↑n ∈ Set.Icc 0 1
hs : Bornology.IsBounded (Set.Icc 0 1)
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n => ↑(mu n) / ↑n) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
m : ℕ
hm : 1 ≤ m
⊢ 1 - ↑(mu (ψ m)) / ↑(ψ m) = ↑(nu (ψ m)) / ↑(ψ m)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toArray_append {xs : List α} {ys : Array α} :
    xs.toArray ++ ys = (xs ++ ys.toList).toArray

Proof state:
case mk
α : Type u_1
xs ys : List α
⊢ xs.toArray ++ { toList := ys } = (xs ++ { toList := ys }.toList).toArray

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
xs : List α
ys : Array α
⊢ xs.toArray ++ ys = (xs ++ ys.toList).toArray

Tactic:
rcases ys with ⟨ys⟩

Result:
case mk
α : Type u_1
xs ys : List α
⊢ xs.toArray ++ { toList := ys } = (xs ++ { toList := ys }.toList).toArray
-- Mathlib/Topology/Instances/CantorSet.lean
lemma quarters_mem_preCantorSet (n : ℕ) : 1/4 ∈ preCantorSet n ∧ 3/4 ∈ preCantorSet n

Proof state:
case succ.right
n : ℕ
ih : 1 / 4 ∈ preCantorSet n ∧ 3 / 4 ∈ preCantorSet n
⊢ 3 / 4 ∈ preCantorSet (n + 1)

Tactic:
exact Or.inr ⟨1 / 4, ih.1, by norm_num⟩

Result:
no goals

Proof state:
case zero

⊢ 1 / 4 ∈ Set.Icc 0 1 ∧ 3 / 4 ∈ Set.Icc 0 1

Tactic:
refine ⟨⟨ ?_, ?_⟩, ?_, ?_⟩ <;> norm_num

Result:
no goals

Proof state:
n : ℕ
ih : 1 / 4 ∈ preCantorSet n ∧ 3 / 4 ∈ preCantorSet n
⊢ (fun x => (2 + x) / 3) (1 / 4) = 3 / 4

Tactic:
norm_num

Result:
no goals

Proof state:
n : ℕ
ih : 1 / 4 ∈ preCantorSet n ∧ 3 / 4 ∈ preCantorSet n
⊢ (fun x => x / 3) (3 / 4) = 1 / 4

Tactic:
norm_num

Result:
no goals

Proof state:
case succ
n : ℕ
ih : 1 / 4 ∈ preCantorSet n ∧ 3 / 4 ∈ preCantorSet n
⊢ 1 / 4 ∈ preCantorSet (n + 1) ∧ 3 / 4 ∈ preCantorSet (n + 1)

Tactic:
apply And.intro

Result:
case succ.left
n : ℕ
ih : 1 / 4 ∈ preCantorSet n ∧ 3 / 4 ∈ preCantorSet n
⊢ 1 / 4 ∈ preCantorSet (n + 1)

case succ.right
n : ℕ
ih : 1 / 4 ∈ preCantorSet n ∧ 3 / 4 ∈ preCantorSet n
⊢ 3 / 4 ∈ preCantorSet (n + 1)

Proof state:
case succ.left
n : ℕ
ih : 1 / 4 ∈ preCantorSet n ∧ 3 / 4 ∈ preCantorSet n
⊢ 1 / 4 ∈ preCantorSet (n + 1)

Tactic:
exact Or.inl ⟨3 / 4, ih.2, by norm_num⟩

Result:
no goals

Proof state:
case zero

⊢ 1 / 4 ∈ preCantorSet 0 ∧ 3 / 4 ∈ preCantorSet 0

Tactic:
simp only [preCantorSet_zero, inv_nonneg]

Result:
case zero

⊢ 1 / 4 ∈ Set.Icc 0 1 ∧ 3 / 4 ∈ Set.Icc 0 1
-- Mathlib/Algebra/AddTorsor/Basic.lean
theorem vadd_eq_vadd_iff_sub_eq_vsub {v₁ v₂ : G} {p₁ p₂ : P} :
    v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ v₂ - v₁ = p₁ -ᵥ p₂

Proof state:
G : Type u_1
P : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
v₁ v₂ : G
p₁ p₂ : P
⊢ v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ v₂ - v₁ = p₁ -ᵥ p₂

Tactic:
rw [vadd_eq_vadd_iff_neg_add_eq_vsub, neg_add_eq_sub]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem natAbs_mul_self' (a : Int) : (natAbs a * natAbs a : Int) = a * a

Proof state:
a : Int
⊢ ↑a.natAbs * ↑a.natAbs = a * a

Tactic:
rw [← Int.ofNat_mul, natAbs_mul_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldl_filter (p : α → Bool) (f : β → α → β) (l : Array α) (init : β) :
    (l.filter p).foldl f init = l.foldl (fun x y => if p y then f x y else x) init

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Bool
f : β → α → β
init : β
l : List α
⊢ foldl f init (filter p { toList := l }) = foldl (fun x y => if p y = true then f x y else x) init { toList := l }

Tactic:
rw [List.filter_toArray]

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Bool
f : β → α → β
init : β
l : List α
⊢ foldl f init (List.filter p l).toArray = foldl (fun x y => if p y = true then f x y else x) init { toList := l }

Proof state:
α : Type u_1
β : Type u_2
p : α → Bool
f : β → α → β
l : Array α
init : β
⊢ foldl f init (filter p l) = foldl (fun x y => if p y = true then f x y else x) init l

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Bool
f : β → α → β
init : β
l : List α
⊢ foldl f init (filter p { toList := l }) = foldl (fun x y => if p y = true then f x y else x) init { toList := l }

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Bool
f : β → α → β
init : β
l : List α
⊢ foldl f init (List.filter p l).toArray = foldl (fun x y => if p y = true then f x y else x) init { toList := l }

Tactic:
simp [List.foldl_filter]

Result:
no goals
-- Mathlib/Probability/ConditionalProbability.lean
theorem cond_isProbabilityMeasure_of_finite (hcs : μ s ≠ 0) (hs : μ s ≠ ∞) :
    IsProbabilityMeasure μ[|s] :=
  ⟨by
    unfold ProbabilityTheory.cond
    simp only [Measure.coe_smul, Pi.smul_apply, MeasurableSet.univ, Measure.restrict_apply,
      Set.univ_inter, smul_eq_mul]
    exact ENNReal.inv_mul_cancel hcs hs⟩

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hcs : μ s ≠ 0
hs : μ s ≠ ⊤
⊢ μ[univ | s] = 1

Tactic:
unfold ProbabilityTheory.cond

Result:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hcs : μ s ≠ 0
hs : μ s ≠ ⊤
⊢ ((μ s)⁻¹ • μ.restrict s) univ = 1

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hcs : μ s ≠ 0
hs : μ s ≠ ⊤
⊢ (μ s)⁻¹ * μ s = 1

Tactic:
exact ENNReal.inv_mul_cancel hcs hs

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hcs : μ s ≠ 0
hs : μ s ≠ ⊤
⊢ ((μ s)⁻¹ • μ.restrict s) univ = 1

Tactic:
simp only [Measure.coe_smul, Pi.smul_apply, MeasurableSet.univ, Measure.restrict_apply,
  Set.univ_inter, smul_eq_mul]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hcs : μ s ≠ 0
hs : μ s ≠ ⊤
⊢ (μ s)⁻¹ * μ s = 1
-- Mathlib/Data/Complex/Norm.lean
theorem abs_im_le_norm (z : ℂ) : |z.im| ≤ ‖z‖ :=
  Real.abs_le_sqrt <| by
    rw [normSq_apply, ← sq, ← sq]
    exact le_add_of_nonneg_left (sq_nonneg _)

Proof state:
z : ℂ
⊢ z.im ^ 2 ≤ z.re ^ 2 + z.im ^ 2

Tactic:
exact le_add_of_nonneg_left (sq_nonneg _)

Result:
no goals

Proof state:
z : ℂ
⊢ z.im ^ 2 ≤ normSq z

Tactic:
rw [normSq_apply, ← sq, ← sq]

Result:
z : ℂ
⊢ z.im ^ 2 ≤ z.re ^ 2 + z.im ^ 2
-- Mathlib/NumberTheory/Cyclotomic/Three.lean
/-- If `λ` divides `x + 1`, then `λ ^ 4` divides `x ^ 3 + 1`. -/
lemma lambda_pow_four_dvd_cube_add_one_of_dvd_add_one {x : 𝓞 K} (h : λ ∣ x + 1) :
    λ ^ 4 ∣ x ^ 3 + 1

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : λ ∣ -x - 1
⊢ λ ^ 4 ∣ x ^ 3 + 1

Tactic:
convert (lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one hζ h).neg_right using 1

Result:
case h.e'_4
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : λ ∣ -x - 1
⊢ x ^ 3 + 1 = -((-x) ^ 3 - 1)

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : λ ∣ x + 1
⊢ λ ^ 4 ∣ x ^ 3 + 1

Tactic:
replace h : λ ∣ -x - 1 := by
  convert h.neg_right using 1
  exact (neg_add' x 1).symm

Result:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : λ ∣ -x - 1
⊢ λ ^ 4 ∣ x ^ 3 + 1

Proof state:
case h.e'_4
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : λ ∣ -x - 1
⊢ x ^ 3 + 1 = -((-x) ^ 3 - 1)

Tactic:
ring

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : λ ∣ x + 1
⊢ λ ∣ -x - 1

Tactic:
convert h.neg_right using 1

Result:
case h.e'_4
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : λ ∣ x + 1
⊢ -x - 1 = -(x + 1)

Proof state:
case h.e'_4
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
x : 𝓞 K
h : λ ∣ x + 1
⊢ -x - 1 = -(x + 1)

Tactic:
exact (neg_add' x 1).symm

Result:
no goals
-- Mathlib/Combinatorics/Additive/ETransform.lean
theorem mulDysonETransform.smul_finset_snd_subset_fst :
    e • (mulDysonETransform e x).2 ⊆ (mulDysonETransform e x).1

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ e • (x.2 ∩ e⁻¹ • x.1) ⊆ x.1 ∪ e • x.2

Tactic:
rw [smul_finset_inter, smul_inv_smul, inter_comm]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.1 ∩ e • x.2 ⊆ x.1 ∪ e • x.2

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ e • (mulDysonETransform e x).2 ⊆ (mulDysonETransform e x).1

Tactic:
dsimp

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ e • (x.2 ∩ e⁻¹ • x.1) ⊆ x.1 ∪ e • x.2

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.1 ∩ e • x.2 ⊆ x.1 ∪ e • x.2

Tactic:
exact inter_subset_union

Result:
no goals
-- Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
lemma homMk'_id (f : StructuredArrow S T) : homMk' f (𝟙 f.right) = eqToHom (by aesop_cat)

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
f : StructuredArrow S T
⊢ (f.homMk' (𝟙 f.right)).right = (eqToHom ⋯).right

Tactic:
simp [eqToHom_right]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
f : StructuredArrow S T
⊢ f.homMk' (𝟙 f.right) = eqToHom ⋯

Tactic:
ext

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
f : StructuredArrow S T
⊢ (f.homMk' (𝟙 f.right)).right = (eqToHom ⋯).right

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
f : StructuredArrow S T
⊢ f = mk (f.hom ≫ T.map (𝟙 f.right))

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
theorem pullbackDiagonalMapIdIso_hom_snd :
    (pullbackDiagonalMapIdIso f g i).hom ≫ pullback.snd _ _ =
      pullback.snd _ _ ≫ pullback.snd _ _

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (asIso
            (map (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) (diagonal i)
              (map ((f ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) i i
                ((f ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) (𝟙 S) ⋯ ⋯)
              (𝟙 T) (congrHom ⋯ ⋯).hom (𝟙 (diagonalObj i)) ⋯ ⋯) ≪≫
          pullbackDiagonalMapIso i (𝟙 S) (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S))) ≪≫
            asIso (map (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S))) f g (𝟙 X) (𝟙 Y) (fst i (𝟙 S)) ⋯ ⋯)).hom ≫
      snd f g =
    snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ snd (f ≫ i) (g ≫ i)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (pullbackDiagonalMapIdIso f g i).hom ≫ snd f g =
    snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ snd (f ≫ i) (g ≫ i)

Tactic:
delta pullbackDiagonalMapIdIso

Result:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
X Y : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ (asIso
            (map (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) (diagonal i)
              (map ((f ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ snd i (𝟙 S)) i i
                ((f ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) ((g ≫ inv (fst i (𝟙 S))) ≫ fst i (𝟙 S)) (𝟙 S) ⋯ ⋯)
              (𝟙 T) (congrHom ⋯ ⋯).hom (𝟙 (diagonalObj i)) ⋯ ⋯) ≪≫
          pullbackDiagonalMapIso i (𝟙 S) (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S))) ≪≫
            asIso (map (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S))) f g (𝟙 X) (𝟙 Y) (fst i (𝟙 S)) ⋯ ⋯)).hom ≫
      snd f g =
    snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ snd (f ≫ i) (g ≫ i)
-- Mathlib/Data/DFinsupp/Submonoid.lean
theorem AddSubmonoid.iSup_eq_mrange_dfinsupp_sumAddHom
    [AddCommMonoid γ] (S : ι → AddSubmonoid γ) :
    iSup S = AddMonoidHom.mrange (DFinsupp.sumAddHom fun i => (S i).subtype)

Proof state:
ι : Type u
γ : Type w
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
i : ι
y : γ
hy : y ∈ S i
⊢ y ∈ AddMonoidHom.mrange (sumAddHom fun i => (S i).subtype)

Tactic:
exact ⟨DFinsupp.single i ⟨y, hy⟩, DFinsupp.sumAddHom_single _ _ _⟩

Result:
no goals

Proof state:
ι : Type u
γ : Type w
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ ∀ (i : ι), S i ≤ AddMonoidHom.mrange (sumAddHom fun i => (S i).subtype)

Tactic:
intro i y hy

Result:
ι : Type u
γ : Type w
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
i : ι
y : γ
hy : y ∈ S i
⊢ y ∈ AddMonoidHom.mrange (sumAddHom fun i => (S i).subtype)

Proof state:
ι : Type u
γ : Type w
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ iSup S = AddMonoidHom.mrange (sumAddHom fun i => (S i).subtype)

Tactic:
apply le_antisymm

Result:
case a
ι : Type u
γ : Type w
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ iSup S ≤ AddMonoidHom.mrange (sumAddHom fun i => (S i).subtype)

case a
ι : Type u
γ : Type w
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ AddMonoidHom.mrange (sumAddHom fun i => (S i).subtype) ≤ iSup S

Proof state:
case a.intro
ι : Type u
γ : Type w
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
⊢ (sumAddHom fun i => (S i).subtype) v ∈ iSup S

Tactic:
exact dfinsupp_sumAddHom_mem _ v _ fun i _ => (le_iSup S i : S i ≤ _) (v i).prop

Result:
no goals

Proof state:
case a
ι : Type u
γ : Type w
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ AddMonoidHom.mrange (sumAddHom fun i => (S i).subtype) ≤ iSup S

Tactic:
rintro x ⟨v, rfl⟩

Result:
case a.intro
ι : Type u
γ : Type w
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
⊢ (sumAddHom fun i => (S i).subtype) v ∈ iSup S

Proof state:
case a
ι : Type u
γ : Type w
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ iSup S ≤ AddMonoidHom.mrange (sumAddHom fun i => (S i).subtype)

Tactic:
apply iSup_le _

Result:
ι : Type u
γ : Type w
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ ∀ (i : ι), S i ≤ AddMonoidHom.mrange (sumAddHom fun i => (S i).subtype)
-- Mathlib/Algebra/Homology/ExactSequence.lean
lemma exact_iff_δ₀ (S : ComposableArrows C (n + 2)) :
    S.Exact ↔ (mk₂ (S.map' 0 1) (S.map' 1 2)).Exact ∧ S.δ₀.Exact

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
⊢ S.Exact → (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact ∧ S.δ₀.Exact

Tactic:
intro h

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact ∧ S.δ₀.Exact

Proof state:
case mpr.intro.refine_1
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact
h₀ : S.δ₀.Exact
i : ℕ
hi : autoParam (i + 2 ≤ n + 2) _auto✝
⊢ S.map' i (i + 1) ⋯ ⋯ ≫ S.map' (i + 1) (i + 2) ⋯ hi = 0

Tactic:
obtain _ | i := i

Result:
case mpr.intro.refine_1.zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact
h₀ : S.δ₀.Exact
hi : autoParam (0 + 2 ≤ n + 2) _auto✝
⊢ S.map' 0 (0 + 1) ⋯ ⋯ ≫ S.map' (0 + 1) (0 + 2) ⋯ hi = 0

case mpr.intro.refine_1.succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact
h₀ : S.δ₀.Exact
i : ℕ
hi : autoParam (i + 1 + 2 ≤ n + 2) _auto✝
⊢ S.map' (i + 1) (i + 1 + 1) ⋯ ⋯ ≫ S.map' (i + 1 + 1) (i + 1 + 2) ⋯ hi = 0
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocDiv_sub_eq_toIocDiv_add (a b c : α) :
    toIocDiv hp a (b - c) = toIocDiv hp (a + c) b

Proof state:
case h
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ b - c - toIocDiv hp (a + c) b • p ∈ Set.Ioc a (a + p)

Tactic:
rw [← sub_right_comm, Set.sub_mem_Ioc_iff_left, add_right_comm]

Result:
case h
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ b - toIocDiv hp (a + c) b • p ∈ Set.Ioc (a + c) (a + c + p)

Proof state:
case h
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ b - toIocDiv hp (a + c) b • p ∈ Set.Ioc (a + c) (a + c + p)

Tactic:
exact sub_toIocDiv_zsmul_mem_Ioc hp (a + c) b

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIocDiv hp a (b - c) = toIocDiv hp (a + c) b

Tactic:
apply toIocDiv_eq_of_sub_zsmul_mem_Ioc

Result:
case h
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ b - c - toIocDiv hp (a + c) b • p ∈ Set.Ioc a (a + p)
-- Mathlib/Data/List/OfFn.lean
theorem get_ofFn {n} (f : Fin n → α) (i) : get (ofFn f) i = f (Fin.cast (by simp) i)

Proof state:
α : Type u
n : ℕ
f : Fin n → α
i : Fin (ofFn f).length
⊢ (ofFn f).get i = f (Fin.cast ⋯ i)

Tactic:
simp

Result:
α : Type u
n : ℕ
f : Fin n → α
i : Fin (ofFn f).length
⊢ f ⟨↑i, ⋯⟩ = f (Fin.cast ⋯ i)

Proof state:
α : Type u
n : ℕ
f : Fin n → α
i : Fin (ofFn f).length
⊢ f ⟨↑i, ⋯⟩ = f (Fin.cast ⋯ i)

Tactic:
congr

Result:
no goals

Proof state:
α : Type u
n : ℕ
f : Fin n → α
i : Fin (ofFn f).length
⊢ (ofFn f).length = n

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Set/OrderEmbedding.lean
theorem preimage_Ico : e ⁻¹' Ico (e x) (e y) = Ico x y

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y x✝ : α
⊢ x✝ ∈ ⇑e ⁻¹' Ico (e x) (e y) ↔ x✝ ∈ Ico x y

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y : α
⊢ ⇑e ⁻¹' Ico (e x) (e y) = Ico x y

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y x✝ : α
⊢ x✝ ∈ ⇑e ⁻¹' Ico (e x) (e y) ↔ x✝ ∈ Ico x y