harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/GroupAction/Basic.lean
theorem stabilizer_vadd_eq_stabilizer_map_conj (g : G) (a : α) :
    stabilizer G (g +ᵥ a) = (stabilizer G a).map (AddAut.conj g).toAddMonoidHom

Proof state:
case h
G : Type u_1
α : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddAction G α
g : G
a : α
h : G
⊢ h ∈ stabilizer G (g +ᵥ a) ↔ h ∈ AddSubgroup.map (AddEquiv.toAddMonoidHom (AddAut.conj g)) (stabilizer G a)

Tactic:
rw [mem_stabilizer_iff, ← vadd_left_cancel_iff (-g), vadd_vadd, vadd_vadd, vadd_vadd,
  neg_add_cancel, zero_vadd, ← mem_stabilizer_iff, AddSubgroup.mem_map_equiv,
  AddAut.conj_symm_apply]

Result:
no goals

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddAction G α
g : G
a : α
⊢ stabilizer G (g +ᵥ a) = AddSubgroup.map (AddEquiv.toAddMonoidHom (AddAut.conj g)) (stabilizer G a)

Tactic:
ext h

Result:
case h
G : Type u_1
α : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddAction G α
g : G
a : α
h : G
⊢ h ∈ stabilizer G (g +ᵥ a) ↔ h ∈ AddSubgroup.map (AddEquiv.toAddMonoidHom (AddAut.conj g)) (stabilizer G a)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey?_insertEntryIfNew [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
    {v : β k} : getKey? a (insertEntryIfNew k v l) =
      if k == a ∧ containsKey k l = false then some k else getKey? a l

Proof state:
case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey k l = true
⊢ getKey? a (insertEntryIfNew k v l) = if (k == a) = true ∧ true = false then some k else getKey? a l

Tactic:
simp [insertEntryIfNew_of_containsKey h]

Result:
no goals

Proof state:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey k l = false
⊢ getKey? a (insertEntryIfNew k v l) = if (k == a) = true ∧ false = false then some k else getKey? a l

Tactic:
rw [insertEntryIfNew_of_containsKey_eq_false h]

Result:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey k l = false
⊢ getKey? a (⟨k, v⟩ :: l) = if (k == a) = true ∧ false = false then some k else getKey? a l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
⊢ getKey? a (insertEntryIfNew k v l) = if (k == a) = true ∧ containsKey k l = false then some k else getKey? a l

Tactic:
cases h : containsKey k l

Result:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey k l = false
⊢ getKey? a (insertEntryIfNew k v l) = if (k == a) = true ∧ false = false then some k else getKey? a l

case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey k l = true
⊢ getKey? a (insertEntryIfNew k v l) = if (k == a) = true ∧ true = false then some k else getKey? a l

Proof state:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey k l = false
⊢ getKey? a (⟨k, v⟩ :: l) = if (k == a) = true ∧ false = false then some k else getKey? a l

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Data/Sum/Basic.lean
theorem isRight_right (h : LiftRel r s (inr b) y) : y.isRight

Proof state:
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
y : γ ⊕ δ
b : β
h : LiftRel r s (inr b) y
⊢ y.isRight = true

Tactic:
cases h

Result:
case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
b : β
d✝ : δ
a✝ : s b d✝
⊢ (inr d✝).isRight = true

Proof state:
case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
b : β
d✝ : δ
a✝ : s b d✝
⊢ (inr d✝).isRight = true

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/FiberedCategory/Cocartesian.lean
@[simp]
lemma map_self : map p f φ (comp_id f).symm φ = 𝟙 b

Proof state:
case map.hψ
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsStronglyCocartesian (p.map φ) φ
⊢ φ ≫ 𝟙 b✝ = φ

Tactic:
simp only [comp_id]

Result:
no goals

Proof state:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsStronglyCocartesian (p.map φ) φ
⊢ 𝟙 b✝ = map p (p.map φ) φ ⋯ φ

Tactic:
apply map_uniq

Result:
case map.hψ
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsStronglyCocartesian (p.map φ) φ
⊢ φ ≫ 𝟙 b✝ = φ

Proof state:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsStronglyCocartesian (p.map φ) φ
⊢ map p (p.map φ) φ ⋯ φ = 𝟙 b✝

Tactic:
symm

Result:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsStronglyCocartesian (p.map φ) φ
⊢ 𝟙 b✝ = map p (p.map φ) φ ⋯ φ

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsStronglyCocartesian f φ
⊢ map p f φ ⋯ φ = 𝟙 b

Tactic:
subst_hom_lift p f φ

Result:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsStronglyCocartesian (p.map φ) φ
⊢ map p (p.map φ) φ ⋯ φ = 𝟙 b✝
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem map_surjective (f : S →+* T) (hf : Function.Surjective f) :
    Function.Surjective (PowerSeries.map f)

Proof state:
case h.h
S : Type u_2
T : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* T
hf : Function.Surjective ⇑f
g : T⟦X⟧
k : ℕ
⊢ f (Classical.choose ⋯) = (coeff T k) g

Tactic:
exact Classical.choose_spec (hf ((coeff T k) g))

Result:
no goals

Proof state:
S : Type u_2
T : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* T
hf : Function.Surjective ⇑f
⊢ Function.Surjective ⇑(map f)

Tactic:
intro g

Result:
S : Type u_2
T : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* T
hf : Function.Surjective ⇑f
g : T⟦X⟧
⊢ ∃ a, (map f) a = g

Proof state:
S : Type u_2
T : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* T
hf : Function.Surjective ⇑f
g : T⟦X⟧
⊢ ∃ a, (map f) a = g

Tactic:
use PowerSeries.mk fun k ↦ Function.surjInv hf (PowerSeries.coeff _ k g)

Result:
case h
S : Type u_2
T : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* T
hf : Function.Surjective ⇑f
g : T⟦X⟧
⊢ (map f) (mk fun k => Function.surjInv hf ((coeff T k) g)) = g

Proof state:
case h.h
S : Type u_2
T : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* T
hf : Function.Surjective ⇑f
g : T⟦X⟧
k : ℕ
⊢ (coeff T k) ((map f) (mk fun k => Function.surjInv hf ((coeff T k) g))) = (coeff T k) g

Tactic:
simp only [Function.surjInv, coeff_map, coeff_mk]

Result:
case h.h
S : Type u_2
T : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* T
hf : Function.Surjective ⇑f
g : T⟦X⟧
k : ℕ
⊢ f (Classical.choose ⋯) = (coeff T k) g

Proof state:
case h
S : Type u_2
T : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* T
hf : Function.Surjective ⇑f
g : T⟦X⟧
⊢ (map f) (mk fun k => Function.surjInv hf ((coeff T k) g)) = g

Tactic:
ext k

Result:
case h.h
S : Type u_2
T : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* T
hf : Function.Surjective ⇑f
g : T⟦X⟧
k : ℕ
⊢ (coeff T k) ((map f) (mk fun k => Function.surjInv hf ((coeff T k) g))) = (coeff T k) g
-- Mathlib/Logic/Equiv/Set.lean
theorem sumCompl_symm_apply_of_not_mem {α : Type u} {s : Set α} [DecidablePred (· ∈ s)] {x : α}
    (hx : x ∉ s) : (Equiv.Set.sumCompl s).symm x = Sum.inr ⟨x, hx⟩

Proof state:
α : Type u
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
x : α
hx : x ∉ s
⊢ (Set.sumCompl s).symm x = Sum.inr ⟨x, hx⟩

Tactic:
simp [Equiv.Set.sumCompl, Equiv.Set.univ, union_apply_right, hx]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/CompleteLattice.lean
@[to_additive]
lemma sInf_inv (s : Set M) : sInf s⁻¹ = (sSup s)⁻¹

Proof state:
M : Type u_1
inst✝³ : CompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s : Set M
⊢ ⨅ a ∈ s, a⁻¹ = (sSup s)⁻¹

Tactic:
exact ((OrderIso.inv M).map_sSup _).symm

Result:
no goals

Proof state:
M : Type u_1
inst✝³ : CompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s : Set M
⊢ sInf s⁻¹ = (sSup s)⁻¹

Tactic:
rw [← image_inv_eq_inv, sInf_image]

Result:
M : Type u_1
inst✝³ : CompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s : Set M
⊢ ⨅ a ∈ s, a⁻¹ = (sSup s)⁻¹
-- Mathlib/Analysis/SpecialFunctions/Complex/Arctan.lean
theorem hasSum_arctan {z : ℂ} (hz : ‖z‖ < 1) :
    HasSum (fun n : ℕ ↦ (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)) (arctan z)

Proof state:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x => -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
k : ℕ
⊢ -I * (z ^ (2 * k + 1) * (I * (-1) ^ k)) = -(I * I) * (-1) ^ k * z ^ (2 * k + 1)

Tactic:
ring

Result:
no goals

Proof state:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x => -I / 2 * (((-1) ^ (x.1 * 2 + ↑x.2 + 1) + 1) * (z * I) ^ (x.1 * 2 + ↑x.2) / ↑(x.1 * 2 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
⊢ HasSum (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)) z.arctan

Tactic:
simp_rw [← mul_comm 2 _] at this

Result:
z : ℂ
hz : ‖z‖ < 1
this :
  HasSum (fun x => -I / 2 * (((-1) ^ (2 * x.1 + ↑x.2 + 1) + 1) * (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)))
    (-I / 2 * log ((1 + z * I) / (1 - z * I)))
⊢ HasSum (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)) z.arctan
-- Mathlib/Algebra/EuclideanDomain/Basic.lean
theorem div_self {a : R} (a0 : a ≠ 0) : a / a = 1

Proof state:
R : Type u
inst✝ : EuclideanDomain R
a : R
a0 : a ≠ 0
⊢ a / a = 1

Tactic:
simpa only [one_mul] using mul_div_cancel_right₀ 1 a0

Result:
no goals
-- Mathlib/Data/Finsupp/NeLocus.lean
theorem neLocus_neg : neLocus (-f) g = f.neLocus (-g)

Proof state:
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f g : α →₀ N
⊢ (-f).neLocus g = f.neLocus (-g)

Tactic:
rw [← neLocus_neg_neg, neg_neg]

Result:
no goals
-- Mathlib/Analysis/Complex/ReImTopology.lean
theorem interior_setOf_le_re (a : ℝ) : interior { z : ℂ | a ≤ z.re } = { z | a < z.re }

Proof state:
a : ℝ
⊢ interior {z | a ≤ z.re} = {z | a < z.re}

Tactic:
simpa only [interior_Ici] using interior_preimage_re (Ici a)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem DivModState.udiv_eq_of_lawful {n d : BitVec w} {qr : DivModState w}
    (h_lawful : DivModState.Lawful {n, d} qr)
    (h_final  : qr.wn = 0) :
    n / d = qr.q

Proof state:
w : Nat
n d : BitVec w
qr : DivModState w
h_lawful : Lawful { n := n, d := d } qr
h_final : qr.wn = 0
⊢ n / d = qr.q

Tactic:
apply udiv_eq_of_mul_add_toNat h_lawful.hdPos h_lawful.hrLtDivisor

Result:
w : Nat
n d : BitVec w
qr : DivModState w
h_lawful : Lawful { n := n, d := d } qr
h_final : qr.wn = 0
⊢ { n := n, d := d }.d.toNat * qr.q.toNat + qr.r.toNat = n.toNat

Proof state:
w : Nat
n d : BitVec w
qr : DivModState w
h_lawful : Lawful { n := n, d := d } qr
h_final : qr.wn = 0
hdiv : { n := n, d := d }.n.toNat >>> qr.wn = { n := n, d := d }.d.toNat * qr.q.toNat + qr.r.toNat
⊢ { n := n, d := d }.d.toNat * qr.q.toNat + qr.r.toNat = n.toNat

Tactic:
simp only [h_final] at *

Result:
w : Nat
n d : BitVec w
qr : DivModState w
h_lawful : Lawful { n := n, d := d } qr
h_final : True
hdiv : n.toNat >>> 0 = d.toNat * qr.q.toNat + qr.r.toNat
⊢ d.toNat * qr.q.toNat + qr.r.toNat = n.toNat

Proof state:
w : Nat
n d : BitVec w
qr : DivModState w
h_lawful : Lawful { n := n, d := d } qr
h_final : qr.wn = 0
⊢ { n := n, d := d }.d.toNat * qr.q.toNat + qr.r.toNat = n.toNat

Tactic:
have hdiv := h_lawful.hdiv

Result:
w : Nat
n d : BitVec w
qr : DivModState w
h_lawful : Lawful { n := n, d := d } qr
h_final : qr.wn = 0
hdiv : { n := n, d := d }.n.toNat >>> qr.wn = { n := n, d := d }.d.toNat * qr.q.toNat + qr.r.toNat
⊢ { n := n, d := d }.d.toNat * qr.q.toNat + qr.r.toNat = n.toNat

Proof state:
w : Nat
n d : BitVec w
qr : DivModState w
h_lawful : Lawful { n := n, d := d } qr
h_final : True
hdiv : n.toNat >>> 0 = d.toNat * qr.q.toNat + qr.r.toNat
⊢ d.toNat * qr.q.toNat + qr.r.toNat = n.toNat

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_extract_aux {as : Array α} {start stop : Nat} (h : i < (as.extract start stop).size) :
    start + i < as.size

Proof state:
case a.h
α : Type u_1
i : Nat
as : Array α
start stop : Nat
h : i < min stop as.size - start
⊢ min stop as.size ≤ as.size

Tactic:
apply Nat.min_le_right

Result:
no goals

Proof state:
α : Type u_1
i : Nat
as : Array α
start stop : Nat
h : i < (as.extract start stop).size
⊢ start + i < as.size

Tactic:
rw [size_extract] at h

Result:
α : Type u_1
i : Nat
as : Array α
start stop : Nat
h : i < min stop as.size - start
⊢ start + i < as.size

Proof state:
α : Type u_1
i : Nat
as : Array α
start stop : Nat
h : i < min stop as.size - start
⊢ start + i < as.size

Tactic:
apply Nat.add_lt_of_lt_sub'

Result:
case a
α : Type u_1
i : Nat
as : Array α
start stop : Nat
h : i < min stop as.size - start
⊢ i < as.size - start

Proof state:
case a
α : Type u_1
i : Nat
as : Array α
start stop : Nat
h : i < min stop as.size - start
⊢ i < as.size - start

Tactic:
apply Nat.lt_of_lt_of_le h

Result:
case a
α : Type u_1
i : Nat
as : Array α
start stop : Nat
h : i < min stop as.size - start
⊢ min stop as.size - start ≤ as.size - start

Proof state:
case a
α : Type u_1
i : Nat
as : Array α
start stop : Nat
h : i < min stop as.size - start
⊢ min stop as.size - start ≤ as.size - start

Tactic:
apply Nat.sub_le_sub_right

Result:
case a.h
α : Type u_1
i : Nat
as : Array α
start stop : Nat
h : i < min stop as.size - start
⊢ min stop as.size ≤ as.size
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem isEmpty_alterKey_eq_isEmpty_eraseKey {k : α} {f : Option β → Option β}
    {l : List ((_ : α) × β)} :
    (alterKey k f l).isEmpty = ((eraseKey k l).isEmpty && (f (getValue? k l)).isNone)

Proof state:
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
l : List ((_ : α) × β)
⊢ (alterKey k f l).isEmpty = ((eraseKey k l).isEmpty && (f (getValue? k l)).isNone)

Tactic:
simp only [alterKey, List.isEmpty_eq_true]

Result:
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
l : List ((_ : α) × β)
⊢ (match f (getValue? k l) with
      | none => eraseKey k l
      | some v => insertEntry k v l).isEmpty =
    ((eraseKey k l).isEmpty && (f (getValue? k l)).isNone)

Proof state:
case h_2
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
l : List ((_ : α) × β)
x✝ : Option β
v✝ : β
heq✝ : f (getValue? k l) = some v✝
⊢ (insertEntry k v✝ l).isEmpty = ((eraseKey k l).isEmpty && (f (getValue? k l)).isNone)

Tactic:
next heq => simp [heq]

Result:
no goals

Proof state:
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
l : List ((_ : α) × β)
⊢ (match f (getValue? k l) with
      | none => eraseKey k l
      | some v => insertEntry k v l).isEmpty =
    ((eraseKey k l).isEmpty && (f (getValue? k l)).isNone)

Tactic:
split <;> { next heq => simp [heq] }

Result:
no goals

Proof state:
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
l : List ((_ : α) × β)
x✝ : Option β
v✝ : β
heq : f (getValue? k l) = some v✝
⊢ (insertEntry k v✝ l).isEmpty = ((eraseKey k l).isEmpty && (f (getValue? k l)).isNone)

Tactic:
simp [heq]

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma pos_of_smul_pos_left [PosSMulReflectLT α β] (h : 0 < a • b) (ha : 0 ≤ a) : 0 < b :=
  lt_of_smul_lt_smul_left (by rwa [smul_zero]) ha

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulZeroClass α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : PosSMulReflectLT α β
h : 0 < a • b
ha : 0 ≤ a
⊢ a • 0 < a • b

Tactic:
rwa [smul_zero]

Result:
no goals
-- Mathlib/Topology/LocalAtTarget.lean
theorem IsClosedMap.restrictPreimage (H : IsClosedMap f) (s : Set β) :
    IsClosedMap (s.restrictPreimage f)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : IsClosedMap f
s : Set β
t : Set ↑(f ⁻¹' s)
u : Set α
hu : IsClosed u
e : Subtype.val ⁻¹' u = t
⊢ Subtype.val ⁻¹' (f '' u) = s.restrictPreimage f '' t

Tactic:
simp [← e, image_restrictPreimage]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : IsClosedMap f
s : Set β
t : Set ↑(f ⁻¹' s)
⊢ IsClosed t → IsClosed (s.restrictPreimage f '' t)

Tactic:
suffices ∀ u, IsClosed u → Subtype.val ⁻¹' u = t →
  ∃ v, IsClosed v ∧ Subtype.val ⁻¹' v = s.restrictPreimage f '' t by
    simpa [isClosed_induced_iff]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : IsClosedMap f
s : Set β
t : Set ↑(f ⁻¹' s)
⊢ ∀ (u : Set α), IsClosed u → Subtype.val ⁻¹' u = t → ∃ v, IsClosed v ∧ Subtype.val ⁻¹' v = s.restrictPreimage f '' t

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : IsClosedMap f
s : Set β
t : Set ↑(f ⁻¹' s)
⊢ ∀ (u : Set α), IsClosed u → Subtype.val ⁻¹' u = t → ∃ v, IsClosed v ∧ Subtype.val ⁻¹' v = s.restrictPreimage f '' t

Tactic:
exact fun u hu e => ⟨f '' u, H u hu, by simp [← e, image_restrictPreimage]⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : IsClosedMap f
s : Set β
⊢ IsClosedMap (s.restrictPreimage f)

Tactic:
intro t

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : IsClosedMap f
s : Set β
t : Set ↑(f ⁻¹' s)
⊢ IsClosed t → IsClosed (s.restrictPreimage f '' t)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : IsClosedMap f
s : Set β
t : Set ↑(f ⁻¹' s)
this :
  ∀ (u : Set α), IsClosed u → Subtype.val ⁻¹' u = t → ∃ v, IsClosed v ∧ Subtype.val ⁻¹' v = s.restrictPreimage f '' t
⊢ IsClosed t → IsClosed (s.restrictPreimage f '' t)

Tactic:
simpa [isClosed_induced_iff]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
/-- Let `F` be a semi-`NormedSpace` over a `NontriviallyNormedField`, and let `q` be a
seminorm on `F`. If `q` is continuous, then it is uniformly controlled by the norm, that is there
is some `C > 0` such that `∀ x, q x ≤ C * ‖x‖`.
The continuity ensures boundedness on a ball of some radius `ε`. The nontriviality of the
norm is then used to rescale any element into an element of norm in `[ε/C, ε[`, thus with a
controlled image by `q`. The control of `q` at the original element follows by rescaling. -/
lemma bound_of_continuous_normedSpace (q : Seminorm 𝕜 F)
    (hq : Continuous q) : ∃ C, 0 < C ∧ (∀ x : F, q x ≤ C * ‖x‖)

Proof state:
case neg
𝕜 : Type u_1
F : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
q : Seminorm 𝕜 F
hq : Continuous ⇑q
hq' : Tendsto (⇑q) (𝓝 0) (𝓝 0)
ε : ℝ
ε_pos : 0 < ε
hε : {y | ‖y‖ < ε} ⊆ ⇑q ⁻¹' Iio 1
c : 𝕜
hc : 1 < ‖c‖
this : 0 < ‖c‖ / ε
x✝ : F
hx : ¬‖x✝‖ = 0
x : F
hle : ε / ‖c‖ ≤ (normSeminorm 𝕜 F) x
hlt : (normSeminorm 𝕜 F) x < ε
⊢ q x ≤ ‖c‖ / ε * (normSeminorm 𝕜 F) x

Tactic:
refine (le_of_lt <| show q x < _ from hε hlt).trans ?_

Result:
case neg
𝕜 : Type u_1
F : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
q : Seminorm 𝕜 F
hq : Continuous ⇑q
hq' : Tendsto (⇑q) (𝓝 0) (𝓝 0)
ε : ℝ
ε_pos : 0 < ε
hε : {y | ‖y‖ < ε} ⊆ ⇑q ⁻¹' Iio 1
c : 𝕜
hc : 1 < ‖c‖
this : 0 < ‖c‖ / ε
x✝ : F
hx : ¬‖x✝‖ = 0
x : F
hle : ε / ‖c‖ ≤ (normSeminorm 𝕜 F) x
hlt : (normSeminorm 𝕜 F) x < ε
⊢ 1 ≤ ‖c‖ / ε * (normSeminorm 𝕜 F) x

Proof state:
case intro.intro.intro
𝕜 : Type u_1
F : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
q : Seminorm 𝕜 F
hq : Continuous ⇑q
hq' : Tendsto (⇑q) (𝓝 0) (𝓝 0)
ε : ℝ
ε_pos : 0 < ε
hε : {y | ‖y‖ < ε} ⊆ ⇑q ⁻¹' Iio 1
c : 𝕜
hc : 1 < ‖c‖
⊢ ∃ C, 0 < C ∧ ∀ (x : F), q x ≤ C * ‖x‖

Tactic:
have : 0 < ‖c‖ / ε := by positivity

Result:
case intro.intro.intro
𝕜 : Type u_1
F : Type u_6
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
q : Seminorm 𝕜 F
hq : Continuous ⇑q
hq' : Tendsto (⇑q) (𝓝 0) (𝓝 0)
ε : ℝ
ε_pos : 0 < ε
hε : {y | ‖y‖ < ε} ⊆ ⇑q ⁻¹' Iio 1
c : 𝕜
hc : 1 < ‖c‖
this : 0 < ‖c‖ / ε
⊢ ∃ C, 0 < C ∧ ∀ (x : F), q x ≤ C * ‖x‖
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Biproducts.lean
theorem biprod.mapBiprod_inv_map_desc (f : X ⟶ W) (g : Y ⟶ W) :
    (F.mapBiprod X Y).inv ≫ F.map (biprod.desc f g) = biprod.desc (F.map f) (F.map g)

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
X Y : C
inst✝¹ : HasBinaryBiproduct X Y
inst✝ : PreservesBinaryBiproduct X Y F
W : C
f : X ⟶ W
g : Y ⟶ W
⊢ (F.mapBiprod X Y).inv ≫ F.map (desc f g) = desc (F.map f) (F.map g)

Tactic:
ext <;> simp [mapBiprod, ← F.map_comp]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Matrix.lean
theorem toMatrix_mul_toMatrix : b.toMatrix b₂ * b₂.toMatrix b = 1

Proof state:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : Ring k
inst✝² : Module k V
b : AffineBasis ι k P
inst✝¹ : Fintype ι
b₂ : AffineBasis ι k P
inst✝ : DecidableEq ι
⊢ b.toMatrix ⇑b₂ * b₂.toMatrix ⇑b = 1

Tactic:
ext l m

Result:
case a
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : Ring k
inst✝² : Module k V
b : AffineBasis ι k P
inst✝¹ : Fintype ι
b₂ : AffineBasis ι k P
inst✝ : DecidableEq ι
l m : ι
⊢ (b.toMatrix ⇑b₂ * b₂.toMatrix ⇑b) l m = 1 l m

Proof state:
case a
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : Ring k
inst✝² : Module k V
b : AffineBasis ι k P
inst✝¹ : Fintype ι
b₂ : AffineBasis ι k P
inst✝ : DecidableEq ι
l m : ι
⊢ (b.toMatrix ⇑b₂ * b₂.toMatrix ⇑b) l m = 1 l m

Tactic:
change (b.coords (b₂ l) ᵥ* b₂.toMatrix b) m = _

Result:
case a
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : Ring k
inst✝² : Module k V
b : AffineBasis ι k P
inst✝¹ : Fintype ι
b₂ : AffineBasis ι k P
inst✝ : DecidableEq ι
l m : ι
⊢ (b.coords (b₂ l) ᵥ* b₂.toMatrix ⇑b) m = 1 l m

Proof state:
case a
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁵ : AddCommGroup V
inst✝⁴ : AffineSpace V P
inst✝³ : Ring k
inst✝² : Module k V
b : AffineBasis ι k P
inst✝¹ : Fintype ι
b₂ : AffineBasis ι k P
inst✝ : DecidableEq ι
l m : ι
⊢ (b.coords (b₂ l) ᵥ* b₂.toMatrix ⇑b) m = 1 l m

Tactic:
rw [toMatrix_vecMul_coords, coords_apply, ← toMatrix_apply, toMatrix_self]

Result:
no goals