mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
Q : β → Prop
f : (a : α) → P a → β
g : (b : β) → Q b → γ
z : Sym2 α
h : ∀ a ∈ z, P a
h' : ∀ b ∈ pmap f z h, Q b
⊢ pmap g (pmap f z h) h' = pmap (fun a ha ↦ g (f a ⋯) ⋯) z ⋯

Tactic:
by

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

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
X Y X' Y' : V
f : X ⟶ Y
g : X' ⟶ Y'
hX : X' = X
hY : Y' = Y
⊢ f ≍ homOfEq g hX hY ↔ f ≍ g

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
P : α → Prop
s : Sym2 α
h : ∀ a ∈ s, P a
⊢ map Subtype.val (pmap Subtype.mk s h) = s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
s : Sym2 α
P : α → Prop
h : ∀ a ∈ s, P a
⊢ map Subtype.val (s.attachWith h) = s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
x y : α
h : diag x = diag y
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝²³ : AddCommMonoid M
inst✝²² : AddCommMonoid N
inst✝²¹ : CommSemiring R
inst✝²⁰ : CommSemiring S
inst✝¹⁹ : Algebra R S
inst✝¹⁸ : Module R M
inst✝¹⁷ : Module R N
inst✝¹⁶ : Module S N
inst✝¹⁵ : IsScalarTower R S N
T : Type u_4
O : Type u_5
inst✝¹⁴ : CommSemiring T
inst✝¹³ : Algebra R T
inst✝¹² : Algebra S T
inst✝¹¹ : IsScalarTower R S T
inst✝¹⁰ : AddCommMonoid O
inst✝⁹ : Module R O
inst✝⁸ : Module S O
inst✝⁷ : Module T O
inst✝⁶ : IsScalarTower S T O
inst✝⁵ : IsScalarTower R S O
inst✝⁴ : IsScalarTower R T O
f : M →ₗ[R] N
hf : IsBaseChange S f
h : N →ₗ[S] O
hc : IsBaseChange T (↑R h ∘ₗ f)
Q : Type (max v₂ u_5 u_4)
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module T Q
inst✝ : IsScalarTower S T Q
r✝ : N →ₗ[S] Q
this✝ : Module R Q := Module.restrictScalars R S Q
this : IsScalarTower R S Q
r : R
x : Q
⊢ (algebraMap R T) r • x = r • x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
a b a' b' : α
h : Rel α (a, b) (a', b')
hx : a' = b'
⊢ Eq.ndrec (motive := fun x ↦ x.IsDiag → α) (fun x ↦ a) ⋯ hx = a'

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
z : Sym2 α
h : z.IsDiag
⊢ diag (z.diagElem h) = z

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : { a // a.IsDiag }
⊢ (fun a ↦ ⟨diag a, ⋯⟩) ((fun x ↦ (↑x).diagElem ⋯) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
a : α
⊢ (fun x ↦ (↑x).diagElem ⋯) ((fun a ↦ ⟨diag a, ⋯⟩) a) = a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
⊢ Set.range diag = diagSet

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
inst✝ : Subsingleton α
⊢ diagSet = Set.univ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
a : α
z : Sym2 α
hd : ¬z.IsDiag
h : a ∈ z
⊢ Mem.other h ≠ a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
r : β → β → Prop
sym : Std.Symm r
f : α → β
z : Sym2 α
⊢ z ∈ fromRel ⋯ ↔ map f z ∈ fromRel sym

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
⊢ ∀ (x y : α), s(x, y) ∉ fromRel ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
r : α → α → Prop
sym : Std.Symm r
⊢ fromRel sym = ∅ ↔ r = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
⊢ ∀ (x y : α), s(x, y) ∈ fromRel ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
r : α → α → Prop
sym : Std.Symm r
⊢ fromRel sym = Set.univ ↔ r = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
z : Sym2 α
⊢ ∀ (x y : α), s(x, y) ∈ fromRel ⋯ ↔ s(x, y) ∈ {z | ¬z.IsDiag}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
⊢ fromRel ⋯ = {z | ¬z.IsDiag}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
⊢ diagSet = fromRel ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
⊢ diagSetᶜ = fromRel ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
r : α → α → Prop
hr : Std.Symm r
⊢ diagSet ⊆ fromRel hr ↔ Std.Refl r

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
r : α → α → Prop
hr : Std.Symm r
⊢ Disjoint diagSet (fromRel hr) ↔ Std.Irrefl r

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
r : α → α → Prop
hr : Std.Symm r
⊢ fromRel hr ⊆ diagSetᶜ ↔ Std.Irrefl r

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
r : α → α → Prop
sym : Std.Symm r
⊢ Std.Irrefl r → ∀ {z : Sym2 α}, z ∈ fromRel sym → ¬z.IsDiag

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
hr : Std.Symm r
f : α → β
⊢ fromRel ⋯ = map f '' fromRel hr

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z✝ : Sym2 α
f✝ : α → β
r r₁ r₂ : α → α → Prop
sym : Std.Symm r
f : α → β
hf : r ≤ ⇑(Setoid.ker f)
z : ↑(fromRel sym)
a₁ a₂ : α
h : r a₁ a₂
⊢ ⟨f a₁, ⟨s(⟨a₁, ⋯⟩, ⟨a₂, ⋯⟩), h⟩⟩ = ⟨f a₂, ⟨s(⟨a₂, ⋯⟩, ⟨a₁, ⋯⟩), ⋯⟩⟩

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z✝ : Sym2 α
f✝ : α → β
r r₁ r₂ : α → α → Prop
sym : Std.Symm r
f : α → β
hf : r ≤ ⇑(Setoid.ker f)
z : ↑(fromRel sym)
⊢ (fun z ↦ ⟨map Subtype.val ↑z.snd, ⋯⟩)
      ((fun z ↦ fromRelNdrec ↑z ⋯ (fun a₁ a₂ h ↦ ⟨f a₁, ⟨s(⟨a₁, ⋯⟩, ⟨a₂, ⋯⟩), h⟩⟩) ⋯) z) =
    z

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z✝ : Sym2 α
f✝ : α → β
r r₁ r₂ : α → α → Prop
sym : Std.Symm r
f : α → β
hf : r ≤ ⇑(Setoid.ker f)
z : (b : β) × ↑(fromRel ⋯)
⊢ (fun z ↦ fromRelNdrec ↑z ⋯ (fun a₁ a₂ h ↦ ⟨f a₁, ⟨s(⟨a₁, ⋯⟩, ⟨a₂, ⋯⟩), h⟩⟩) ⋯)
      ((fun z ↦ ⟨map Subtype.val ↑z.snd, ⋯⟩) z) =
    z

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
r r₁ r₂ : α → α → Prop
s : Set (Sym2 α)
x y : α
⊢ ToRel s x y → ToRel s y x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
r✝ r₁ r₂ : α → α → Prop
r : { r // Std.Symm r }
⊢ (fun s ↦ ⟨ToRel s, ⋯⟩) ((fun r ↦ fromRel ⋯) r) = r

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
r✝ r₁ r₂ : α → α → Prop
r : { r // Std.Symm r }
⊢ (fun s ↦ ⟨ToRel s, ⋯⟩) ((fun r ↦ fromRel ⋯) r) = r

Tactic:
by simp [toRel_fromRel]

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
r r₁ r₂ : α → α → Prop
s : Set (Sym2 α)
⊢ (fun r ↦ fromRel ⋯) ((fun s ↦ ⟨ToRel s, ⋯⟩) s) = s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
r r₁✝ r₂✝ : α → α → Prop
r₁ r₂ : { r // Std.Symm r }
⊢ { toFun := fun r ↦ fromRel ⋯, invFun := fun s ↦ ⟨ToRel s, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } r₁ ⊆
      { toFun := fun r ↦ fromRel ⋯, invFun := fun s ↦ ⟨ToRel s, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } r₂ ↔
    r₁ ≤ r₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
r₁ r₂ : α → α → Prop
sym₁ : Std.Symm r₁
sym₂ : Std.Symm r₂
⊢ fromRel sym₁ = fromRel sym₂ ↔ r₁ = r₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
z✝ : Sym2 α✝
f : α✝ → β
α : Type u_4
z : Sym2 α
⊢ Multiset α

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_4
z : Sym2 α
⊢ z.toMultiset.card = 2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_4
x : α
z : Sym2 α
⊢ x ∈ z.toMultiset ↔ x ∈ z

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
z : Sym2 α
⊢ x ∈ z.toFinset ↔ x ∈ z

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
z : Sym2 α
⊢ z.toFinset ≠ ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : α
⊢ s(x, y).toFinset = {x, y}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
z : Sym2 α
h : z.IsDiag
⊢ #z.toFinset = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
z : Sym2 α
h : ¬z.IsDiag
⊢ #z.toFinset = 2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
z : Sym2 α
⊢ #z.toFinset = if z.IsDiag then 1 else 2

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
a₁ b₁ a₂ b₂ : α
⊢ [a₁, b₁].Perm [a₂, b₂] → a₁ = a₂ ∧ b₁ = b₂ ∨ a₁ = b₂ ∧ b₁ = a₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = a₂
h₂ : b₁ = b₂
⊢ [a₁, b₁].Perm [a₂, b₂]

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
a₁ b₁ a₂ b₂ : α
h₁ : a₁ = b₂
h₂ : b₁ = a₂
⊢ [a₁, b₁].Perm [a₂, b₂]

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
⊢ ∀ ⦃a b : α × α⦄, Rel α a b → (Vector.Perm.isSetoid α 2) ⟨[a.1, a.2], ⋯⟩ ⟨[b.1, b.2], ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
⊢ 𝟙 X ≫ f = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
⊢ f ≫ 𝟙 Y = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f g : X ⟶ Y
w : f = g
h : Y ⟶ Z
⊢ f ≫ h = g ≫ h

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
w : ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Prefunctor

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F_obj : V → W
map✝¹ : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
G_obj : V → W
map✝ : {X Y : V} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
h_obj : ∀ (X : V), { obj := F_obj, map := map✝¹ }.obj X = { obj := G_obj, map := map✝ }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹ }.map f = Eq.recOn ⋯ (Eq.recOn ⋯ ({ obj := G_obj, map := map✝ }.map f))
⊢ F_obj = G_obj

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
w : (fun {Z} h ↦ f ≫ h) = fun {Z} h ↦ g ≫ h
Z : C
h : Y ⟶ Z
⊢ f ≫ h = g ≫ h

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
f : X ⟶ X
w : ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g
⊢ f = 𝟙 X

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Prop
inst✝ : Decidable P
X Y Z : C
f : X ⟶ Y
g g' : Y ⟶ Z
⊢ (f ≫ if P then g else g') = if P then f ≫ g else f ≫ g'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Prop
inst✝ : Decidable P
X Y Z : C
f : X ⟶ Y
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
⊢ (f ≫ if h : P then g h else g' h) = if h : P then f ≫ g h else f ≫ g' h

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y Z X Z✝ : C
g h : X ⟶ Z✝
w : 𝟙 X ≫ g = 𝟙 X ≫ h
⊢ g = h

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : Epi f
g h : Y ⟶ Z
W : C
k l : Z ⟶ W
p : (f ≫ g) ≫ k = (f ≫ h) ≫ l
⊢ f ≫ g ≫ k = f ≫ h ≫ l

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : Epi f
g h : Y ⟶ Z
W : C
k l : Z ⟶ W
p : g ≫ k = h ≫ l
⊢ (f ≫ g) ≫ k = (f ≫ h) ≫ l

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Prefunctor

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F G : Prefunctor V W
h_obj : ∀ (X : V), F.obj X = G.obj X
h_map : ∀ (X Y : V) (f : X ⟶ Y), F.map f = Eq.recOn ⋯ (Eq.recOn ⋯ (G.map f))
⊢ F = G

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
h : Y ⟶ Y
⊢ f ≫ h = f ↔ h = 𝟙 Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi (f ≫ g)
Z✝ : C
x✝¹ x✝ : Z ⟶ Z✝
w : g ≫ x✝¹ = g ≫ x✝
⊢ (f ≫ g) ≫ x✝¹ = (f ≫ g) ≫ x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : Epi h
w : f ≫ g = h
⊢ Epi g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Category.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u
inst✝ : SmallCategory D
⊢ LargeCategory (ULift.{u + 1, u} D)

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Prefunctor

Goal state before:
pp: V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
F G : Prefunctor V W
h_obj : ∀ (X : V), F.obj X = G.obj X
h_map : ∀ (X Y : V) (f : X ⟶ Y), F.map f = Quiver.homOfEq (G.map f) ⋯ ⋯
⊢ F = G

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Prefunctor

Goal state before:
pp: U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F : U ⥤q V
X Y : U
f g : X ⟶ Y
h : f = g
⊢ F.map f = F.map g

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Prefunctor

Goal state before:
pp: U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F G : U ⥤q V
e : F = G
X : U
⊢ F.obj X = G.obj X

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Prefunctor

Goal state before:
pp: U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F G : U ⥤q V
e : F = G
X Y : U
f : X ⟶ Y
⊢ Quiver.homOfEq (F.map f) ⋯ ⋯ = G.map f

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Prefunctor

Goal state before:
pp: U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F : U ⥤q V
X Y : U
f : X ⟶ Y
X' Y' : U
hX : X = X'
hY : Y = Y'
⊢ F.map (Quiver.homOfEq f hX hY) = Quiver.homOfEq (F.map f) ⋯ ⋯

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Algebra R S
inst✝¹⁴ : Module R M
inst✝¹³ : Module R N
inst✝¹² : Module S N
inst✝¹¹ : IsScalarTower R S N
T : Type u_4
O : Type u_5
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R T
inst✝⁸ : Algebra S T
inst✝⁷ : IsScalarTower R S T
inst✝⁶ : AddCommMonoid O
inst✝⁵ : Module R O
inst✝⁴ : Module S O
inst✝³ : Module T O
inst✝² : IsScalarTower S T O
inst✝¹ : IsScalarTower R S O
inst✝ : IsScalarTower R T O
f : M →ₗ[R] N
hf : IsBaseChange S f
h : N →ₗ[S] O
hc : IsBaseChange T (↑R h ∘ₗ f)
⊢ IsBaseChange T h

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
x : R
y : N
⊢ (IsTensorProduct.map hf hf LinearMap.id ((LinearMap.lsmul R M) x)) 0 =
    (↑R ((LinearMap.lsmul S N) ((algebraMap R S) x))) 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
x : R
y x✝¹ x✝ : N
ha :
  (IsTensorProduct.map hf hf LinearMap.id ((LinearMap.lsmul R M) x)) x✝¹ =
    (↑R ((LinearMap.lsmul S N) ((algebraMap R S) x))) x✝¹
hb :
  (IsTensorProduct.map hf hf LinearMap.id ((LinearMap.lsmul R M) x)) x✝ =
    (↑R ((LinearMap.lsmul S N) ((algebraMap R S) x))) x✝
⊢ (IsTensorProduct.map hf hf LinearMap.id ((LinearMap.lsmul R M) x)) (x✝¹ + x✝) =
    (↑R ((LinearMap.lsmul S N) ((algebraMap R S) x))) (x✝¹ + x✝)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
⊢ ∀ ⦃a b : List.Vector α 2⦄, (Vector.Perm.isSetoid α 2) a b → Rel α (fromVector a) (fromVector b)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
x : R
⊢ IsTensorProduct.map hf hf LinearMap.id ((LinearMap.lsmul R M) x) = ↑R ((LinearMap.lsmul S N) ((algebraMap R S) x))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
⊢ ∀ ⦃a b : List.Vector α 2⦄, (Vector.Perm.isSetoid α 2) a b → Rel α (fromVector a) (fromVector b)

Tactic:
by
        rintro ⟨x, hx⟩ ⟨y, hy⟩ h
        rcases x with - | ⟨_, x⟩; · simp at hx
        rcases x with - | ⟨_, x⟩; · simp at hx
        rcases x with - | ⟨_, x⟩; swap
        · exfalso
          simp at hx
        rcases y with - | ⟨_, y⟩; · simp at hy
        rcases y with - | ⟨_, y⟩; · simp at hy
        rcases y with - | ⟨_, y⟩; swap
        · exfalso
          simp at hy
        rcases perm_card_two_iff.mp h with (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)
        · constructor
        apply Sym2.Rel.swap

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
⊢ LeftInverse (Quot.map fromVector ⋯) (Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : Sym' α 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ x) = x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝³³ : AddCommMonoid M
inst✝³² : AddCommMonoid N
inst✝³¹ : CommSemiring R
inst✝³⁰ : CommSemiring S
inst✝²⁹ : Algebra R S
inst✝²⁸ : Module R M
inst✝²⁷ : Module R N
inst✝²⁶ : Module S N
inst✝²⁵ : IsScalarTower R S N
f : M →ₗ[R] N
h✝ : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst✝²⁴ : AddCommMonoid P
inst✝²³ : Module R P
inst✝²² : AddCommMonoid Q
inst✝²¹ : Module S Q
inst✝²⁰ : Module R Q
inst✝¹⁹ : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst✝¹⁸ : CommSemiring T
inst✝¹⁷ : Algebra R T
inst✝¹⁶ : Algebra S T
inst✝¹⁵ : IsScalarTower R S T
inst✝¹⁴ : AddCommMonoid O
inst✝¹³ : Module R O
inst✝¹² : Module S O
inst✝¹¹ : Module T O
inst✝¹⁰ : IsScalarTower S T O
inst✝⁹ : IsScalarTower R S O
inst✝⁸ : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst✝⁷ : CommSemiring R'
inst✝⁶ : CommSemiring S'
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R' S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
h : IsPushout R S R' S'
x y : S ⊗[R] R'
⊢ (↑⋯.equiv).toFun (x * y) = (↑⋯.equiv).toFun x * (↑⋯.equiv).toFun y

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝³³ : AddCommMonoid M
inst✝³² : AddCommMonoid N
inst✝³¹ : CommSemiring R
inst✝³⁰ : CommSemiring S
inst✝²⁹ : Algebra R S
inst✝²⁸ : Module R M
inst✝²⁷ : Module R N
inst✝²⁶ : Module S N
inst✝²⁵ : IsScalarTower R S N
f : M →ₗ[R] N
h✝ : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst✝²⁴ : AddCommMonoid P
inst✝²³ : Module R P
inst✝²² : AddCommMonoid Q
inst✝²¹ : Module S Q
inst✝²⁰ : Module R Q
inst✝¹⁹ : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst✝¹⁸ : CommSemiring T
inst✝¹⁷ : Algebra R T
inst✝¹⁶ : Algebra S T
inst✝¹⁵ : IsScalarTower R S T
inst✝¹⁴ : AddCommMonoid O
inst✝¹³ : Module R O
inst✝¹² : Module S O
inst✝¹¹ : Module T O
inst✝¹⁰ : IsScalarTower S T O
inst✝⁹ : IsScalarTower R S O
inst✝⁸ : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst✝⁷ : CommSemiring R'
inst✝⁶ : CommSemiring S'
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R' S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
h : IsPushout R S R' S'
⊢ ∀ (r : S), (↑⋯.equiv).toFun ((algebraMap S (S ⊗[R] R')) r) = (algebraMap S S') r

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f✝ : α → β
inst✝ : DecidableEq α
a b c d e : α
h✝ : Rel α (b, c) (d, e)
hy : a ∈ s(d, e)
f : Sym2 α
g : s(b, c) = f
h : a ∈ f
⊢ Eq.ndrec (motive := fun x ↦ a ∈ x → α) (fun x ↦ if a = b then c else b) g h = if a = b then c else b

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝⁸ : CommSemiring R'
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra R R'
inst✝⁵ : Algebra S S'
inst✝⁴ : Algebra R' S'
inst✝³ : Algebra R S'
inst✝² : IsScalarTower R R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsPushout R S R' S'
a : S
⊢ (equiv R S R' S').symm ((algebraMap S S') a) = a ⊗ₜ[R] 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z✝ : Sym2 α
f : α → β
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ ∀ (a_1 b c d : α) (h : Rel α (a_1, b) (c, d)),
    Eq.ndrec (motive := fun x ↦ a ∈ x → α) (fun x ↦ if a = a_1 then b else a_1) ⋯ = fun x ↦ if a = c then d else c

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝⁸ : CommSemiring R'
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra R R'
inst✝⁵ : Algebra S S'
inst✝⁴ : Algebra R' S'
inst✝³ : Algebra R S'
inst✝² : IsScalarTower R R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsPushout R S R' S'
a : R'
⊢ (equiv R S R' S').symm ((algebraMap R' S') a) = 1 ⊗ₜ[R] a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ s(a, Mem.other' h) = z

Tactic:
by

Goal state after: