harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/TopologicallyNilpotent.lean
theorem mul_right_of_commute [IsLinearTopology Rᵐᵒᵖ R]
    {a b : R} (ha : IsTopologicallyNilpotent a) (hab : Commute a b) :
    IsTopologicallyNilpotent (a * b)

Proof state:
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : Ring R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
a b : R
ha : IsTopologicallyNilpotent a
hab : Commute a b
⊢ Tendsto (fun x => a ^ x * b ^ x) atTop (𝓝 0)

Tactic:
exact IsLinearTopology.tendsto_mul_zero_of_left _ _ ha

Result:
no goals

Proof state:
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : Ring R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
a b : R
ha : IsTopologicallyNilpotent a
hab : Commute a b
⊢ IsTopologicallyNilpotent (a * b)

Tactic:
simp_rw [IsTopologicallyNilpotent, hab.mul_pow]

Result:
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : Ring R
inst✝ : IsLinearTopology Rᵐᵒᵖ R
a b : R
ha : IsTopologicallyNilpotent a
hab : Commute a b
⊢ Tendsto (fun x => a ^ x * b ^ x) atTop (𝓝 0)
-- Mathlib/Data/Finset/Basic.lean
theorem filter_eq [DecidableEq β] (s : Finset β) (b : β) :
    s.filter (Eq b) = ite (b ∈ s) {b} ∅

Proof state:
β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b : β
⊢ filter (Eq b) s = if b ∈ s then {b} else ∅

Tactic:
split_ifs with h

Result:
case pos
β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b : β
h : b ∈ s
⊢ filter (Eq b) s = {b}

case neg
β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b : β
h : b ∉ s
⊢ filter (Eq b) s = ∅

Proof state:
case neg.h
β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b : β
h : b ∉ s
a✝ : β
⊢ a✝ ∈ s → ¬b = a✝

Tactic:
rintro m rfl

Result:
case neg.h
β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b : β
h : b ∉ s
m : b ∈ s
⊢ False

Proof state:
case pos
β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b : β
h : b ∈ s
⊢ filter (Eq b) s = {b}

Tactic:
ext

Result:
case pos.h
β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b : β
h : b ∈ s
a✝ : β
⊢ a✝ ∈ filter (Eq b) s ↔ a✝ ∈ {b}

Proof state:
case pos.h
β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b : β
h : b ∈ s
a✝ : β
⊢ a✝ ∈ filter (Eq b) s ↔ a✝ ∈ {b}

Tactic:
simp only [mem_filter, mem_singleton, decide_eq_true_eq]

Result:
case pos.h
β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b : β
h : b ∈ s
a✝ : β
⊢ a✝ ∈ s ∧ b = a✝ ↔ a✝ = b

Proof state:
case pos.h
β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b : β
h : b ∈ s
a✝ : β
⊢ a✝ ∈ s ∧ b = a✝ ↔ a✝ = b

Tactic:
refine ⟨fun h => h.2.symm, ?_⟩

Result:
case pos.h
β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b : β
h : b ∈ s
a✝ : β
⊢ a✝ = b → a✝ ∈ s ∧ b = a✝

Proof state:
case neg
β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b : β
h : b ∉ s
⊢ filter (Eq b) s = ∅

Tactic:
ext

Result:
case neg.h
β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b : β
h : b ∉ s
a✝ : β
⊢ a✝ ∈ filter (Eq b) s ↔ a✝ ∈ ∅

Proof state:
case neg.h
β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b : β
h : b ∉ s
m : b ∈ s
⊢ False

Tactic:
exact h m

Result:
no goals

Proof state:
case pos.h
β : Type u_2
inst✝ : DecidableEq β
s : Finset β
a✝ : β
h : a✝ ∈ s
⊢ a✝ ∈ s ∧ a✝ = a✝

Tactic:
exact ⟨h, rfl⟩

Result:
no goals

Proof state:
case neg.h
β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b : β
h : b ∉ s
a✝ : β
⊢ a✝ ∈ filter (Eq b) s ↔ a✝ ∈ ∅

Tactic:
simp only [mem_filter, not_and, iff_false, not_mem_empty, decide_eq_true_eq]

Result:
case neg.h
β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b : β
h : b ∉ s
a✝ : β
⊢ a✝ ∈ s → ¬b = a✝

Proof state:
case pos.h
β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b : β
h : b ∈ s
a✝ : β
⊢ a✝ = b → a✝ ∈ s ∧ b = a✝

Tactic:
rintro rfl

Result:
case pos.h
β : Type u_2
inst✝ : DecidableEq β
s : Finset β
a✝ : β
h : a✝ ∈ s
⊢ a✝ ∈ s ∧ a✝ = a✝
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tsum_const_smul {R} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (a : R) :
    ∑' i, a • f i = a • ∑' i, f i

Proof state:
α : Type u_1
f : α → ℝ≥0∞
R : Type u_4
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
a : R
⊢ ∑' (i : α), a • f i = a • ∑' (i : α), f i

Tactic:
simpa only [smul_one_mul] using @ENNReal.tsum_mul_left _ (a • (1 : ℝ≥0∞)) _

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Vieta.lean
theorem esymm_neg (s : Multiset R) (k : ℕ) : (map Neg.neg s).esymm k = (-1) ^ k * esymm s k

Proof state:
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
⊢ ∀ x ∈ powersetCard k s, (prod ∘ map Neg.neg) x = (-1) ^ k * x.prod

Tactic:
intro x hx

Result:
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
⊢ (prod ∘ map Neg.neg) x = (-1) ^ k * x.prod

Proof state:
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
⊢ (map Neg.neg s).esymm k = (-1) ^ k * s.esymm k

Tactic:
rw [esymm, esymm, ← Multiset.sum_map_mul_left, Multiset.powersetCard_map, Multiset.map_map,
  map_congr rfl]

Result:
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
⊢ ∀ x ∈ powersetCard k s, (prod ∘ map Neg.neg) x = (-1) ^ k * x.prod

Proof state:
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
⊢ (prod ∘ map Neg.neg) x = (map (Function.const R (-1)) x).prod * (map (fun x => x) x).prod

Tactic:
rw [← prod_map_mul, map_congr rfl, Function.comp_apply]

Result:
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
⊢ ∀ x_1 ∈ x, Function.const R (-1) x_1 * x_1 = -x_1

Proof state:
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
⊢ (prod ∘ map Neg.neg) x = (-1) ^ k * x.prod

Tactic:
rw [(mem_powersetCard.mp hx).right.symm, ← prod_replicate, ← Multiset.map_const]

Result:
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
⊢ (prod ∘ map Neg.neg) x = (map (Function.const R (-1)) x).prod * x.prod

Proof state:
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
⊢ ∀ x_1 ∈ x, Function.const R (-1) x_1 * x_1 = -x_1

Tactic:
exact fun z _ => neg_one_mul z

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
⊢ (prod ∘ map Neg.neg) x = (map (Function.const R (-1)) x).prod * x.prod

Tactic:
nth_rw 3 [← map_id' x]

Result:
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
⊢ (prod ∘ map Neg.neg) x = (map (Function.const R (-1)) x).prod * (map (fun x => x) x).prod
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem add_log_le_log_mul {x y : Ordinal} (b : Ordinal) (hx : x ≠ 0) (hy : y ≠ 0) :
    log b x + log b y ≤ log b (x * y)

Proof state:
case inl
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : 1 < b
⊢ b ^ log b x * b ^ log b y ≤ x * y

Tactic:
exact mul_le_mul' (opow_log_le_self b hx) (opow_log_le_self b hy)

Result:
no goals

Proof state:
case inr
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : b ≤ 1
⊢ log b x + log b y ≤ log b (x * y)

Tactic:
simpa only [log_of_left_le_one hb, zero_add] using le_rfl

Result:
no goals

Proof state:
case inl
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : 1 < b
⊢ log b x + log b y ≤ log b (x * y)

Tactic:
rw [← opow_le_iff_le_log hb (mul_ne_zero hx hy), opow_add]

Result:
case inl
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : 1 < b
⊢ b ^ log b x * b ^ log b y ≤ x * y

Proof state:
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
⊢ log b x + log b y ≤ log b (x * y)

Tactic:
obtain hb | hb := lt_or_le 1 b

Result:
case inl
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : 1 < b
⊢ log b x + log b y ≤ log b (x * y)

case inr
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : b ≤ 1
⊢ log b x + log b y ≤ log b (x * y)
-- Mathlib/Algebra/Star/StarAlgHom.lean
theorem fst_prod (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C) : (fst R B C).comp (prod f g) = f

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Star A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Star B
inst✝² : Semiring C
inst✝¹ : Algebra R C
inst✝ : Star C
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
⊢ (fst R B C).comp (f.prod g) = f

Tactic:
ext

Result:
case h
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Star A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Star B
inst✝² : Semiring C
inst✝¹ : Algebra R C
inst✝ : Star C
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
x✝ : A
⊢ ((fst R B C).comp (f.prod g)) x✝ = f x✝

Proof state:
case h
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Star A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Star B
inst✝² : Semiring C
inst✝¹ : Algebra R C
inst✝ : Star C
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
x✝ : A
⊢ ((fst R B C).comp (f.prod g)) x✝ = f x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
theorem isTheta_exp_arg_mul_im (hl : IsBoundedUnder (· ≤ ·) l fun x => |(g x).im|) :
    (fun x => Real.exp (arg (f x) * im (g x))) =Θ[l] fun _ => (1 : ℝ)

Proof state:
case intro
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (x : ℝ) in Filter.map (fun x => |(g x).im|) l, (fun x1 x2 => x1 ≤ x2) x b
⊢ ∀ᶠ (x : ℝ) in Filter.map (fun x => |(f x).arg * (g x).im|) l, (fun x1 x2 => x1 ≤ x2) x (π * b)

Tactic:
rw [eventually_map] at hb ⊢

Result:
case intro
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (a : α) in l, (fun x1 x2 => x1 ≤ x2) |(g a).im| b
⊢ ∀ᶠ (a : α) in l, (fun x1 x2 => x1 ≤ x2) |(f a).arg * (g a).im| (π * b)

Proof state:
case intro
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (x : ℝ) in Filter.map (fun x => |(g x).im|) l, (fun x1 x2 => x1 ≤ x2) x b
⊢ (fun x => rexp ((f x).arg * (g x).im)) =Θ[l] fun x => 1

Tactic:
refine Real.isTheta_exp_comp_one.2 ⟨π * b, ?_⟩

Result:
case intro
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (x : ℝ) in Filter.map (fun x => |(g x).im|) l, (fun x1 x2 => x1 ≤ x2) x b
⊢ ∀ᶠ (x : ℝ) in Filter.map (fun x => |(f x).arg * (g x).im|) l, (fun x1 x2 => x1 ≤ x2) x (π * b)

Proof state:
case intro
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (a : α) in l, (fun x1 x2 => x1 ≤ x2) |(g a).im| b
x : α
hx : (fun x1 x2 => x1 ≤ x2) |(g x).im| b
⊢ (fun x1 x2 => x1 ≤ x2) |(f x).arg * (g x).im| (π * b)

Tactic:
rw [abs_mul]

Result:
case intro
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (a : α) in l, (fun x1 x2 => x1 ≤ x2) |(g a).im| b
x : α
hx : (fun x1 x2 => x1 ≤ x2) |(g x).im| b
⊢ (fun x1 x2 => x1 ≤ x2) (|(f x).arg| * |(g x).im|) (π * b)

Proof state:
case intro
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (a : α) in l, (fun x1 x2 => x1 ≤ x2) |(g a).im| b
⊢ ∀ᶠ (a : α) in l, (fun x1 x2 => x1 ≤ x2) |(f a).arg * (g a).im| (π * b)

Tactic:
refine hb.mono fun x hx => ?_

Result:
case intro
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (a : α) in l, (fun x1 x2 => x1 ≤ x2) |(g a).im| b
x : α
hx : (fun x1 x2 => x1 ≤ x2) |(g x).im| b
⊢ (fun x1 x2 => x1 ≤ x2) |(f x).arg * (g x).im| (π * b)

Proof state:
α : Type u_1
l : Filter α
f g : α → ℂ
hl : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => |(g x).im|
⊢ (fun x => rexp ((f x).arg * (g x).im)) =Θ[l] fun x => 1

Tactic:
rcases hl with ⟨b, hb⟩

Result:
case intro
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (x : ℝ) in Filter.map (fun x => |(g x).im|) l, (fun x1 x2 => x1 ≤ x2) x b
⊢ (fun x => rexp ((f x).arg * (g x).im)) =Θ[l] fun x => 1

Proof state:
case intro
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℝ
hb : ∀ᶠ (a : α) in l, (fun x1 x2 => x1 ≤ x2) |(g a).im| b
x : α
hx : (fun x1 x2 => x1 ≤ x2) |(g x).im| b
⊢ (fun x1 x2 => x1 ≤ x2) (|(f x).arg| * |(g x).im|) (π * b)

Tactic:
exact mul_le_mul (abs_arg_le_pi _) hx (abs_nonneg _) Real.pi_pos.le

Result:
no goals
-- Mathlib/Data/Finite/Card.lean
theorem card_eq [Finite α] [Finite β] : Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
this✝ : Fintype α
this : Fintype β
⊢ Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)

Tactic:
simp only [Nat.card_eq_fintype_card, Fintype.card_eq]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
⊢ Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)

Tactic:
haveI := Fintype.ofFinite α

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
this : Fintype α
⊢ Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
this : Fintype α
⊢ Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)

Tactic:
haveI := Fintype.ofFinite β

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
this✝ : Fintype α
this : Fintype β
⊢ Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filterMap_flatMap {β γ} (l : List α) (g : α → List β) (f : β → Option γ) :
    (l.flatMap g).filterMap f = l.flatMap fun a => (g a).filterMap f

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
g : α → List β
f : β → Option γ
⊢ filterMap f (flatMap g l) = flatMap (fun a => filterMap f (g a)) l

Tactic:
induction l <;> simp [*]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean
theorem denote_blastConst (aig : AIG α) (c : BitVec w) (assign : α → Bool) :
    ∀ (idx : Nat) (hidx : idx < w),
        ⟦(blastConst aig c).aig, (blastConst aig c).vec.get idx hidx, assign⟧
          =
        c.getLsbD idx

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
c : BitVec w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦assign, { aig := (blastConst aig c).aig, ref := (blastConst aig c).vec.get idx✝ hidx✝ }⟧ = c.getLsbD idx✝

Tactic:
apply blastConst.go_denote_eq

Result:
case a
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
c : BitVec w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ 0 ≤ idx✝

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
c : BitVec w
assign : α → Bool
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign, { aig := (blastConst aig c).aig, ref := (blastConst aig c).vec.get idx hidx }⟧ = c.getLsbD idx

Tactic:
intros

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
c : BitVec w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦assign, { aig := (blastConst aig c).aig, ref := (blastConst aig c).vec.get idx✝ hidx✝ }⟧ = c.getLsbD idx✝

Proof state:
case a
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
c : BitVec w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ 0 ≤ idx✝

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldr_map_hom (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : List α)
    (h : ∀ x y, f' (g x) (g y) = g (f x y)) :
    (l.map g).foldr f' (g a) = g (l.foldr f a)

Proof state:
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
l : List α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
⊢ foldr f' (g a) (map g l) = g (foldr f a l)

Tactic:
induction l generalizing a

Result:
case nil
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
a : α
⊢ foldr f' (g a) (map g []) = g (foldr f a [])

case cons
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (a : α), foldr f' (g a) (map g tail✝) = g (foldr f a tail✝)
a : α
⊢ foldr f' (g a) (map g (head✝ :: tail✝)) = g (foldr f a (head✝ :: tail✝))

Proof state:
case cons
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (a : α), foldr f' (g a) (map g tail✝) = g (foldr f a tail✝)
a : α
⊢ foldr f' (g a) (map g (head✝ :: tail✝)) = g (foldr f a (head✝ :: tail✝))

Tactic:
simp [*, h]

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
a : α
⊢ foldr f' (g a) (map g []) = g (foldr f a [])

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See `lt_mul_inv_iff₀'` for a version with multiplication on the other side. -/
lemma lt_mul_inv_iff₀ (hc : 0 < c) : a < b * c⁻¹ ↔ a * c < b where
  mp h

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : MulPosStrictMono G₀
hc : 0 < c
h : a < b * c⁻¹
⊢ a * c < b

Tactic:
simpa [hc.ne'] using mul_lt_mul_of_pos_right h hc

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : MulPosStrictMono G₀
hc : 0 < c
h : a * c < b
⊢ a < b * c⁻¹

Tactic:
simpa [hc.ne'] using mul_lt_mul_of_pos_right h (inv_pos.2 hc)

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
/-- If a short complex `S` is such that `S.g = 0` and that the cokernel of `S.f` is preserved
by a functor `F`, then `F` preserves the right homology of `S`. -/
lemma preservesRightHomology_of_zero_g (hg : S.g = 0)
    [PreservesColimit (parallelPair S.f 0) F] :
    F.PreservesRightHomologyOf S := ⟨fun h =>
  { f

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_3, u_1} C
inst✝⁴ : Category.{u_4, u_2} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hg : S.g = 0
inst✝ : PreservesColimit (parallelPair S.f 0) F
h : S.RightHomologyData
⊢ h.g' = 0

Tactic:
rw [← cancel_epi h.p, h.p_g', comp_zero, hg]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_3, u_1} C
inst✝⁴ : Category.{u_4, u_2} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hg : S.g = 0
inst✝ : PreservesColimit (parallelPair S.f 0) F
h : S.RightHomologyData
⊢ PreservesColimit (parallelPair S.f 0) F

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Data/Multiset/Nodup.lean
theorem nodup_union [DecidableEq α] {s t : Multiset α} : Nodup (s ∪ t) ↔ Nodup s ∧ Nodup t :=
  ⟨fun h => ⟨nodup_of_le le_union_left h, nodup_of_le le_union_right h⟩, fun ⟨h₁, h₂⟩ =>
    nodup_iff_count_le_one.2 fun a => by
      rw [count_union]
      exact max_le (nodup_iff_count_le_one.1 h₁ a) (nodup_iff_count_le_one.1 h₂ a)⟩

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
x✝ : s.Nodup ∧ t.Nodup
h₁ : s.Nodup
h₂ : t.Nodup
a : α
⊢ count a (s ∪ t) ≤ 1

Tactic:
rw [count_union]

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
x✝ : s.Nodup ∧ t.Nodup
h₁ : s.Nodup
h₂ : t.Nodup
a : α
⊢ count a s ⊔ count a t ≤ 1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
x✝ : s.Nodup ∧ t.Nodup
h₁ : s.Nodup
h₂ : t.Nodup
a : α
⊢ count a s ⊔ count a t ≤ 1

Tactic:
exact max_le (nodup_iff_count_le_one.1 h₁ a) (nodup_iff_count_le_one.1 h₂ a)

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
lemma IsGreatest.norm_cfc [Nontrivial A] (f : 𝕜 → 𝕜) (a : A)
    (hf : ContinuousOn f (σ 𝕜 a)

Proof state:
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σ 𝕜 a)) _auto✝
ha : autoParam (p a) _auto✝
x : 𝕜
hx' : x ∈ σ 𝕜 a
hx : IsGreatest ((fun x => ‖f x‖) '' σ 𝕜 a) ((fun x => ‖f x‖) x)
⊢ (fun x => ‖f x‖) x ≤ ‖{ toFun := (σ 𝕜 a).restrict f, continuous_toFun := ⋯ } ⟨x, hx'⟩‖

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_4.a
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σ 𝕜 a)) _auto✝
ha : autoParam (p a) _auto✝
x : 𝕜
hx' : x ∈ σ 𝕜 a
hx : IsGreatest ((fun x => ‖f x‖) '' σ 𝕜 a) ((fun x => ‖f x‖) x)
⊢ ∀ (x_1 : ↑(σ 𝕜 a)), ‖{ toFun := (σ 𝕜 a).restrict f, continuous_toFun := ⋯ } x_1‖ ≤ ‖f x‖

Tactic:
rintro ⟨y, hy⟩

Result:
case h.e'_4.a.mk
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedRing A
inst✝³ : StarRing A
inst✝² : NormedAlgebra 𝕜 A
inst✝¹ : IsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : Nontrivial A
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σ 𝕜 a)) _auto✝
ha : autoParam (p a) _auto✝
x : 𝕜
hx' : x ∈ σ 𝕜 a
hx : IsGreatest ((fun x => ‖f x‖) '' σ 𝕜 a) ((fun x => ‖f x‖) x)
y : 𝕜
hy : y ∈ σ 𝕜 a
⊢ ‖{ toFun := (σ 𝕜 a).restrict f, continuous_toFun := ⋯ } ⟨y, hy⟩‖ ≤ ‖f x‖
-- Mathlib/RingTheory/GradedAlgebra/Basic.lean
theorem coe_decompose_mul_of_right_mem_zero [AddMonoid ι] [GradedRing 𝒜] {a b : A}
    (b_mem : b ∈ 𝒜 0) : (decompose 𝒜 (a * b) i : A) = decompose 𝒜 a i * b

Proof state:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i : ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
a b : A
b_mem : b ∈ 𝒜 0
⊢ ↑(((decompose 𝒜) (a * b)) i) = ↑(((decompose 𝒜) a) i) * b

Tactic:
lift b to 𝒜 0 using b_mem

Result:
case intro
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i : ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
a : A
b : ↥(𝒜 0)
⊢ ↑(((decompose 𝒜) (a * ↑b)) i) = ↑(((decompose 𝒜) a) i) * ↑b

Proof state:
case intro
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i : ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
a : A
b : ↥(𝒜 0)
⊢ ↑(((decompose 𝒜) (a * ↑b)) i) = ↑(((decompose 𝒜) a) i) * ↑b

Tactic:
rw [decompose_mul, decompose_coe, coe_mul_of_apply_of_mem_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean
@[simp]
lemma PrelaxFunctor.map₂_eqToHom (F : PrelaxFunctor B C) {a b : B} {f g : a ⟶ b} (h : f = g) :
    F.map₂ (eqToHom h) = eqToHom (F.congr_map h)

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : PrelaxFunctor B C
a b : B
f g : a ⟶ b
h : f = g
⊢ F.map₂ (eqToHom h) = eqToHom ⋯

Tactic:
subst h

Result:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : PrelaxFunctor B C
a b : B
f : a ⟶ b
⊢ F.map₂ (eqToHom ⋯) = eqToHom ⋯

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : PrelaxFunctor B C
a b : B
f : a ⟶ b
⊢ F.map₂ (eqToHom ⋯) = eqToHom ⋯

Tactic:
simp only [eqToHom_refl, PrelaxFunctor.map₂_id]

Result:
no goals
-- Mathlib/Algebra/ZeroOne/Lemmas.lean
@[to_additive dite_pos]
lemma one_lt_dite [LT α] (ha : ∀ h, 1 < a h) (hb : ∀ h, 1 < b h) : 1 < dite p a b

Proof state:
case isTrue
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LT α
ha : ∀ (h : p), 1 < a h
hb : ∀ (h : ¬p), 1 < b h
h✝ : p
⊢ 1 < a h✝

case isFalse
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LT α
ha : ∀ (h : p), 1 < a h
hb : ∀ (h : ¬p), 1 < b h
h✝ : ¬p
⊢ 1 < b h✝

Tactic:
exacts [ha ‹_›, hb ‹_›]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LT α
ha : ∀ (h : p), 1 < a h
hb : ∀ (h : ¬p), 1 < b h
⊢ 1 < dite p a b

Tactic:
split

Result:
case isTrue
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LT α
ha : ∀ (h : p), 1 < a h
hb : ∀ (h : ¬p), 1 < b h
h✝ : p
⊢ 1 < a h✝

case isFalse
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a : p → α
b : ¬p → α
inst✝ : LT α
ha : ∀ (h : p), 1 < a h
hb : ∀ (h : ¬p), 1 < b h
h✝ : ¬p
⊢ 1 < b h✝