mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.sndKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0
q : T ⟶ X
hq : q ≫ b.inl = m - (f ≫ b.inl + g ≫ b.inr)
⊢ m = f ≫ b.inl + g ≫ b.inr

Tactic:
← sub_eq_zero,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.sndKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0
q : T ⟶ X
hq : q ≫ b.inl = m - (f ≫ b.inl + g ≫ b.inr)
⊢ m - (f ≫ b.inl + g ≫ b.inr) = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
b : Bicone f
hb : b.IsBilimit
j : J
j' : Discrete J
⊢ (ι f j ≫ (hb.isLimit.conePointUniqueUpToIso (isLimit f)).inv) ≫ b.toCone.π.app j' =
    (ι f j ≫ desc b.ι) ≫ b.toCone.π.app j'

Tactic:
rw [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp, Bicone.toCone_π_app,
    biproduct.bicone_π, biproduct.ι_desc, biproduct.ι_π, b.toCone_π_app, b.ι_π]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.fstKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0
q : T ⟶ Y
hq : q ≫ b.inr = m - (f ≫ b.inl + g ≫ b.inr)
⊢ m = f ≫ b.inl + g ≫ b.inr

Tactic:
← sub_eq_zero,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.fstKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0
q : T ⟶ Y
hq : q ≫ b.inr = m - (f ≫ b.inl + g ≫ b.inr)
⊢ m - (f ≫ b.inl + g ≫ b.inr) = 0
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsColimit b.inrCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
h₂' : b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
q : X ⟶ T
hq : b.fst ≫ q = m - (b.fst ≫ f + b.snd ≫ g)
⊢ m = b.fst ≫ f + b.snd ≫ g

Tactic:
← sub_eq_zero,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsColimit b.inrCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
h₂' : b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
q : X ⟶ T
hq : b.fst ≫ q = m - (b.fst ≫ f + b.snd ≫ g)
⊢ m - (b.fst ≫ f + b.snd ≫ g) = 0
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsColimit b.inlCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
h₂' : b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
q : Y ⟶ T
hq : b.snd ≫ q = m - (b.fst ≫ f + b.snd ≫ g)
⊢ m = b.fst ≫ f + b.snd ≫ g

Tactic:
← sub_eq_zero,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsColimit b.inlCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
h₂' : b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0
q : Y ⟶ T
hq : b.snd ≫ q = m - (b.fst ≫ f + b.snd ≫ g)
⊢ m - (b.fst ≫ f + b.snd ≫ g) = 0
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: k n : ℕ
⊢ (antidiagonalTuple k n).Nodup

Tactic:
induction k generalizing n with

Goal state after:
case succ
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
⊢ (antidiagonalTuple (k + 1) n).Nodup
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
hn : 0 < n
c : Composition n
⊢ c ≠ single n hn ↔ ∀ (i : Fin c.length), c.blocksFun i < n

Tactic:
contrapose!

Goal state after:
n : ℕ
hn : 0 < n
c : Composition n
⊢ c = single n hn ↔ ∃ i, n ≤ c.blocksFun i
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List (Perm α)
h : List.Pairwise Disjoint l
⊢ l.prod.support = List.foldr (fun x1 x2 ↦ x1 ⊔ x2) ⊥ (List.map support l)

Tactic:
by
  induction l with
  | nil => simp
  | cons hd tl hl =>
    rw [List.pairwise_cons] at h
    have : Disjoint hd tl.prod := disjoint_prod_right _ h.left
    simp [this.support_mul, hl h.right]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ True) ∧ y ≠ z ∧ True
⊢ (swap x y * swap y z).support ⊆ {x, y, z}

pp: case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ True) ∧ y ≠ z ∧ True
⊢ {x, y, z} ⊆ (swap x y * swap y z).support

Tactic:
· convert! support_mul_le (swap x y) (swap y z) using 1
    rw [support_swap h.left.left, support_swap h.right.left]
    simp [-Finset.union_singleton]

Goal state after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ True) ∧ y ≠ z ∧ True
⊢ {x, y, z} ⊆ (swap x y * swap y z).support
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
⊢ (x :: xs).formPerm (x :: xs)[xs.length] = x

Tactic:
rw [getElem_cons_length rfl, formPerm_apply_getLast]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h : σ ≠ 1
⊢ #{x | σ x = x} < Fintype.card α - 1

Tactic:
Nat.lt_sub_iff_add_lt,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h : σ ≠ 1
⊢ #{x | σ x = x} + 1 < Fintype.card α
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x ((σ ^ n) x) ∈ H
h5 : ¬x = (σ ^ n) x
h6 : x = (σ ^ (n + 1)) x
⊢ swap x ((σ ^ (n + 1)) x) ∈ H

Tactic:
rw [← h6, swap_self]
        exact H.one_mem

Goal state after:
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
y : α
hx : x ∈ univ
⊢ swap x y ∈ H

Tactic:
← h2,

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
y : α
hx : x ∈ σ.support
⊢ swap x y ∈ H
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
y : α
hx : σ x ≠ x
hy : y ∈ univ
⊢ swap x y ∈ H

Tactic:
← h2,

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
y : α
hx : σ x ≠ x
hy : y ∈ σ.support
⊢ swap x y ∈ H
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
σ : Perm α
h0 : n.Coprime #univ
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
⊢ closure {σ, swap x ((σ ^ n) x)} = ⊤

Tactic:
← h2,

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
σ : Perm α
h0 : n.Coprime #σ.support
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
⊢ closure {σ, swap x ((σ ^ n) x)} = ⊤
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i m : ℕ
hi : ((σ ^ #univ) ^ m) x = y
hm : i = Fintype.card α * m
⊢ x = y

Tactic:
← h2,

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i m : ℕ
hi : ((σ ^ #σ.support) ^ m) x = y
hm : i = Fintype.card α * m
⊢ x = y
Module: Mathlib.Data.List.Iterate

Goal state before:
pp: α : Type u_1
f : α → α
a : α
m n : ℕ
⊢ map (fun x ↦ f^[x] a) (take m (range n)) = map (fun x ↦ f^[x] a) (range (min m n))

Tactic:
take_range

Goal state after:
α : Type u_1
f : α → α
a : α
m n : ℕ
⊢ map (fun x ↦ f^[x] a) (range (min m n)) = map (fun x ↦ f^[x] a) (range (min m n))
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case a
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j ↦ ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
this : DecidableEq ι := ⋯
⊢ mrange (noncommPiCoprod ϕ hcomm) ≤ ⨆ i, mrange (ϕ i)

Tactic:
rintro x ⟨f, rfl⟩
    refine Submonoid.noncommProd_mem _ _ _ (fun _ _ _ _ h => hcomm h _ _) (fun i _ => ?_)
    apply Submonoid.mem_sSup_of_mem
    · use i
    simp

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case neg
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
h : ¬f.SameCycle x y
⊢ (ofSubtype (f.subtypePerm ⋯)) y = y

Tactic:
apply ofSubtype_apply_of_not_mem

Goal state after:
case neg
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
h : ¬f.SameCycle x y
⊢ ¬f.SameCycle x y
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
⊢ (f.cycleOf x)⁻¹ y = (f⁻¹.cycleOf x) y

Tactic:
by
    rw [inv_eq_iff_eq, cycleOf_apply, cycleOf_apply]
    split_ifs <;> simp_all [sameCycle_inv, sameCycle_symm_apply_right]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case pos
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableRel f.SameCycle
inst✝ : DecidableEq α
hf : f.IsCycle
hx : f x = x
⊢ f.cycleOf x = 1

Tactic:
cycleOf_eq_one_iff

Goal state after:
case pos
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableRel f.SameCycle
inst✝ : DecidableEq α
hf : f.IsCycle
hx : f x = x
⊢ f x = x
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
i : ℤ
hi : (fun x ↦ c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x : α
hx : x ∈ c.support
⊢ g (c x) = c (g x)

Tactic:
suffices hi' : ∀ x ∈ c.support, g x = (c ^ i) x by
        rw [hi' x hx, hi' (c x) (apply_mem_support.mpr hx)]
        simp only [← mul_apply, ← zpow_add_one, ← zpow_one_add, add_comm]
      intro x hx
      have hix := Perm.congr_fun hi ⟨x, hx⟩
      simp only [← Subtype.coe_inj, subtypePermOfSupport, subtypePerm_apply,
        subtypePerm_apply_zpow_of_mem] at hix
      exact hix.symm

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
⊢ Commute g c ↔ ∃ (hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support), ofSubtype (g.subtypePerm hc') ∈ Subgroup.zpowers c

Tactic:
simp_rw [hc.commute_iff', Subgroup.mem_zpowers_iff]

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
⊢ (∃ (h : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support), ∃ k, c.subtypePermOfSupport ^ k = g.subtypePerm ⋯) ↔
    ∃ (h : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support), ∃ k, c ^ k = ofSubtype (g.subtypePerm ⋯)
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j, Fintype.card (H ↑j)
⊢ f ∈ ⊥

Tactic:
change f = 1

Goal state after:
case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ x, (ϕ ↑x).range)
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf : (noncommPiCoprod (fun x ↦ ϕ ↑x) ⋯) g = f
g' : H i
hg'f : (ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j, Fintype.card (H ↑j)
⊢ f = 1
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
⊢ iSupIndep fun i ↦ (ϕ i).range

Tactic:
cases nonempty_fintype ι
  let := Classical.decEq ι
  rintro i
  rw [disjoint_iff_inf_le]
  rintro f ⟨hxi, hxp⟩
  dsimp at hxi hxp
  rw [iSup_subtype', ← noncommPiCoprod_range] at hxp
  rotate_left
  · intro _ _ hj
    apply hcomm
    exact hj ∘ Subtype.ext
  obtain ⟨g, hgf⟩ := hxp
  obtain ⟨g', hg'f⟩ := hxi
  have hxi : orderOf f ∣ Fintype.card (H i) := by
    rw [← hg'f]
    exact (orderOf_map_dvd _ _).trans orderOf_dvd_card
  have hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H j) := by
    rw [← hgf, ← Fintype.card_pi]
    exact (orderOf_map_dvd _ _).trans orderOf_dvd_card
  change f = 1
  rw [← pow_one f, ← orderOf_dvd_iff_pow_eq_one]
  obtain ⟨c, hc⟩ := Nat.dvd_gcd hxp hxi
  use c
  rw [← hc]
  symm
  rw [← Nat.coprime_iff_gcd_eq_one, Nat.coprime_fintype_prod_left_iff, Subtype.forall]
  intro j h
  exact hcoprime h

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
hind : iSupIndep H
⊢ Function.Injective ⇑(noncommPiCoprod hcomm)

Tactic:
apply MonoidHom.injective_noncommPiCoprod_of_iSupIndep
  · simpa using hind
  · intro i
    exact Subtype.coe_injective

Goal state after:
Module: Mathlib.GroupTheory.Perm.Option

Goal state before:
pp: case some
α : Type u_1
inst✝ : DecidableEq α
x y i a✝ : α
⊢ (optionCongr (swap x y)) (some i) = some a✝ ↔ (swap (some x) (some y)) (some i) = some a✝

Tactic:
by_cases hx : i = x

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
x y i a✝ : α
hx : i = x
⊢ (optionCongr (swap x y)) (some i) = some a✝ ↔ (swap (some x) (some y)) (some i) = some a✝

case neg
α : Type u_1
inst✝ : DecidableEq α
x y i a✝ : α
hx : ¬i = x
⊢ (optionCongr (swap x y)) (some i) = some a✝ ↔ (swap (some x) (some y)) (some i) = some a✝
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ^ 2 = 1
⊢ (if Odd 2 then 1 else (-1) ^ ((Fintype.card α - Fintype.card ↑(Function.fixedPoints ⇑σ)) / 2)) =
    (-1) ^ ((Fintype.card α - Fintype.card ↑(Function.fixedPoints ⇑σ)) / 2)

Tactic:
if_neg (Nat.not_odd_iff.mpr rfl)

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ^ 2 = 1
⊢ (-1) ^ ((Fintype.card α - Fintype.card ↑(Function.fixedPoints ⇑σ)) / 2) =
    (-1) ^ ((Fintype.card α - Fintype.card ↑(Function.fixedPoints ⇑σ)) / 2)
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
σ : Perm α
h1 : Nat.Prime (Fintype.card α)
h2 : orderOf σ = Fintype.card α
⊢ 1 * Fintype.card α < 2 * orderOf σ

Tactic:
← h2,

Goal state after:
α : Type u_1
inst✝ : Fintype α
σ : Perm α
h1 : Nat.Prime (Fintype.card α)
h2 : orderOf σ = Fintype.card α
⊢ 1 * orderOf σ < 2 * orderOf σ
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
⊢ ¬g.cycleOf x = 1 ↔ g x ≠ x

Tactic:
cycleOf_eq_one_iff

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
⊢ ¬g x = x ↔ g x ≠ x
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
⊢ σ.cycleType.sum = 3

Tactic:
h.cycleType,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
⊢ {3}.sum = 3
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
⊢ σ.cycleType.card = 1

Tactic:
h.cycleType,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
⊢ {3}.card = 1
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.add_zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (x.add zero) = descFunLift F s x

Tactic:
dsimp; rw [add_zero]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.add_zero
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ descFunLift F s (x.add zero) = descFunLift F s x

Tactic:
dsimp; rw [add_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
e e' : m ≃ n
M : Matrix m m R
⊢ ((reindex (e.trans e'.symm) (Equiv.refl m)) M).det = ↑↑(sign (e'.trans e.symm)) * M.det

Tactic:
reindex_apply,

Goal state after:
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
e e' : m ≃ n
M : Matrix m m R
⊢ (M.submatrix ⇑(e.trans e'.symm).symm ⇑(Equiv.refl m).symm).det = ↑↑(sign (e'.trans e.symm)) * M.det
Module: Mathlib.Algebra.Category.Grp.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ GrpCat
x : ↑(G F)
⊢ ↑(G F)

Tactic:
by
    refine Quot.lift (colimitInvAux.{v, u} F) ?_ x
    intro x y h
    apply colimitInvAux_eq_of_rel
    apply Types.FilteredColimit.rel_of_colimitTypeRel
    exact h

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j₁ : J
x : ↑(F.obj j₁)
j₂ : J
y : ↑(F.obj j₂)
j₃ : J
x' : ↑(F.obj j₃)
l : J
f : ⟨j₁, x⟩.fst ⟶ l
g : ⟨j₃, x'⟩.fst ⟶ l
hfg : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) x'
⊢ colimitMulAux F ⟨j₁, x⟩ ⟨j₂, y⟩ = colimitMulAux F ⟨j₃, x'⟩ ⟨j₂, y⟩

Tactic:
obtain ⟨s, α, β, γ, h₁, h₂, h₃⟩ :=
    IsFiltered.tulip (IsFiltered.leftToMax j₁ j₂) (IsFiltered.rightToMax j₁ j₂)
      (IsFiltered.rightToMax j₃ j₂) (IsFiltered.leftToMax j₃ j₂) f g

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
j₁ : J
x : ↑(F.obj j₁)
j₂ : J
y : ↑(F.obj j₂)
j₃ : J
x' : ↑(F.obj j₃)
l : J
f : ⟨j₁, x⟩.fst ⟶ l
g : ⟨j₃, x'⟩.fst ⟶ l
hfg : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) x'
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : l ⟶ s
γ : IsFiltered.max j₃ j₂ ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = IsFiltered.rightToMax j₃ j₂ ≫ γ
h₃ : IsFiltered.leftToMax j₃ j₂ ≫ γ = g ≫ β
⊢ colimitMulAux F ⟨j₁, x⟩ ⟨j₂, y⟩ = colimitMulAux F ⟨j₃, x'⟩ ⟨j₂, y⟩
Module: Mathlib.Algebra.Category.MonCat.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
t : Cocone F
i : J
x : ↑(F.obj i)
j : J
y : ↑(F.obj j)
⊢ (F ⋙ forget MonCat).descColimitType ((F ⋙ forget MonCat).coconeTypesEquiv.symm ((forget MonCat).mapCocone t))
      (M.mk F ⟨i, x⟩ * M.mk F ⟨j, y⟩) =
    (F ⋙ forget MonCat).descColimitType ((F ⋙ forget MonCat).coconeTypesEquiv.symm ((forget MonCat).mapCocone t))
        (M.mk F ⟨i, x⟩) *
      (F ⋙ forget MonCat).descColimitType ((F ⋙ forget MonCat).coconeTypesEquiv.symm ((forget MonCat).mapCocone t))
        (M.mk F ⟨j, y⟩)

Tactic:
colimit_mul_mk_eq F ⟨i, x⟩ ⟨j, y⟩ (max' i j) (IsFiltered.leftToMax i j)
        (IsFiltered.rightToMax i j)

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ MonCat
inst✝ : IsFiltered J
t : Cocone F
i : J
x : ↑(F.obj i)
j : J
y : ↑(F.obj j)
⊢ (F ⋙ forget MonCat).descColimitType ((F ⋙ forget MonCat).coconeTypesEquiv.symm ((forget MonCat).mapCocone t))
      (M.mk F
        ⟨IsFiltered.max i j,
          (ConcreteCategory.hom (F.map (IsFiltered.leftToMax i j))) ⟨i, x⟩.snd *
            (ConcreteCategory.hom (F.map (IsFiltered.rightToMax i j))) ⟨j, y⟩.snd⟩) =
    (F ⋙ forget MonCat).descColimitType ((F ⋙ forget MonCat).coconeTypesEquiv.symm ((forget MonCat).mapCocone t))
        (M.mk F ⟨i, x⟩) *
      (F ⋙ forget MonCat).descColimitType ((F ⋙ forget MonCat).coconeTypesEquiv.symm ((forget MonCat).mapCocone t))
        (M.mk F ⟨j, y⟩)