mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Hall.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : DecidableEq β
R : SetRel α β
inst✝ : (a : α) → Fintype ↑(R.image {a})
⊢ (∀ (A : Finset α), #A ≤ card ↑(R.image ↑A)) ↔ ∃ f, Injective f ∧ ∀ (x : α), (x, f x) ∈ R

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hall.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : DecidableRel r
this : DecidableEq β
r' : α → Finset β := fun a ↦ {b | r a b}
⊢ ∀ (A : Finset α), {b | ∃ a ∈ A, r a b} = A.biUnion r'

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
⊢ ∃ 𝓕', 𝓕'.Countable ∧ sSup 𝓕' = φ ∧ ∀ f ∈ 𝓕', f ≤ φ ∧ ∃ l c, f = ⇑re ∘ ⇑l + const E c

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hall.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : DecidableRel r
this : DecidableEq β
r' : α → Finset β := fun a ↦ {b | r a b}
h : ∀ (A : Finset α), {b | ∃ a ∈ A, r a b} = A.biUnion r'
⊢ ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
φ : E → ℝ
inst✝⁹ : RCLike 𝕜
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : HereditarilyLindelofSpace E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
⊢ ∃ l c, (∀ (i : ℕ), ⇑re ∘ ⇑(l i) + const E (c i) ≤ φ) ∧ ⨆ i, ⇑re ∘ ⇑(l i) + const E (c i) = φ

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Hall.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Fintype β
r : α → β → Prop
inst✝ : DecidableRel r
⊢ (∀ (A : Finset α), #A ≤ #{b | ∃ a ∈ A, r a b}) ↔ ∃ f, Injective f ∧ ∀ (x : α), r x (f x)

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type x
⊢ Injective toFun

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type x
f : α ≃. β
g : β ≃. γ
a : α
b : γ
⊢ (g.symm b).bind ⇑f.symm = some a ↔ (f a).bind ⇑g = some b

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
x : β
y : α
⊢ f.symm x = some y ↔ some x = f y

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
x : β
y : α
⊢ some y = f.symm x ↔ f y = some x

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α ≃. β
g : β ≃. γ
a : α
⊢ (f.trans g) a = none ↔ ∀ (b : β) (c : γ), ¬b ∈ f a ∨ ¬c ∈ g b

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
⊢ (PEquiv.refl α).trans f = f

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
⊢ f.trans (PEquiv.refl β) = f

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
a₁ a₂ : α
b : β
h₁ : b ∈ f a₁
h₂ : b ∈ f a₂
⊢ a₁ = a₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → (f a₁).isSome = true
x : α
hfx : f x = none
⊢ ¬none.isSome = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
a₂ : α
h : ∀ (a₁ : α), a₁ ≠ a₂ → (f a₁).isSome = true
x : α
⊢ (fun b ↦ Option.recOn b a₂ fun b' ↦ Option.recOn (f.symm b') a₂ id) (f x) = x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
j : J
⊢ ∃ i_1 f,
    ∀ ⦃k : J⦄ (g : k ⟶ i_1),
      range ⇑(ConcreteCategory.hom ((F.toPreimages s).map f)) ⊆
        range ⇑(ConcreteCategory.hom ((F.toPreimages s).map (g ≫ f)))

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x ↦ x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
a b : α
⊢ (if b ∈ s then some b else none) = some a ↔ (if a ∈ s then some a else none) = some b

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
a : α
⊢ a ∈ (ofSet s) a ↔ a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
a b : α
⊢ a ∈ (ofSet s) b ↔ a = b ∧ a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
h : ofSet s = PEquiv.refl α
⊢ s = Set.univ

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
h : s = Set.univ
⊢ ofSet s = PEquiv.refl α

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
⊢ f.trans f.symm = ofSet {a | (f a).isSome = true}

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
⊢ (f.symm.trans f).symm = (ofSet {b | (f.symm b).isSome = true}).symm

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
⊢ f.trans f.symm = PEquiv.refl α ↔ ∀ (a : α), (f a).isSome = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type x
⊢ ∀ (a : α) (b : β), none = some a ↔ none = some b

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α ≃. β
⊢ f.trans ⊥ = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : β ≃. γ
⊢ ⊥.trans f = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
f : α ≃. β
a : α
h : (f a).isSome = true
⊢ f.symm ((f a).get h) = some a

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
h : ∀ (j : J), ∃ i f, (range ⇑(ConcreteCategory.hom (F.map f))).Finite
⊢ F.IsMittagLeffler

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
i j : J
f : i ⟶ j
x✝ : (fun X ↦ X) (F.toEventualRanges.obj j)
x : (fun X ↦ X) (F.obj j)
hx : x ∈ F.eventualRange j
⊢ ∃ a, (ConcreteCategory.hom (F.toEventualRanges.map f)) a = ⟨x, hx⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
x : α
y : β
h1 : y = b
h2 : ¬x = a
⊢ some a = some x ↔ False

pp: case pos
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
x : α
y : β
h1 : ¬y = b
h✝ : x = a
⊢ False ↔ some b = some y

pp: case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
x : α
y : β
h1 : ¬y = b
h✝ : ¬x = a
⊢ False ↔ False

Tactic:
· simp only [some.injEq, iff_false] at *
      exact Ne.symm h2

Goal state after:
case pos
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
x : α
y : β
h1 : ¬y = b
h✝ : x = a
⊢ False ↔ some b = some y

case neg
α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
x : α
y : β
h1 : ¬y = b
h✝ : ¬x = a
⊢ False ↔ False
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝² : Category.{v_1, u} J
F : J ⥤ Type v
inst✝¹ : IsCofilteredOrEmpty J
h : F.IsMittagLeffler
inst✝ : ∀ (j : J), Nonempty (F.obj j)
j : J
⊢ Nonempty (F.toEventualRanges.obj j)

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
x : α
y : β
⊢ (if y = b then some a else none) = some x ↔ (if x = a then some b else none) = some y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
i j : J
f g : i ⟶ j
⊢ F.map f = F.map g

Tactic:
by

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
inst✝ : IsOrderedRing R
n : ℕ
s : Simplex R P n
i j : Fin (n + 1)
h : i ≠ j
⊢ (s.face ⋯).closedInterior = affineSegment R (s.points i) (s.points j)

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a₁ a₂ : α
b₁ b₂ : β
⊢ b₁ ∈ (single a₂ b₂) a₁ ↔ a₁ = a₂ ∧ b₁ = b₂

Tactic:
by

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
inst✝ : IsOrderedRing R
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
⊢ p ∈ (s.face ⋯).closedInterior ↔ Wbtw R (s.points i) p (s.points j)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
i : J
s : Set (F.obj i)
inst✝ : IsCofilteredOrEmpty J
hFn : ∀ (j : J), Nonempty (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
hs : s.Nonempty
j : J
⊢ Nonempty ((F.toPreimages s).obj j)

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a : α
b : β
c : γ
f : β ≃. γ
h : c ∈ f b
⊢ (single a b).trans f = single a c

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
j : J
Finj : ∀ (i : J) (f : i ⟶ j), Function.Injective ⇑(ConcreteCategory.hom (F.map f))
i : J
f : i ⟶ j
⊢ Function.Injective fun s ↦ ↑s j

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Subsingleton α
a b : α
⊢ single a b = PEquiv.refl α

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝³ : Category.{v_1, u} J
F : J ⥤ Type v
inst✝² : IsCofilteredOrEmpty J
inst✝¹ : ∀ (j : J), Nonempty (F.obj j)
inst✝ : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
i : J
x : F.obj i
s : Set (F.obj i) := {x}
this : ∀ (j : J), Nonempty ((F.toPreimages s).obj j)
sec : (j : J) → (F.toPreimages s).obj j
h : sec ∈ (F.toPreimages s).sections
j✝ j'✝ : J
jk : j✝ ⟶ j'✝
⊢ (ConcreteCategory.hom (F.map jk)) ((fun j ↦ ↑(sec j)) j✝) = (fun j ↦ ↑(sec j)) j'✝

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
b : β
c : γ
f : δ ≃. β
h : f.symm b = none
⊢ f.trans (single b c) = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type x
f g : α ≃. β
fg : ∀ (a : α) (b : β), b ∈ f a → b ∈ g a
gf : ∀ (a : α) (b : β), b ∈ g a → b ∈ f a
a : α
⊢ f a = g a

Tactic:
rcases h : g a with _ | b

Goal state after:
case none
α : Type u
β : Type v
γ : Type w
δ : Type x
f g : α ≃. β
fg : ∀ (a : α) (b : β), b ∈ f a → b ∈ g a
gf : ∀ (a : α) (b : β), b ∈ g a → b ∈ f a
a : α
h : g a = none
⊢ f a = none

case some
α : Type u
β : Type v
γ : Type w
δ : Type x
f g : α ≃. β
fg : ∀ (a : α) (b : β), b ∈ f a → b ∈ g a
gf : ∀ (a : α) (b : β), b ∈ g a → b ∈ f a
a : α
b : β
h : g a = some b
⊢ f a = some b
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
inst✝ : IsOrderedRing R
s : Simplex R P 1
w : Fin (1 + 1) → R
hw : ∑ i, w i = 1
h01 : ∀ (i : Fin (1 + 1)), w i ∈ Set.Ioo 0 1
⊢ w = Finset.affineCombinationLineMapWeights 0 1 (w 1)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝³ : Category.{v_1, u} J
F : J ⥤ Type v
inst✝² : IsCofilteredOrEmpty J
inst✝¹ : ∀ (j : J), Nonempty (F.obj j)
inst✝ : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
i : J
x : F.obj i
⊢ ∃ a, (fun s ↦ ↑s i) a = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type x
f g : α ≃. β
fg : ∀ (a : α) (b : β), b ∈ f a → b ∈ g a
gf : ∀ (a : α) (b : β), b ∈ g a → b ∈ f a
⊢ ∀ (x : α), f x = g x

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f g : α ≃. β
a : α
b : β
⊢ (if f.symm b = g.symm b then f.symm b else none) = some a ↔ (if f a = g a then f a else none) = some b

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.CofilteredSystem

Goal state before:
pp: J : Type u
inst✝⁵ : Category.{v_1, u} J
F : J ⥤ Type v
inst✝⁴ : IsCofilteredOrEmpty J
inst✝³ : ∀ (j : J), Nonempty (F.obj j)
inst✝² : ∀ (j : J), Finite (F.obj j)
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(ConcreteCategory.hom (F.map f))
inst✝¹ : Nonempty J
inst✝ : Finite ↑F.sections
⊢ ∃ j, ∀ (i : J) (f : i ⟶ j), Function.Injective ⇑(ConcreteCategory.hom (F.map f))

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x✝³ x✝² : α ≃. β
x✝¹ : α
x✝ : β
⊢ x✝ ∈
      { toFun := fun a ↦ if x✝³ a = x✝² a then x✝³ a else none,
          invFun := fun b ↦ if x✝³.symm b = x✝².symm b then x✝³.symm b else none, inv := ⋯ }
        x✝¹ →
    x✝ ∈ x✝³ x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x✝³ x✝² : α ≃. β
x✝¹ : α
x✝ : β
⊢ x✝ ∈
      { toFun := fun a ↦ if x✝³ a = x✝² a then x✝³ a else none,
          invFun := fun b ↦ if x✝³.symm b = x✝².symm b then x✝³.symm b else none, inv := ⋯ }
        x✝¹ →
    x✝ ∈ x✝² x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Permutation

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Zero R
inst✝ : One R
⊢ Perm.permMatrix R (Equiv.refl n) = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Permutation

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Zero R
inst✝ : One R
⊢ (Perm.permMatrix R σ)ᵀ = Perm.permMatrix R σ⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Permutation

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : NonAssocSemiring R
inst✝ : StarRing R
⊢ (Perm.permMatrix R σ)ᴴ = Perm.permMatrix R σ⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Permutation

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Fintype n
inst✝ : CommRing R
⊢ (Perm.permMatrix R σ).det = ↑↑(Perm.sign σ)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Permutation

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Fintype n
inst✝ : AddCommMonoidWithOne R
⊢ (Perm.permMatrix R σ).trace = ↑(Function.fixedPoints ⇑σ).ncard

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Permutation

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Fintype n
v : n → R
inst✝ : CommRing R
⊢ Perm.permMatrix R σ *ᵥ v = v ∘ ⇑σ

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Permutation

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Fintype n
v : n → R
inst✝ : CommRing R
⊢ v ᵥ* Perm.permMatrix R σ = v ∘ ⇑(Equiv.symm σ)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonAssocSemiring α
f : l ≃. m
i : l
j : n
M : Matrix m n α
⊢ (f.toMatrix * M) i j = Option.casesOn (f i) 0 fun fi ↦ M fi j

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f g h : α ≃. β
fg : f ≤ g
gh : f ≤ h
a : α
b : β
⊢ b ∈ f a →
    b ∈
      { toFun := fun a ↦ if g a = h a then g a else none,
          invFun := fun b ↦ if g.symm b = h.symm b then g.symm b else none, inv := ⋯ }
        a

Tactic:
by

Goal state after:
Module: Mathlib.Data.PEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α ≃ β
⊢ ∀ (a : α) (b : β), (some ∘ ⇑f.symm) b = some a ↔ (some ∘ ⇑f) a = some b

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Permutation

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ τ : Perm n
inst✝¹ : Fintype n
inst✝ : NonAssocSemiring R
⊢ Perm.permMatrix R (σ * τ) = Perm.permMatrix R τ * Perm.permMatrix R σ

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Permutation

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ✝ τ✝ : Perm n
inst✝¹ : Fintype n
inst✝ : NonAssocSemiring R
σ τ : Perm n
⊢ Perm.permMatrix R (σ * τ)⁻¹ = Perm.permMatrix R σ⁻¹ * Perm.permMatrix R τ⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Permutation

Goal state before:
pp: n : Type u_1
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Fintype n
𝕜 : Type u_3
inst✝ : RCLike 𝕜
⊢ 0 ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Permutation

Goal state before:
pp: n : Type u_1
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Fintype n
𝕜 : Type u_3
inst✝ : RCLike 𝕜
⊢ ∀ (x : EuclideanSpace 𝕜 n),
    ‖((toEuclideanLin.trans LinearMap.toContinuousLinearMap) (Perm.permMatrix 𝕜 σ)) x‖ ≤ 1 * ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Permutation

Goal state before:
pp: n : Type u_1
inst✝³ : DecidableEq n
σ : Perm n
inst✝² : Fintype n
𝕜 : Type u_3
inst✝¹ : RCLike 𝕜
inst✝ : Nonempty n
⊢ 1 ≤ ‖Perm.permMatrix 𝕜 σ‖

Tactic:
by

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AffineSpace V P
inst✝ : IsOrderedRing R
s : Simplex R P 1
⊢ s.interior = ⇑(lineMap (s.points 0) (s.points 1)) '' Set.Ioo 0 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq n
M : Matrix l m α
f : m ≃. n
i : l
j : n
⊢ (M * f.toMatrix) i j = Option.casesOn (f.symm j) 0 (M i)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AffineSpace V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
s : Simplex R P 1
p : P
⊢ 0 ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃. n
⊢ f.symm.toMatrix = f.toMatrixᵀ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
⊢ (PEquiv.refl n).toMatrix = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃ n
i : m
⊢ f.toPEquiv.toMatrix i = Pi.single (f i) 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AffineSpace V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
s : Simplex R P 1
p : P
⊢ p ∈ s.interior ↔ Sbtw R (s.points 0) p (s.points 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃ n
j : n
⊢ f.toPEquiv.toMatrixᵀ j = Pi.single (f.symm j) 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonAssocSemiring α
f : l ≃ m
M : Matrix m n α
⊢ f.toPEquiv.toMatrix * M = M.submatrix (⇑f) id

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : NonAssocSemiring α
M : Matrix l m α
f : m ≃ n
i : l
j : n
⊢ (M * f.toPEquiv.toMatrix) i j = M.submatrix id (⇑f.symm) i j

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : NonAssocSemiring α
σ : m ≃ n
a : n → α
⊢ σ.toPEquiv.toMatrix *ᵥ a = a ∘ ⇑σ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonAssocSemiring α
σ : m ≃ n
a : m → α
⊢ a ᵥ* σ.toPEquiv.toMatrix = a ∘ ⇑σ.symm

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : NonAssocSemiring α
f : l ≃. m
g : m ≃. n
⊢ (f.trans g).toMatrix = f.toMatrix * g.toMatrix

Tactic:
by

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

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AffineSpace V P
inst✝² : IsOrderedRing R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R V
n : ℕ
s : Simplex R P n
p : P
i j : Fin (n + 1)
h : i ≠ j
⊢ Sbtw R (s.points i) p (s.points j) ↔ Sbtw R (s.points (min i j)) p (s.points (max i j))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.PEquiv

Goal state before:
pp: m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
⊢ Function.Injective toMatrix

Tactic:
by

Goal state after: