mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁸ : Ring k
inst✝¹⁷ : AddCommGroup V₁
inst✝¹⁶ : AddCommGroup V₂
inst✝¹⁵ : AddCommGroup V₃
inst✝¹⁴ : AddCommGroup V₄
inst✝¹³ : Module k V₁
inst✝¹² : Module k V₂
inst✝¹¹ : Module k V₃
inst✝¹⁰ : Module k V₄
inst✝⁹ : AffineSpace V₁ P₁
inst✝⁸ : AffineSpace V₂ P₂
inst✝⁷ : AffineSpace V₃ P₃
inst✝⁶ : AffineSpace V₄ P₄
R : Type u_10
W : Type u_11
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module R W
inst✝¹ : SMulCommClass k R W
e : P₁ ≃ᵃ[k] P₂
Q : Type u_12
inst✝ : AffineSpace W Q
x✝¹ : P₁ →ᵃ[k] Q
x✝ : P₁ →ᵃ[k] W
p✝ : P₂
⊢ ((e.arrowCongrEquiv (refl k Q)) (x✝ +ᵥ x✝¹)) p✝ = ((congrLeftₗ R W e) x✝ +ᵥ (e.arrowCongrEquiv (refl k Q)) x✝¹) p✝

Tactic:
;

Goal state after:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁸ : Ring k
inst✝¹⁷ : AddCommGroup V₁
inst✝¹⁶ : AddCommGroup V₂
inst✝¹⁵ : AddCommGroup V₃
inst✝¹⁴ : AddCommGroup V₄
inst✝¹³ : Module k V₁
inst✝¹² : Module k V₂
inst✝¹¹ : Module k V₃
inst✝¹⁰ : Module k V₄
inst✝⁹ : AffineSpace V₁ P₁
inst✝⁸ : AffineSpace V₂ P₂
inst✝⁷ : AffineSpace V₃ P₃
inst✝⁶ : AffineSpace V₄ P₄
R : Type u_10
W : Type u_11
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module R W
inst✝¹ : SMulCommClass k R W
e : P₁ ≃ᵃ[k] P₂
Q : Type u_12
inst✝ : AffineSpace W Q
x✝¹ : P₁ →ᵃ[k] Q
x✝ : P₁ →ᵃ[k] W
p✝ : P₂
⊢ ((e.arrowCongrEquiv (refl k Q)) (x✝ +ᵥ x✝¹)) p✝ = ((congrLeftₗ R W e) x✝ +ᵥ (e.arrowCongrEquiv (refl k Q)) x✝¹) p✝
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case e'_4
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : CommRing 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : IsOrderedRing 𝕜
inst✝² : IsDomain 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
hs : s ≠ t
c : E
H : LinearIndependent 𝕜 ![-1 • x + t • y, -1 • x + s • y]
⊢ ![t • y - x, s • y - x] = ![-1 • x + t • y, -1 • x + s • y]

Tactic:
;

Goal state after:
case e'_4
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : CommRing 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : IsOrderedRing 𝕜
inst✝² : IsDomain 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
hs : s ≠ t
c : E
H : LinearIndependent 𝕜 ![-1 • x + t • y, -1 • x + s • y]
⊢ ![t • y - x, s • y - x] = ![-1 • x + t • y, -1 • x + s • y]
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case e'_4
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : CommRing 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : IsOrderedRing 𝕜
inst✝² : IsDomain 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
hs : s ≠ t
c : E
H : LinearIndependent 𝕜 ![-1 • x + t • y, -1 • x + s • y]
⊢ ![t • y - x, s • y - x] = ![-x + t • y, -x + s • y]

Tactic:
;

Goal state after:
case e'_4
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : CommRing 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : IsOrderedRing 𝕜
inst✝² : IsDomain 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y : E
h : LinearIndependent 𝕜 ![x, y]
s t : 𝕜
hs : s ≠ t
c : E
H : LinearIndependent 𝕜 ![-1 • x + t • y, -1 • x + s • y]
⊢ ![t • y - x, s • y - x] = ![-x + t • y, -x + s • y]
Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E
a b : 𝕜
f : E →ᵃ[𝕜] F
h : a + b = 1
⊢ f (a • x + b • y) = a • f x + b • f y

Tactic:
by
  simp only [Convex.combo_eq_smul_sub_add h, ← vsub_eq_sub]
  exact f.apply_lineMap _ _ _

Goal state after:
Module: Mathlib.Analysis.Convex.Segment

Goal state before:
pp: case left
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Semiring 𝕜
inst✝⁵ : PartialOrder 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : PartialOrder E
inst✝² : IsOrderedCancelAddMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : PosSMulStrictMono 𝕜 E
x y : E
h : x < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ x < a • x + b • y

Tactic:
calc
      x = a • x + b • x := (Convex.combo_self hab _).symm
      _ < a • x + b • y := by gcongr

Goal state after:
Module: Mathlib.Analysis.Convex.Star

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMulWithZero 𝕜 E
s : Set E
x : E
x✝ : x ∈ s
h : ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ b ≤ a + b

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : AddRightMono 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMulWithZero 𝕜 E
s : Set E
x : E
x✝ : x ∈ s
h : ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ b ≤ a + b
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: case mk
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
q : AffineSubspace k P
carrier✝ : Set P
smul_vsub_vadd_mem'✝ :
  ∀ (c : k) {p₁ p₂ p₃ : P}, p₁ ∈ carrier✝ → p₂ ∈ carrier✝ → p₃ ∈ carrier✝ → c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ carrier✝
x✝ : { carrier := carrier✝, smul_vsub_vadd_mem' := smul_vsub_vadd_mem'✝ }.carrier = q.carrier
⊢ { carrier := carrier✝, smul_vsub_vadd_mem' := smul_vsub_vadd_mem'✝ } = q

Tactic:
;

Goal state after:
case mk
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
q : AffineSubspace k P
carrier✝ : Set P
smul_vsub_vadd_mem'✝ :
  ∀ (c : k) {p₁ p₂ p₃ : P}, p₁ ∈ carrier✝ → p₂ ∈ carrier✝ → p₃ ∈ carrier✝ → c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ carrier✝
x✝ : { carrier := carrier✝, smul_vsub_vadd_mem' := smul_vsub_vadd_mem'✝ }.carrier = q.carrier
⊢ { carrier := carrier✝, smul_vsub_vadd_mem' := smul_vsub_vadd_mem'✝ } = q
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: case mk.mk
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
carrier✝¹ : Set P
smul_vsub_vadd_mem'✝¹ :
  ∀ (c : k) {p₁ p₂ p₃ : P}, p₁ ∈ carrier✝¹ → p₂ ∈ carrier✝¹ → p₃ ∈ carrier✝¹ → c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ carrier✝¹
carrier✝ : Set P
smul_vsub_vadd_mem'✝ :
  ∀ (c : k) {p₁ p₂ p₃ : P}, p₁ ∈ carrier✝ → p₂ ∈ carrier✝ → p₃ ∈ carrier✝ → c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ carrier✝
x✝ :
  { carrier := carrier✝¹, smul_vsub_vadd_mem' := smul_vsub_vadd_mem'✝¹ }.carrier =
    { carrier := carrier✝, smul_vsub_vadd_mem' := smul_vsub_vadd_mem'✝ }.carrier
⊢ { carrier := carrier✝¹, smul_vsub_vadd_mem' := smul_vsub_vadd_mem'✝¹ } =
    { carrier := carrier✝, smul_vsub_vadd_mem' := smul_vsub_vadd_mem'✝ }

Tactic:
;

Goal state after:
case mk.mk
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
carrier✝¹ : Set P
smul_vsub_vadd_mem'✝¹ :
  ∀ (c : k) {p₁ p₂ p₃ : P}, p₁ ∈ carrier✝¹ → p₂ ∈ carrier✝¹ → p₃ ∈ carrier✝¹ → c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ carrier✝¹
carrier✝ : Set P
smul_vsub_vadd_mem'✝ :
  ∀ (c : k) {p₁ p₂ p₃ : P}, p₁ ∈ carrier✝ → p₂ ∈ carrier✝ → p₃ ∈ carrier✝ → c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ carrier✝
x✝ :
  { carrier := carrier✝¹, smul_vsub_vadd_mem' := smul_vsub_vadd_mem'✝¹ }.carrier =
    { carrier := carrier✝, smul_vsub_vadd_mem' := smul_vsub_vadd_mem'✝ }.carrier
⊢ { carrier := carrier✝¹, smul_vsub_vadd_mem' := smul_vsub_vadd_mem'✝¹ } =
    { carrier := carrier✝, smul_vsub_vadd_mem' := smul_vsub_vadd_mem'✝ }
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : AffineSubspace k V
h : ↑s.direction = s
⊢ 0 ∈ ↑s.direction

Tactic:
;

Goal state after:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : AffineSubspace k V
h : ↑s.direction = s
⊢ 0 ∈ ↑s.direction
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : (↑s₁ ∩ ↑s₂).Nonempty
p : P
hq1 : hn.some ∈ ↑s₁
hq2 : hn.some ∈ ↑s₂
hp : p ∈ s₂
⊢ p -ᵥ hn.some ∈ s₁.direction

Tactic:
rw [hd]

Goal state after:
case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
hd : s₁.direction = s₂.direction
hn : (↑s₁ ∩ ↑s₂).Nonempty
p : P
hq1 : hn.some ∈ ↑s₁
hq2 : hn.some ∈ ↑s₂
hp : p ∈ s₂
⊢ p -ᵥ hn.some ∈ s₂.direction
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Submodule k V
x : V
⊢ x ∈ (↑s).direction ↔ x ∈ s

Tactic:
;

Goal state after:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Submodule k V
x : V
⊢ x ∈ (↑s).direction ↔ x ∈ s
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: case a
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₁ p₂ : P
hp₂ : p₂ ∈ s
v₁ : V
hv₁ : v₁ ∈ vectorSpan k s
hp₁ : p₁ = v₁ +ᵥ p₂
p₃ p₄ : P
hp₄ : p₄ ∈ s
v₂ : V
hv₂ : v₂ ∈ vectorSpan k s
hp₃ : p₃ = v₂ +ᵥ p₄
⊢ v₁ + (p₂ -ᵥ p₄) - v₂ ∈ vectorSpan k s

Tactic:
exact
      (vectorSpan k s).sub_mem ((vectorSpan k s).add_mem hv₁ (vsub_mem_vectorSpan k hp₂ hp₄)) hv₂

Goal state after:
Module: Mathlib.Analysis.Convex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h : Convex 𝕜 s
x y : E
p q : 𝕜
hx : x ∈ s
hy : y ∈ s
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ∃ z ∈ s, (p + q) • z = p • x + q • y

Tactic:
rcases _root_.em (p = 0 ∧ q = 0) with (⟨rfl, rfl⟩ | hpq)

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : y ∈ s
hp hq : 0 ≤ 0
⊢ ∃ z ∈ s, (0 + 0) • z = 0 • x + 0 • y

case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h : Convex 𝕜 s
x y : E
p q : 𝕜
hx : x ∈ s
hy : y ∈ s
hp : 0 ≤ p
hq : 0 ≤ q
hpq : ¬(p = 0 ∧ q = 0)
⊢ ∃ z ∈ s, (p + q) • z = p • x + q • y
Module: Mathlib.Analysis.Convex.Hull

Goal state before:
pp: case h₁
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : Ring 𝕜
inst✝⁴ : PartialOrder 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set E
⊢ ⇑f '' s ⊆ (convexHull 𝕜) (⇑f '' s)

Tactic:
exact subset_convexHull 𝕜 (f '' s)

Goal state after:
Module: Mathlib.Analysis.Convex.Hull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ (convexHull 𝕜) s ⊆ ↑(affineSpan 𝕜 s)

Tactic:
exact convexHull_subset_affineSpan s

Goal state after:
Module: Mathlib.Topology.Bornology.Absorbs

Goal state before:
pp: M : Type u_1
E : Type u_2
inst✝² : Bornology M
s₁ s₂ t₁ t₂ : Set E
inst✝¹ : AddZeroClass E
inst✝ : DistribSMul M E
h₁ : Absorbs M s₁ t₁
h₂ : Absorbs M s₂ t₂
x : M
hx₁ : t₁ ⊆ x • s₁
hx₂ : t₂ ⊆ x • s₂
⊢ t₁ + t₂ ⊆ x • s₁ + x • s₂

Tactic:
;

Goal state after:
M : Type u_1
E : Type u_2
inst✝² : Bornology M
s₁ s₂ t₁ t₂ : Set E
inst✝¹ : AddZeroClass E
inst✝ : DistribSMul M E
h₁ : Absorbs M s₁ t₁
h₂ : Absorbs M s₂ t₂
x : M
hx₁ : t₁ ⊆ x • s₁
hx₂ : t₂ ⊆ x • s₂
⊢ t₁ + t₂ ⊆ x • s₁ + x • s₂
Module: Mathlib.Topology.Bornology.Absorbs

Goal state before:
pp: G₀ : Type u_1
α : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : Bornology G₀
inst✝ : MulAction G₀ α
s : Set α
a : G₀
ha : a ≠ 0
⊢ s ⊆ univ

Tactic:
;

Goal state after:
G₀ : Type u_1
α : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : Bornology G₀
inst✝ : MulAction G₀ α
s : Set α
a : G₀
ha : a ≠ 0
⊢ s ⊆ univ
Module: Mathlib.Topology.Bornology.Absorbs

Goal state before:
pp: G₀ : Type u_1
α : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : Bornology G₀
inst✝ : MulAction G₀ α
s t : Set α
c : G₀
hc : c ≠ 0
⊢ t ⊆ (fun x ↦ c⁻¹ • x) ⁻¹' s ↔ MapsTo (fun x ↦ c⁻¹ • x) t s

Tactic:
;

Goal state after:
G₀ : Type u_1
α : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : Bornology G₀
inst✝ : MulAction G₀ α
s t : Set α
c : G₀
hc : c ≠ 0
⊢ t ⊆ (fun x ↦ c⁻¹ • x) ⁻¹' s ↔ MapsTo (fun x ↦ c⁻¹ • x) t s
Module: Mathlib.Topology.Bornology.Absorbs

Goal state before:
pp: M : Type u_1
E : Type u_2
inst✝² : Bornology M
inst✝¹ : AddZeroClass E
inst✝ : DistribSMul M E
s₁ s₂ t : Set E
x : E
h₁ : Absorbent M s₁
h₂ : Absorbs M s₂ t
⊢ Absorbs M (s₁ + s₂) ({x} +ᵥ t)

Tactic:
;

Goal state after:
M : Type u_1
E : Type u_2
inst✝² : Bornology M
inst✝¹ : AddZeroClass E
inst✝ : DistribSMul M E
s₁ s₂ t : Set E
x : E
h₁ : Absorbent M s₁
h₂ : Absorbs M s₂ t
⊢ Absorbs M (s₁ + s₂) ({x} +ᵥ t)
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
p : P
h₁ : p ∈ s₁
h₂ : p ∈ s₂
v : V
⊢ v ∈ (s₁ ⊓ s₂).direction ↔ v ∈ s₁.direction ⊓ s₂.direction

Tactic:
rw [Submodule.mem_inf, ← vadd_mem_iff_mem_direction v h₁, ← vadd_mem_iff_mem_direction v h₂, ←
    vadd_mem_iff_mem_direction v ((mem_inf_iff p s₁ s₂).2 ⟨h₁, h₂⟩), mem_inf_iff]

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
A B : Set E
⊢ (∃ i, ∀ ⦃x : 𝕜⦄, x ∈ norm ⁻¹' Ici i → B ⊆ x • A) ↔ ∃ r, ∀ (c : 𝕜), r ≤ ‖c‖ → B ⊆ c • A

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
A B : Set E
⊢ (∃ i, ∀ ⦃x : 𝕜⦄, x ∈ norm ⁻¹' Ici i → B ⊆ x • A) ↔ ∃ r, ∀ (c : 𝕜), r ≤ ‖c‖ → B ⊆ c • A
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Sort u_4
s : ι → AffineSubspace k P
p : P
⊢ p ∈ iInf s ↔ ∀ (i : ι), p ∈ s i

Tactic:
rw [iInf, mem_sInf_iff, Set.forall_mem_range]

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
⊢ (∀ᶠ (c : 𝕜) in Bornology.cobounded 𝕜, MapsTo (fun x ↦ c⁻¹ • x) t s) ↔
    ∀ᶠ (c : 𝕜) in (Bornology.cobounded 𝕜)⁻¹, MapsTo (fun x ↦ c • x) t s

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
⊢ (∀ᶠ (c : 𝕜) in Bornology.cobounded 𝕜, MapsTo (fun x ↦ c⁻¹ • x) t s) ↔
    ∀ᶠ (c : 𝕜) in (Bornology.cobounded 𝕜)⁻¹, MapsTo (fun x ↦ c • x) t s
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s
h : a ≠ 0
⊢ ∀ (r : 𝕜), 1 ≤ ‖r‖ → (fun x ↦ a • x) y ∈ r • s

Tactic:
intro r

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s
h : a ≠ 0
r : 𝕜
⊢ 1 ≤ ‖r‖ → (fun x ↦ a • x) y ∈ r • s
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
a : 𝕜
hs : Balanced 𝕜 s
ha : ‖1‖ ≤ ‖a‖
⊢ s ⊆ a • s

Tactic:
;

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
a : 𝕜
hs : Balanced 𝕜 s
ha : ‖1‖ ≤ ‖a‖
⊢ s ⊆ a • s
Module: Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : AffineSubspace k P
⊢ affineSpan k ↑s = s

Tactic:
refine le_antisymm ?_ (subset_affineSpan _ _)

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : AffineSubspace k P
⊢ affineSpan k ↑s ≤ s
Module: Mathlib.Analysis.LocallyConvex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : PartialOrder 𝕜
hs : Balanced 𝕜 s
x : E
hx : x ∈ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ (convexHull 𝕜) s}
y : E
hy : y ∈ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ (convexHull 𝕜) s}
u v : 𝕜
hu : 0 ≤ u
hv : 0 ≤ v
huv : u + v = 1
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ u • a • x + a • v • y ∈ (convexHull 𝕜) s

Tactic:
← smul_comm v

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : PartialOrder 𝕜
hs : Balanced 𝕜 s
x : E
hx : x ∈ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ (convexHull 𝕜) s}
y : E
hy : y ∈ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ (convexHull 𝕜) s}
u v : 𝕜
hu : 0 ≤ u
hv : 0 ≤ v
huv : u + v = 1
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ u • a • x + v • a • y ∈ (convexHull 𝕜) s
Module: Mathlib.Analysis.LocallyConvex.BalancedCoreHull

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedDivisionRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
U : Set E
inst✝ : (𝓝[≠] 0).NeBot
hU : U ∈ 𝓝 0
r : ℝ
V : Set E
hr : 0 < r
hV : V ∈ 𝓝 0
hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
⊢ balancedCore 𝕜 U ∈ 𝓝 0

Tactic:
obtain ⟨y, hyr, hy₀⟩ : ∃ y : 𝕜, ‖y‖ < r ∧ y ≠ 0 :=
    Filter.nonempty_of_mem <|
      (nhdsWithin_hasBasis NormedAddGroup.nhds_zero_basis_norm_lt {0}ᶜ).mem_of_mem hr

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedDivisionRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
U : Set E
inst✝ : (𝓝[≠] 0).NeBot
hU : U ∈ 𝓝 0
r : ℝ
V : Set E
hr : 0 < r
hV : V ∈ 𝓝 0
hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
y : 𝕜
hyr : ‖y‖ < r
hy₀ : y ≠ 0
⊢ balancedCore 𝕜 U ∈ 𝓝 0
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: 𝕜 : Type u_6
ι : Type u_7
E : ι → Type u_8
inst✝³ : NormedDivisionRing 𝕜
inst✝² : (i : ι) → AddCommGroup (E i)
inst✝¹ : (i : ι) → Module 𝕜 (E i)
inst✝ : (i : ι) → TopologicalSpace (E i)
S : Set ((i : ι) → E i)
⊢ Tendsto (fun x ↦ x • S) (𝓝 0) (⨅ i, comap (image (eval i)) (𝓝 (0 i)).smallSets) ↔
    ∀ (i : ι), Tendsto (fun x ↦ x • eval i '' S) (𝓝 0) (𝓝 0).smallSets

Tactic:
tendsto_iInf,

Goal state after:
𝕜 : Type u_6
ι : Type u_7
E : ι → Type u_8
inst✝³ : NormedDivisionRing 𝕜
inst✝² : (i : ι) → AddCommGroup (E i)
inst✝¹ : (i : ι) → Module 𝕜 (E i)
inst✝ : (i : ι) → TopologicalSpace (E i)
S : Set ((i : ι) → E i)
⊢ (∀ (i : ι), Tendsto (fun x ↦ x • S) (𝓝 0) (comap (image (eval i)) (𝓝 (0 i)).smallSets)) ↔
    ∀ (i : ι), Tendsto (fun x ↦ x • eval i '' S) (𝓝 0) (𝓝 0).smallSets
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
t : Set E
⊢ IsVonNBounded 𝕜 (∅ + t) ↔ ∅ = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 ∅ ∧ IsVonNBounded 𝕜 t

pp: case inr
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : s.Nonempty
⊢ IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Tactic:
;

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
t : Set E
⊢ IsVonNBounded 𝕜 (∅ + t) ↔ ∅ = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 ∅ ∧ IsVonNBounded 𝕜 t

case inr
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : s.Nonempty
⊢ IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t
Module: Mathlib.Analysis.LocallyConvex.Bounded

Goal state before:
pp: case inr.inl
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s : Set E
hs : s.Nonempty
⊢ IsVonNBounded 𝕜 (s + ∅) ↔ s = ∅ ∨ ∅ = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 ∅

pp: case inr.inr
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : s.Nonempty
ht : t.Nonempty
⊢ IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Tactic:
;

Goal state after:
case inr.inl
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s : Set E
hs : s.Nonempty
⊢ IsVonNBounded 𝕜 (s + ∅) ↔ s = ∅ ∨ ∅ = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 ∅

case inr.inr
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : s.Nonempty
ht : t.Nonempty
⊢ IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t
Module: Mathlib.Topology.Algebra.Equicontinuity

Goal state before:
pp: ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁷ : TopologicalSpace G
inst✝⁶ : UniformSpace M
inst✝⁵ : Group G
inst✝⁴ : Group M
inst✝³ : IsTopologicalGroup G
inst✝² : IsUniformGroup M
inst✝¹ : FunLike hom G M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F)) 1
⊢ swap (DFunLike.coe ∘ F) 1 = 1

Tactic:
;

Goal state after:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁷ : TopologicalSpace G
inst✝⁶ : UniformSpace M
inst✝⁵ : Group G
inst✝⁴ : Group M
inst✝³ : IsTopologicalGroup G
inst✝² : IsUniformGroup M
inst✝¹ : FunLike hom G M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F)) 1
⊢ swap (DFunLike.coe ∘ F) 1 = 1
Module: Mathlib.Topology.Algebra.Equicontinuity

Goal state before:
pp: ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁷ : TopologicalSpace G
inst✝⁶ : UniformSpace M
inst✝⁵ : Group G
inst✝⁴ : Group M
inst✝³ : IsTopologicalGroup G
inst✝² : IsUniformGroup M
inst✝¹ : FunLike hom G M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F)) 1
x✝ : ι
⊢ swap (DFunLike.coe ∘ F) 1 x✝ = 1 x✝

Tactic:
;

Goal state after:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁷ : TopologicalSpace G
inst✝⁶ : UniformSpace M
inst✝⁵ : Group G
inst✝⁴ : Group M
inst✝³ : IsTopologicalGroup G
inst✝² : IsUniformGroup M
inst✝¹ : FunLike hom G M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F)) 1
x✝ : ι
⊢ swap (DFunLike.coe ∘ F) 1 x✝ = 1 x✝
Module: Mathlib.Topology.Algebra.Equicontinuity

Goal state before:
pp: ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁷ : TopologicalSpace G
inst✝⁶ : UniformSpace M
inst✝⁵ : Group G
inst✝⁴ : Group M
inst✝³ : IsTopologicalGroup G
inst✝² : IsUniformGroup M
inst✝¹ : FunLike hom G M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F)) 1
a b : G
⊢ swap (DFunLike.coe ∘ F) (a * b) = swap (DFunLike.coe ∘ F) a * swap (DFunLike.coe ∘ F) b

Tactic:
;

Goal state after:
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁷ : TopologicalSpace G
inst✝⁶ : UniformSpace M
inst✝⁵ : Group G
inst✝⁴ : Group M
inst✝³ : IsTopologicalGroup G
inst✝² : IsUniformGroup M
inst✝¹ : FunLike hom G M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (⇑UniformFun.ofFun ∘ swap (DFunLike.coe ∘ F)) 1
a b : G
⊢ swap (DFunLike.coe ∘ F) (a * b) = swap (DFunLike.coe ∘ F) a * swap (DFunLike.coe ∘ F) b