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

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
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i0 : ι
⊢ vectorSpan k (range p) = Submodule.span k (range fun i ↦ p i0 -ᵥ p i)

Tactic:
by
  rw [vectorSpan_eq_span_vsub_set_left k (Set.mem_range_self i0), ← Set.range_comp]
  congr

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type u_5
𝕝 : Type u_6
E : Type u_7
E₂ : Type u_8
E₃ : Type u_9
F : Type u_10
ι : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p q : Seminorm 𝕜 E
x : E
s : Set (Seminorm 𝕜 E)
h : BddAbove (DFunLike.coe '' s)
i : ↑s
⊢ ↑i 0 = 0

Tactic:
exact map_zero i.1

Goal state after:
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case refine_2
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : p x ≠ 0
xεpos : 0 < p x / ε
n : ℤ
hn : p x / ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
⊢ ‖c ^ (-(n + 1))‖ * p x < ε

Tactic:
zpow_neg,

Goal state after:
case refine_2
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : p x ≠ 0
xεpos : 0 < p x / ε
n : ℤ
hn : p x / ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
⊢ ‖(c ^ (n + 1))⁻¹‖ * p x < ε
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case refine_3
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : p x ≠ 0
xεpos : 0 < p x / ε
n : ℤ
hn : p x / ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
⊢ ε / ‖c‖ ≤ p (c ^ (-(n + 1)) • x)

Tactic:
zpow_neg,

Goal state after:
case refine_3
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : p x ≠ 0
xεpos : 0 < p x / ε
n : ℤ
hn : p x / ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
⊢ ε / ‖c‖ ≤ p ((c ^ (n + 1))⁻¹ • x)
Module: Mathlib.Analysis.Seminorm

Goal state before:
pp: case refine_4
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : p x ≠ 0
xεpos : 0 < p x / ε
n : ℤ
hn : p x / ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
this : ε⁻¹ * ‖c‖ * p x = ε⁻¹ * p x * ‖c‖
⊢ ‖c ^ (-(n + 1))‖⁻¹ ≤ ε⁻¹ * ‖c‖ * p x

Tactic:
zpow_neg,

Goal state after:
case refine_4
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ
εpos : 0 < ε
x : E
hx : p x ≠ 0
xεpos : 0 < p x / ε
n : ℤ
hn : p x / ε ∈ Ico (‖c‖ ^ n) (‖c‖ ^ (n + 1))
cpos : 0 < ‖c‖
cnpos : 0 < ‖c ^ (n + 1)‖
this : ε⁻¹ * ‖c‖ * p x = ε⁻¹ * p x * ‖c‖
⊢ ‖(c ^ (n + 1))⁻¹‖⁻¹ ≤ ε⁻¹ * ‖c‖ * p x
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
I : Set k
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
p : P
⊢ p ∈ Simplex.setInterior I (s.reindex e) ↔ p ∈ Simplex.setInterior I s

Tactic:
refine ⟨fun ⟨w, hw, hwI, h⟩ ↦ ?_, fun ⟨w, hw, hwI, h⟩ ↦ ?_⟩

Goal state after:
case refine_1
k : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
I : Set k
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
p : P
x✝ : p ∈ Simplex.setInterior I (s.reindex e)
w : Fin (m + 1) → k
hw : ∑ i, w i = 1
hwI : ∀ (i : Fin (m + 1)), w i ∈ I
h : (affineCombination k univ (s.reindex e).points) w = p
⊢ p ∈ Simplex.setInterior I s

case refine_2
k : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
I : Set k
m n : ℕ
s : Simplex k P n
e : Fin (n + 1) ≃ Fin (m + 1)
p : P
x✝ : p ∈ Simplex.setInterior I s
w : Fin (n + 1) → k
hw : ∑ i, w i = 1
hwI : ∀ (i : Fin (n + 1)), w i ∈ I
h : (affineCombination k univ s.points) w = p
⊢ p ∈ Simplex.setInterior I (s.reindex e)
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x✝¹ x✝ : ι
⊢ Pi.single x✝¹ 1 x✝ = if x✝¹ = x✝ then 1 else 0

Tactic:
aesop

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Set E
hs : s.Finite
this : Fintype ↑s := ⋯
⊢ s = range (⇑(∑ x, (LinearMap.proj x).smulRight ↑x) ∘ fun i j ↦ if i = j then 1 else 0)

Tactic:
aesop

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

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
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
⊢ Injective fun s ↦ affineSpan k (p '' s)

Tactic:
by
  by_contra hn
  rw [not_injective_iff] at hn
  obtain ⟨s₁, s₂, hs₁₂, hne⟩ := hn
  apply hne
  ext i
  simp_rw [← ha.mem_affineSpan_iff, hs₁₂]

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

Goal state before:
pp: S : Type u_1
inst✝⁴ : Semiring S
inst✝³ : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : Fintype X
inst✝¹ : Fintype Y
inst✝ : Fintype Z
⊢ Function.Injective fun s ↦ ↑s

Tactic:
aesop

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

Goal state before:
pp: S : Type u_1
inst✝⁴ : Semiring S
inst✝³ : PartialOrder S
X : Type u_2
Y : Type u_3
inst✝² : Fintype X
inst✝¹ : Fintype Y
inst✝ : IsOrderedRing S
f : X → Y
s : X → S
hs₀ : ∀ (x : X), 0 ≤ s x
hs₁ : ∑ x, s x = 1
y : Y
⊢ ∀ i ∈ {x | f x = y}, 0 ≤ s i

Tactic:
aesop

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

Goal state before:
pp: S : Type u_1
inst✝⁵ : Semiring S
inst✝⁴ : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : Fintype X
inst✝² : Fintype Y
inst✝¹ : Fintype Z
inst✝ : IsOrderedRing S
f : X → Y
s : ↑(stdSimplex S X)
⊢ (FunOnFinite.linearMap S S f) ⇑s ∈ ⇑(FunOnFinite.linearMap S S f) '' stdSimplex S X

Tactic:
aesop

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

Goal state before:
pp: S : Type u_1
inst✝³ : Semiring S
inst✝² : PartialOrder S
X : Type u_2
inst✝¹ : Fintype X
inst✝ : IsOrderedRing S
x : ↑(stdSimplex S X)
⊢ map id x = x

Tactic:
aesop

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

Goal state before:
pp: S : Type u_1
inst✝⁶ : Semiring S
inst✝⁵ : PartialOrder S
X : Type u_2
Y : Type u_3
inst✝⁴ : Fintype X
inst✝³ : Fintype Y
inst✝² : IsOrderedRing S
inst✝¹ : DecidableEq X
inst✝ : DecidableEq Y
f : X → Y
x : X
⊢ map f (vertex x) = vertex (f x)

Tactic:
aesop

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

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
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : s₁.Nontrivial
j : ι
hj : j ∈ s₁
hne : j ≠ i
he : vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)
fs : Finset ↑s₂
w : ↑s₂ → k
hw : ∑ i ∈ fs, w i = 0
hs : p i -ᵥ p j = (fs.weightedVSub fun x ↦ p ↑x) w
w' : ι → k := extend Subtype.val w 0
hw' : ∑ t ∈ map (Embedding.subtype fun x ↦ x ∈ s₂) fs, w' t = 0
hs' : p i -ᵥ p j = ((map (Embedding.subtype fun x ↦ x ∈ s₂) fs).weightedVSub p) w'
fs' : Finset ι := insert i (insert j (map (Embedding.subtype fun x ↦ x ∈ s₂) fs))
hfsfs' : map (Embedding.subtype fun x ↦ x ∈ s₂) fs ⊆ fs'
w'' : ι → k := (↑(map (Embedding.subtype fun x ↦ x ∈ s₂) fs)).indicator w'
⊢ False

Tactic:
have hs'' : p i -ᵥ p j = fs'.weightedVSub p w'' := by
    rw [hs']
    exact weightedVSubOfPoint_indicator_subset _ _ _ (by grind)

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
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
i : ι
his₁ : i ∈ s₁
his₂ : i ∉ s₂
h₁ : s₁.Nontrivial
j : ι
hj : j ∈ s₁
hne : j ≠ i
he : vectorSpan k (p '' s₁) = vectorSpan k (p '' s₂)
fs : Finset ↑s₂
w : ↑s₂ → k
hw : ∑ i ∈ fs, w i = 0
hs : p i -ᵥ p j = (fs.weightedVSub fun x ↦ p ↑x) w
w' : ι → k := extend Subtype.val w 0
hw' : ∑ t ∈ map (Embedding.subtype fun x ↦ x ∈ s₂) fs, w' t = 0
hs' : p i -ᵥ p j = ((map (Embedding.subtype fun x ↦ x ∈ s₂) fs).weightedVSub p) w'
fs' : Finset ι := insert i (insert j (map (Embedding.subtype fun x ↦ x ∈ s₂) fs))
hfsfs' : map (Embedding.subtype fun x ↦ x ∈ s₂) fs ⊆ fs'
w'' : ι → k := (↑(map (Embedding.subtype fun x ↦ x ∈ s₂) fs)).indicator w'
hs'' : p i -ᵥ p j = (fs'.weightedVSub p) w''
⊢ False
Module: Mathlib.Analysis.Convex.StdSimplex

Goal state before:
pp: S : Type u_1
inst✝⁶ : Semiring S
inst✝⁵ : PartialOrder S
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : Fintype X
inst✝³ : Fintype Y
inst✝² : Fintype Z
inst✝¹ : IsOrderedRing S
inst✝ : Unique X
⊢ ∀ (a : ↑(stdSimplex S X)), a = ⟨1, ⋯⟩

Tactic:
by subsingleton

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

Goal state before:
pp: S : Type u_1
inst✝⁴ : Semiring S
inst✝³ : PartialOrder S
X : Type u_2
inst✝² : Fintype X
inst✝¹ : IsOrderedRing S
inst✝ : Unique X
s : ↑(stdSimplex S X)
x : X
⊢ s = default

Tactic:
by subsingleton

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

Goal state before:
pp: R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : Field R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
t : Finset ι
w : ι → R
z : ι → E
w' : ι → R
h : ∀ i ∈ t, w i = w' i
⊢ t.centerMass w z = t.centerMass w' z

Tactic:
classical
  exact centerMass_congr (by grind)

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

Goal state before:
pp: R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : Field R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
t : Finset ι
w : ι → R
z z' : ι → E
h : ∀ i ∈ t, w i ≠ 0 → z i = z' i
⊢ t.centerMass w z = t.centerMass w z'

Tactic:
classical
  exact centerMass_congr (by grind)

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: case pos
k : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : PartialOrder k
inst✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw1 : ∑ i, w i = 1
hp : (∀ i ∈ fs, w i ∈ Set.Icc 0 1) ∧ ∀ i ∉ fs, w i = 0
hp' : (affineCombination k univ s.points) w ∈ affineSpan k (Set.range s.points)
i : Fin (n + 1)
hi : i ∈ fs
⊢ w i ∈ Set.Icc 0 1

Tactic:
aesop

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Goal state before:
pp: case neg
k : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : PartialOrder k
inst✝ : ZeroLEOneClass k
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
w : Fin (n + 1) → k
hw1 : ∑ i, w i = 1
hp : (∀ i ∈ fs, w i ∈ Set.Icc 0 1) ∧ ∀ i ∉ fs, w i = 0
hp' : (affineCombination k univ s.points) w ∈ affineSpan k (Set.range s.points)
i : Fin (n + 1)
hi : i ∉ fs
⊢ w i ∈ Set.Icc 0 1

Tactic:
aesop

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: case inr.refine_2.hd
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
b : Set V
hb₁ : b ⊆ ⇑(Equiv.vaddConst p).symm '' s
hb₂ : Submodule.span k b = vectorSpan k s
hb₃ : AffineIndependent k fun p_1 ↦ ↑p_1
hb₀ : ∀ v ∈ b, v ≠ 0
⊢ (affineSpan k ({p} ∪ ⇑(Equiv.vaddConst p) '' b)).direction = (affineSpan k s).direction

Tactic:
have : Submodule.span k b = Submodule.span k (insert 0 b) := by simp
      simp only [direction_affineSpan, ← hb₂, Equiv.coe_vaddConst, Set.singleton_union,
        vectorSpan_eq_span_vsub_set_right k (Set.mem_insert p _), this]
      congr
      change (Equiv.vaddConst p).symm '' insert p (Equiv.vaddConst p '' b) = _
      rw [Set.image_insert_eq, ← Set.image_comp]
      simp

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

Goal state before:
pp: case refine_2.refine_1
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
i : ι
⊢ 0 ≤ W i

Tactic:
by_cases hi : i ∈ s

Goal state after:
case pos
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
i : ι
hi : i ∈ s
⊢ 0 ≤ W i

case neg
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
v : ι → E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
s' : Finset ι
w' : ι → R
hw₀' : ∀ i ∈ s', 0 ≤ w' i
hw₁' : s'.sum w' = 1
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
W : ι → R := fun i ↦ (if i ∈ s then a * w i else 0) + if i ∈ s' then b * w' i else 0
hW₁ : (s ∪ s').sum W = 1
i : ι
hi : i ∉ s
⊢ 0 ≤ W i
Module: Mathlib.Topology.Connected.LocallyPathConnected

Goal state before:
pp: case neg
ι : Type u_3
Z : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (Z i)
inst✝ : ∀ (i : ι), LocallyPathConnectedSpace (Z i)
hfinite : {i | ¬PathConnectedSpace (Z i)}.Finite
x : (i : ι) → Z i
U : Set ((i : ι) → Z i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (Z i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PathConnectedSpace (Z i)}
i : ι
hi : i ∉ K
⊢ IsPathConnected (K.piecewise (fun i ↦ pathComponentIn (t i) (x i)) (fun x ↦ univ) i)

Tactic:
· rw [piecewise_eq_of_notMem _ _ _ hi]
      have : PathConnectedSpace (Z i) := not_not.mp (not_or.1 hi).2
      exact isPathConnected_univ

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : DecidableEq ι
p : ι → P
ha : AffineIndependent k p
i : ι
p₀ : P
hp₀ : p₀ ∉ affineSpan k (p '' {x | x ≠ i})
f : ι → P := update p i p₀
hf : f = update p i p₀
x : ↑{x | x ≠ i}
⊢ p ↑x = f ↑x

Tactic:
aesop

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Independent

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
ι : Type u_4
inst✝ : DecidableEq ι
p : ι → P
i : ι
p₀ : P
hp₀ : p₀ ∉ affineSpan k (p '' {x | x ≠ i})
f : ι → P := update p i p₀
hf : f = update p i p₀
h₁ : (fun x ↦ p ↑x) = fun x ↦ f ↑x
h₂ : p '' {x | x ≠ i} = f '' {x | x ≠ i}
ha : AffineIndependent k fun x ↦ f ↑x
⊢ f i ∉ affineSpan k (f '' {x | x ≠ i})

Tactic:
aesop

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

Goal state before:
pp: case refine_1
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
i : ι
⊢ 0 ≤ (b.coord i) ((affineCombination R s ⇑b) w)

Tactic:
by_cases hi : i ∈ s

Goal state after:
case pos
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
i : ι
hi : i ∈ s
⊢ 0 ≤ (b.coord i) ((affineCombination R s ⇑b) w)

case neg
R : Type u_1
E : Type u_3
inst✝⁴ : Field R
inst✝³ : AddCommGroup E
inst✝² : Module R E
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
ι : Type u_8
b : AffineBasis ι R E
s : Finset ι
w : ι → R
hw₀ : ∀ i ∈ s, 0 ≤ w i
hw₁ : s.sum w = 1
i : ι
hi : i ∉ s
⊢ 0 ≤ (b.coord i) ((affineCombination R s ⇑b) w)
Module: Mathlib.Analysis.Convex.Combination

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Finite ι
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
s : Set ι
t✝ : (i : ι) → Set (E i)
x : (i : ι) → E i
val✝ : Fintype ι
t : (i : ι) → Set (E i)
κ : ι → Type
x✝ : (i : ι) → Fintype (κ i)
w : (i : ι) → κ i → 𝕜
f : (i : ι) → κ i → E i
hw₀ : ∀ (i : ι) (i_1 : κ i), 0 ≤ w i i_1
hw₁ : ∀ (i : ι), ∑ i_1, w i i_1 = 1
hft : ∀ (i : ι) (i_1 : κ i), f i i_1 ∈ t i
hf : ∀ (i : ι), ∑ i_1, w i i_1 • f i i_1 = x i
i : ι
j : κ i
a✝ : j ∈ Finset.univ
⊢ ∀ a ∈ Finset.univ, ↑a ∈ piFinset fun k ↦ if hk : k = i then ⋯ ▸ {j} else Finset.univ

Tactic:
aesop

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

Goal state before:
pp: case pos
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
hw' : ∀ i ∈ u, w i ≤ 1
hw1' : ∑ i, (↑u).indicator w i = 1
i : Fin (n + 1)
hi : i ∈ ↑u
⊢ (↑u).indicator w i ∈ Icc 0 1

Tactic:
aesop

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

Goal state before:
pp: case neg
𝕜 : Type u_1
V : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsOrderedRing 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
n : ℕ
s : Simplex 𝕜 V n
u : Finset (Fin (n + 1))
w : Fin (n + 1) → 𝕜
hw : ∀ i ∈ u, 0 ≤ w i
hw1 : u.sum w = 1
hw' : ∀ i ∈ u, w i ≤ 1
hw1' : ∑ i, (↑u).indicator w i = 1
i : Fin (n + 1)
hi : i ∉ ↑u
⊢ (↑u).indicator w i ∈ Icc 0 1

Tactic:
aesop

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

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
inst✝ : T1Space E
hp : WithSeminorms p
x : E
hx : x ≠ 0
this : ∀ ⦃x y : E⦄, x ⤳ y → x = y
h : ∀ (i : ι), (p i) x = 0
⊢ False

Tactic:
refine hx (this ?_)

Goal state after:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
inst✝ : T1Space E
hp : WithSeminorms p
x : E
hx : x ≠ 0
this : ∀ ⦃x y : E⦄, x ⤳ y → x = y
h : ∀ (i : ι), (p i) x = 0
⊢ x ⤳ 0
Module: Mathlib.Analysis.LocallyConvex.WithSeminorms

Goal state before:
pp: case mp
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
i : ι
⊢ (∃ r > 0, ∀ x ∈ s, (p i) x < r) → ∃ x, ∀ ⦃x_1 : E⦄, x_1 ∈ s → (p i) x_1 ≤ x

pp: case mpr
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
i : ι
⊢ (∃ x, ∀ ⦃x_1 : E⦄, x_1 ∈ s → (p i) x_1 ≤ x) → ∃ r > 0, ∀ x ∈ s, (p i) x < r

Tactic:
· rintro ⟨r, _⟩
    use r
    grind

Goal state after:
case mpr
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
i : ι
⊢ (∃ x, ∀ ⦃x_1 : E⦄, x_1 ∈ s → (p i) x_1 ≤ x) → ∃ r > 0, ∀ x ∈ s, (p i) x < r
Module: Mathlib.Topology.UniformSpace.CompactConvergence

Goal state before:
pp: α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
s : Set α
inst✝ : CompactSpace ↑s
f : α → β
hf : ContinuousOn f s
ι : Type u_1
p : Filter ι
F : ι → α → β
hF : ∀ (i : ι), ContinuousOn (F i) s
⊢ TendstoUniformly (fun i a ↦ { toFun := s.domRestrict (F i), continuous_toFun := ⋯ } a)
      (⇑{ toFun := s.domRestrict f, continuous_toFun := ⋯ }) p ↔
    TendstoUniformlyOn F f p s

Tactic:
tendstoUniformlyOn_iff_tendstoUniformly_comp_coe

Goal state after:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
s : Set α
inst✝ : CompactSpace ↑s
f : α → β
hf : ContinuousOn f s
ι : Type u_1
p : Filter ι
F : ι → α → β
hF : ∀ (i : ι), ContinuousOn (F i) s
⊢ TendstoUniformly (fun i a ↦ { toFun := s.domRestrict (F i), continuous_toFun := ⋯ } a)
      (⇑{ toFun := s.domRestrict f, continuous_toFun := ⋯ }) p ↔
    TendstoUniformly (fun i x ↦ F i ↑x) (f ∘ Subtype.val) p
Module: Mathlib.Probability.ConditionalProbability

Goal state before:
pp: Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst✝³ : Fintype α
inst✝² : MeasurableSpace α
inst✝¹ : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
⊢ (∑ x, μ (X ⁻¹' {x}) • μ[|X ⁻¹' {x}]) E = μ E

Tactic:
calc
    _ = ∑ x, μ (X ⁻¹' {x} ∩ E) := by
      simp only [Measure.coe_finsetSum, Measure.coe_smul, Finset.sum_apply,
        Pi.smul_apply, smul_eq_mul]
      simp_rw [mul_comm (μ _), cond_mul_eq_inter (hX (.singleton _))]
    _ = _ := by
      have : ⋃ x ∈ Finset.univ, X ⁻¹' {x} ∩ E = E := by ext; simp
      rw [← measure_biUnion_finset _ fun _ _ ↦ (hX (.singleton _)).inter hE, this]
      aesop (add simp [PairwiseDisjoint, Set.Pairwise, Function.onFun, disjoint_left])

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Algebra

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalSemiring R
inst✝ : Subsingleton α
s₁ s₂ : Subalgebra R C(α, R)
⊢ s₁ = s₂

Tactic:
cases isEmpty_or_nonempty α
    · have : Subsingleton C(α, R) := DFunLike.coe_injective.subsingleton
      subsingleton
    · inhabit α
      ext f
      have h : f = algebraMap R C(α, R) (f default) := by
        ext x'
        simp only [mul_one, smul_eq_mul, algebraMap_apply]
        congr
        simp [eq_iff_true_of_subsingleton]
      rw [h]
      simp only [Subalgebra.algebraMap_mem]

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f g : α →ₘ[μ] β
⊢ ↑(f ⊓ g) ≤ᵐ[μ] ↑f

Tactic:
filter_upwards [coeFn_inf f g] with _ ha

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f g : α →ₘ[μ] β
a✝ : α
ha : ↑(f ⊓ g) a✝ = ↑f a✝ ⊓ ↑g a✝
⊢ ↑(f ⊓ g) a✝ ≤ ↑f a✝
Module: Mathlib.MeasureTheory.Function.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f g : α →ₘ[μ] β
⊢ ↑(f ⊓ g) ≤ᵐ[μ] ↑g

Tactic:
filter_upwards [coeFn_inf f g] with _ ha

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f g : α →ₘ[μ] β
a✝ : α
ha : ↑(f ⊓ g) a✝ = ↑f a✝ ⊓ ↑g a✝
⊢ ↑(f ⊓ g) a✝ ≤ ↑g a✝
Module: Mathlib.MeasureTheory.Function.SpecialFunctions.Basic

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
f : α → ℝ
hf : Measurable fun x ↦ rexp (f x)
⊢ Measurable f

Tactic:
by
  have : f = fun x ↦ log (exp (f x)) := by ext; rw [log_exp]
  rw [this]
  exact measurable_log.comp hf

Goal state after: