mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup G s = Subgroup.map (stabilizer G a).subtype (fixingSubgroup (↥(stabilizer G a)) t)
this : a ∉ Subtype.val '' t
⊢ t.ncard = (Subtype.val '' t).ncard

Tactic:
Set.ncard_image_of_injective _ Subtype.coe_injective

Goal state after:
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
hGX : IsPretransitive G α
a : α
has : a ∈ s
t : Set ↥(ofStabilizer G a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup G s = Subgroup.map (stabilizer G a).subtype (fixingSubgroup (↥(stabilizer G a)) t)
this : a ∉ Subtype.val '' t
⊢ t.ncard = t.ncard
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s✝ s t : Set α
x : ↥(ofFixingSubgroup M (s ∪ t))
hx : ⟨↑x, ⋯⟩ ∈ Subtype.val ⁻¹' t
⊢ ↑x ∈ s ∪ t

Tactic:
apply Set.mem_union_right s
          simpa only [Set.mem_preimage, Subtype.coe_mk] using hx

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
G : Subgroup (Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Nat.card α - 1)
this : Fintype α
⊢ G = ⊤

Tactic:
simp only [Nat.card_eq_fintype_card] at hmt

Goal state after:
α : Type u_1
inst✝ : Finite α
G : Subgroup (Perm α)
this : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
⊢ G = ⊤
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
s : Set α
n : ℕ
inst✝ : Finite ↑s
x : Fin n ↪ ↥(ofFixingSubgroup M s)
i : Fin s.ncard
⊢ let Hs := ⋯;
  (append x) (Fin.castAdd n i) = ↑((Classical.choice Hs) i)

Tactic:
by
  simp [ofFixingSubgroup.append]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
s : Set α
n : ℕ
inst✝ : Finite ↑s
x : Fin n ↪ ↥(ofFixingSubgroup M s)
i : Fin n
⊢ (append x) (Fin.natAdd s.ncard i) = ↑(x i)

Tactic:
by
  simp [ofFixingSubgroup.append]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : Finite α
G : Subgroup (Perm α)
this : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j✝ : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := castLEEmb ⋯
k : Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := (Fintype.equivFinOfCardEq ⋯).symm.toEmbedding
x' : Fin (Fintype.card α - 1) ↪ α := j✝.trans x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
hj : ↑j < Fintype.card α - 1
⊢ (g • x) i = (k • x) i

pp: case inr.inr
α : Type u_1
inst✝ : Finite α
G : Subgroup (Perm α)
this : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j✝ : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := castLEEmb ⋯
k : Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := (Fintype.equivFinOfCardEq ⋯).symm.toEmbedding
x' : Fin (Fintype.card α - 1) ↪ α := j✝.trans x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
hj : ↑j = Fintype.card α - 1
⊢ (g • x) i = (k • x) i

Tactic:
· suffices i = j by
          rw [← this, ← hi] at hj
          exact (lt_irrefl _ hj).elim
        apply EmbeddingLike.injective (g • x)
        rw [hgk' j hj, hxj]

Goal state after:
case inr.inr
α : Type u_1
inst✝ : Finite α
G : Subgroup (Perm α)
this : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j✝ : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := castLEEmb ⋯
k : Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := (Fintype.equivFinOfCardEq ⋯).symm.toEmbedding
x' : Fin (Fintype.card α - 1) ↪ α := j✝.trans x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
hj : ↑j = Fintype.card α - 1
⊢ (g • x) i = (k • x) i
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this✝¹ : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this✝ : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
h : Equiv.Perm.sign g = -1
this : (Finset.image (⇑x) Finset.univ)ᶜ.card = 2
a b : α
hab : a ≠ b
hs : (Finset.image (⇑x) Finset.univ)ᶜ = {a, b}
⊢ ⟨g * Equiv.swap a b, ⋯⟩ • x = y

Tactic:
ext i

Goal state after:
case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h2 : 2 ≤ Nat.card α
h2le : Nat.card α - 2 ≤ Nat.card α
this✝¹ : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α)
this✝ : IsMultiplyPretransitive (Equiv.Perm α) α (Nat.card α - 2)
x y : Fin (Nat.card α - 2) ↪ α
g : Equiv.Perm α
hg : g • x = y
h : Equiv.Perm.sign g = -1
this : (Finset.image (⇑x) Finset.univ)ᶜ.card = 2
a b : α
hab : a ≠ b
hs : (Finset.image (⇑x) Finset.univ)ᶜ = {a, b}
i : Fin (Nat.card α - 2)
⊢ (⟨g * Equiv.swap a b, ⋯⟩ • x) i = y i
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Nat.card α
h3 : Nat.card α = 3
this : IsPretransitive (↥(alternatingGroup α)) α
⊢ IsTrivialBlock B

Tactic:
have : IsPreprimitive (alternatingGroup α) α := IsPreprimitive.of_prime_card (h3 ▸ prime_three)

Goal state after:
case inr.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Nat.card α
h3 : Nat.card α = 3
this✝ : IsPretransitive (↥(alternatingGroup α)) α
this : IsPreprimitive (↥(alternatingGroup α)) α
⊢ IsTrivialBlock B
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : 2 < s.ncard
⊢ ∃ g ∈ stabilizer (Perm α) s, g.IsThreeCycle

Tactic:
rw [two_lt_ncard_iff] at hs
  obtain ⟨a, b, c, ha, hb, hc, hab, hac, hbc⟩ := hs
  refine ⟨swap a b * swap a c, ?_, isThreeCycle_swap_mul_swap_same hab hac hbc⟩
  rw [mem_stabilizer_set_iff_subset_smul_set s.toFinite, subset_smul_set_iff]
  rintro _ ⟨x, hx, rfl⟩
  aesop

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : 2 < s.ncard
⊢ ∃ g ∈ stabilizer (Perm α) s, g.IsThreeCycle

Tactic:
by
  rw [two_lt_ncard_iff] at hs
  obtain ⟨a, b, c, ha, hb, hc, hab, hac, hbc⟩ := hs
  refine ⟨swap a b * swap a c, ?_, isThreeCycle_swap_mul_swap_same hab hac hbc⟩
  rw [mem_stabilizer_set_iff_subset_smul_set s.toFinite, subset_smul_set_iff]
  rintro _ ⟨x, hx, rfl⟩
  aesop

Goal state after:
Module: Mathlib.GroupTheory.GroupExtension.Defs

Goal state before:
pp: N : Type u_1
E : Type u_2
G : Type u_3
inst✝³ : Group N
inst✝² : Group E
inst✝¹ : Group G
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
x✝² x✝¹ : S.Equiv S'
toMulEquiv✝¹ : E ≃* E'
inl_comm✝¹ : ⇑toMulEquiv✝¹ ∘ ⇑S.inl = ⇑S'.inl
rightHom_comm✝¹ : ⇑S'.rightHom ∘ ⇑toMulEquiv✝¹ = ⇑S.rightHom
toMulEquiv✝ : E ≃* E'
inl_comm✝ : ⇑toMulEquiv✝ ∘ ⇑S.inl = ⇑S'.inl
rightHom_comm✝ : ⇑S'.rightHom ∘ ⇑toMulEquiv✝ = ⇑S.rightHom
h :
  ⇑{ toMulEquiv := toMulEquiv✝¹, inl_comm := inl_comm✝¹, rightHom_comm := rightHom_comm✝¹ }.toMulEquiv =
    ⇑{ toMulEquiv := toMulEquiv✝, inl_comm := inl_comm✝, rightHom_comm := rightHom_comm✝ }.toMulEquiv
x✝ :
  ⇑{ toMulEquiv := toMulEquiv✝¹, inl_comm := inl_comm✝¹, rightHom_comm := rightHom_comm✝¹ }.symm =
    ⇑{ toMulEquiv := toMulEquiv✝, inl_comm := inl_comm✝, rightHom_comm := rightHom_comm✝ }.symm
⊢ toMulEquiv✝¹ = toMulEquiv✝

Tactic:
rw [MulEquiv.ext_iff]

Goal state after:
N : Type u_1
E : Type u_2
G : Type u_3
inst✝³ : Group N
inst✝² : Group E
inst✝¹ : Group G
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
x✝² x✝¹ : S.Equiv S'
toMulEquiv✝¹ : E ≃* E'
inl_comm✝¹ : ⇑toMulEquiv✝¹ ∘ ⇑S.inl = ⇑S'.inl
rightHom_comm✝¹ : ⇑S'.rightHom ∘ ⇑toMulEquiv✝¹ = ⇑S.rightHom
toMulEquiv✝ : E ≃* E'
inl_comm✝ : ⇑toMulEquiv✝ ∘ ⇑S.inl = ⇑S'.inl
rightHom_comm✝ : ⇑S'.rightHom ∘ ⇑toMulEquiv✝ = ⇑S.rightHom
h :
  ⇑{ toMulEquiv := toMulEquiv✝¹, inl_comm := inl_comm✝¹, rightHom_comm := rightHom_comm✝¹ }.toMulEquiv =
    ⇑{ toMulEquiv := toMulEquiv✝, inl_comm := inl_comm✝, rightHom_comm := rightHom_comm✝ }.toMulEquiv
x✝ :
  ⇑{ toMulEquiv := toMulEquiv✝¹, inl_comm := inl_comm✝¹, rightHom_comm := rightHom_comm✝¹ }.symm =
    ⇑{ toMulEquiv := toMulEquiv✝, inl_comm := inl_comm✝, rightHom_comm := rightHom_comm✝ }.symm
⊢ ∀ (x : E), toMulEquiv✝¹ x = toMulEquiv✝ x
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : MulAction G α
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : ↑(powersetCard α n)
a : α
⊢ a ∈ ↑(((mulActionHom_compl G α ⋯).comp (mulActionHom_compl G α hm)) s) ↔ a ∈ ↑((MulActionHom.id G) s)

Tactic:
change a ∈ (mulActionHom_compl G α _).comp (mulActionHom_compl G α hm) s ↔ a ∈ s

Goal state after:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : MulAction G α
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : ↑(powersetCard α n)
a : α
⊢ a ∈ ((mulActionHom_compl G α ⋯).comp (mulActionHom_compl G α hm)) s ↔ a ∈ s
Module: Mathlib.GroupTheory.IndexNSmul

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module.Finite ℤ M
inst✝¹ : IsTorsionFree ℤ M
A : AddSubgroup M
inst✝ : A.FiniteIndex
this : finrank ℤ ↥(DistribSMul.toLinearMap ℤ M A.index).range = finrank ℤ M
⊢ finrank ℤ ↥(DistribSMul.toLinearMap ℤ M A.index).range ≤ finrank ℤ ↥A

Tactic:
refine Submodule.finrank_mono <| (OrderIso.symm_apply_le toIntSubmodule).mp fun m hm ↦ ?_

Goal state after:
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module.Finite ℤ M
inst✝¹ : IsTorsionFree ℤ M
A : AddSubgroup M
inst✝ : A.FiniteIndex
this : finrank ℤ ↥(DistribSMul.toLinearMap ℤ M A.index).range = finrank ℤ M
m : M
hm : m ∈ toIntSubmodule.symm (DistribSMul.toLinearMap ℤ M A.index).range
⊢ m ∈ A
Module: Mathlib.GroupTheory.MonoidLocalization.Order

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s) (a₁, a₂) (b₁, b₂)
hcd : (r s) (c₁, c₂) (d₁, d₂)
e f : ↥s
he : ↑b₂ * a₁ = ↑a₂ * b₁
hf : ↑d₂ * c₁ = ↑c₂ * d₁
⊢ ?a * (↑d₂ * a₁) ≤ ?a * (↑a₂ * d₁) ↔ ↑d₂ * b₁ ≤ ↑b₂ * d₁

pp: case a
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s) (a₁, a₂) (b₁, b₂)
hcd : (r s) (c₁, c₂) (d₁, d₂)
e f : ↥s
he : ↑b₂ * a₁ = ↑a₂ * b₁
hf : ↑d₂ * c₁ = ↑c₂ * d₁
⊢ α

Tactic:
mul_left_comm,

Goal state after:
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s) (a₁, a₂) (b₁, b₂)
hcd : (r s) (c₁, c₂) (d₁, d₂)
e f : ↥s
he : ↑b₂ * a₁ = ↑a₂ * b₁
hf : ↑d₂ * c₁ = ↑c₂ * d₁
⊢ ↑d₂ * (?a * a₁) ≤ ?a * (↑a₂ * d₁) ↔ ↑d₂ * b₁ ≤ ↑b₂ * d₁

case a
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s) (a₁, a₂) (b₁, b₂)
hcd : (r s) (c₁, c₂) (d₁, d₂)
e f : ↥s
he : ↑b₂ * a₁ = ↑a₂ * b₁
hf : ↑d₂ * c₁ = ↑c₂ * d₁
⊢ α
Module: Mathlib.GroupTheory.MonoidLocalization.Order

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s) (a₁, a₂) (b₁, b₂)
hcd : (r s) (c₁, c₂) (d₁, d₂)
e f : ↥s
he : ↑b₂ * a₁ = ↑a₂ * b₁
hf : ↑d₂ * c₁ = ↑c₂ * d₁
⊢ ↑d₂ * (↑a₂ * b₁) ≤ ↑b₂ * (↑a₂ * d₁) ↔ ↑d₂ * b₁ ≤ ↑b₂ * d₁

Tactic:
mul_left_comm,

Goal state after:
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s) (a₁, a₂) (b₁, b₂)
hcd : (r s) (c₁, c₂) (d₁, d₂)
e f : ↥s
he : ↑b₂ * a₁ = ↑a₂ * b₁
hf : ↑d₂ * c₁ = ↑c₂ * d₁
⊢ ↑a₂ * (↑d₂ * b₁) ≤ ↑b₂ * (↑a₂ * d₁) ↔ ↑d₂ * b₁ ≤ ↑b₂ * d₁
Module: Mathlib.GroupTheory.MonoidLocalization.Order

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s) (a₁, a₂) (b₁, b₂)
hcd : (r s) (c₁, c₂) (d₁, d₂)
e f : ↥s
he : ↑b₂ * a₁ = ↑a₂ * b₁
hf : ↑d₂ * c₁ = ↑c₂ * d₁
⊢ ?a * (↑d₂ * a₁) < ?a * (↑a₂ * d₁) ↔ ↑d₂ * b₁ < ↑b₂ * d₁

pp: case a
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s) (a₁, a₂) (b₁, b₂)
hcd : (r s) (c₁, c₂) (d₁, d₂)
e f : ↥s
he : ↑b₂ * a₁ = ↑a₂ * b₁
hf : ↑d₂ * c₁ = ↑c₂ * d₁
⊢ α

Tactic:
mul_left_comm,

Goal state after:
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s) (a₁, a₂) (b₁, b₂)
hcd : (r s) (c₁, c₂) (d₁, d₂)
e f : ↥s
he : ↑b₂ * a₁ = ↑a₂ * b₁
hf : ↑d₂ * c₁ = ↑c₂ * d₁
⊢ ↑d₂ * (?a * a₁) < ?a * (↑a₂ * d₁) ↔ ↑d₂ * b₁ < ↑b₂ * d₁

case a
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s) (a₁, a₂) (b₁, b₂)
hcd : (r s) (c₁, c₂) (d₁, d₂)
e f : ↥s
he : ↑b₂ * a₁ = ↑a₂ * b₁
hf : ↑d₂ * c₁ = ↑c₂ * d₁
⊢ α
Module: Mathlib.GroupTheory.MonoidLocalization.Order

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s) (a₁, a₂) (b₁, b₂)
hcd : (r s) (c₁, c₂) (d₁, d₂)
e f : ↥s
he : ↑b₂ * a₁ = ↑a₂ * b₁
hf : ↑d₂ * c₁ = ↑c₂ * d₁
⊢ ↑d₂ * (↑a₂ * b₁) < ↑b₂ * (↑a₂ * d₁) ↔ ↑d₂ * b₁ < ↑b₂ * d₁

Tactic:
mul_left_comm,

Goal state after:
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁✝ b₁✝ : α
a₂✝ b₂✝ : ↥s
a b : Localization s
a₁ b₁ : α
a₂ b₂ : ↥s
c₁ d₁ : α
c₂ d₂ : ↥s
hab : (r s) (a₁, a₂) (b₁, b₂)
hcd : (r s) (c₁, c₂) (d₁, d₂)
e f : ↥s
he : ↑b₂ * a₁ = ↑a₂ * b₁
hf : ↑d₂ * c₁ = ↑c₂ * d₁
⊢ ↑a₂ * (↑d₂ * b₁) < ↑b₂ * (↑a₂ * d₁) ↔ ↑d₂ * b₁ < ↑b₂ * d₁
Module: Mathlib.GroupTheory.MonoidLocalization.Order

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a✝ b✝ c✝ : Localization s
a b c : α × ↥s
hab : ↑b.2 * a.1 ≤ ↑a.2 * b.1
hbc : ↑c.2 * b.1 ≤ ↑b.2 * c.1
⊢ ↑b.2 * (↑c.2 * a.1) ≤ ↑b.2 * (↑a.2 * c.1)

Tactic:
mul_left_comm,

Goal state after:
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a✝ b✝ c✝ : Localization s
a b c : α × ↥s
hab : ↑b.2 * a.1 ≤ ↑a.2 * b.1
hbc : ↑c.2 * b.1 ≤ ↑b.2 * c.1
⊢ ↑c.2 * (↑b.2 * a.1) ≤ ↑b.2 * (↑a.2 * c.1)
Module: Mathlib.GroupTheory.MonoidLocalization.Order

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a✝ b✝ c✝ : Localization s
a b c : α × ↥s
hab : ↑b.2 * a.1 ≤ ↑a.2 * b.1
hbc : ↑c.2 * b.1 ≤ ↑b.2 * c.1
⊢ ↑c.2 * (↑a.2 * b.1) ≤ ↑b.2 * (↑a.2 * c.1)

Tactic:
mul_left_comm,

Goal state after:
α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
a✝ b✝ c✝ : Localization s
a b c : α × ↥s
hab : ↑b.2 * a.1 ≤ ↑a.2 * b.1
hbc : ↑c.2 * b.1 ≤ ↑b.2 * c.1
⊢ ↑a.2 * (↑c.2 * b.1) ≤ ↑b.2 * (↑a.2 * c.1)
Module: Mathlib.GroupTheory.Perm.DomMulAct

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a // f a = i }
a : α
⊢ f ((stabilizerEquiv_invFun_aux g) a) = f a

Tactic:
apply comp_stabilizerEquiv_invFun

Goal state after:
Module: Mathlib.GroupTheory.ResiduallyFinite

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : ResiduallyFinite G
g h : G
hgh : g ≠ h
H : FiniteIndexNormalSubgroup G
hH : g⁻¹ * h ∉ H
⊢ ∃ H, ↑g ≠ ↑h

Tactic:
exact ⟨H, by simpa [QuotientGroup.eq]⟩

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
i : ι
⊢ (of i).comp (φ i) = base φ

Tactic:
ext x
  apply (Con.eq _).2
  refine ConGen.Rel.of _ _ ?_
  simp only [MonoidHom.comp_apply]
  exact ⟨_, _, rfl, rfl⟩

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
this : Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3
comm_le : commutator ↥(alternatingGroup α) ≤ kleinFour α
⊢ kleinFour α = commutator ↥(alternatingGroup α)

Tactic:
have comm_ne_bot : commutator (alternatingGroup α) ≠ ⊥ := by
    rw [ne_eq, commutator_eq_bot_iff_center_eq_top,
      center_eq_bot (le_of_eq hα4.symm)]
    apply @bot_ne_top _ _ _ ?_
    rw [Subgroup.nontrivial_iff, ← Finite.one_lt_card_iff_nontrivial,
      card_of_card_eq_four hα4]
    simp

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
x✝ : (kleinFour α).Normal
this : Nat.card (↥(alternatingGroup α) ⧸ kleinFour α) = 3
comm_le : commutator ↥(alternatingGroup α) ≤ kleinFour α
comm_ne_bot : commutator ↥(alternatingGroup α) ≠ ⊥
⊢ kleinFour α = commutator ↥(alternatingGroup α)
Module: Mathlib.GroupTheory.SpecificGroups.Quaternion

Goal state before:
pp: case hnot
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
h' : ↑n = 0
⊢ False

Tactic:
apply_fun ZMod.val at h'

Goal state after:
case hnot
n : ℕ
inst✝ : NeZero n
i : ZMod (2 * n)
this : Fact (Nat.Prime 2)
h' : (↑n).val = ZMod.val 0
⊢ False
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
⊢ ∀ (x y z : Hamming β), dist x z ≤ dist x y + dist y z

Tactic:
by
    push_cast
    exact mod_cast hammingDist_triangle

Goal state after:
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: case mpr
α : Type u_1
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
s : Set (Hamming β × Hamming β)
⊢ (∃ ε > 0, ∀ {a b : Hamming β}, ↑(hammingDist (ofHamming a) (ofHamming b)) < ε → (a, b) ∈ s) →
    s ∈ uniformity (Hamming β)

Tactic:
· rintro ⟨_, hε, hs⟩ ⟨_, _⟩ rfl
      refine hs (lt_of_eq_of_lt ?_ hε)
      exact mod_cast hammingDist_self _

Goal state after:
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure (κ a)
h' : μ ≠ 0
⊢ ∃ s, MeasurableSet s ∧ μ s = 0 ∧ ∀ a ∉ s, IsProbabilityMeasure (κ a)

Tactic:
by
    refine ⟨toMeasurable μ {a | ¬ IsProbabilityMeasure (κ a)}, measurableSet_toMeasurable _ _,
      by simpa [measure_toMeasurable] using! h, ?_⟩
    intro a ha
    contrapose ha
    exact subset_toMeasurable _ _ ha

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: case pos.h_ind
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
⊢ ∀ (c : E) ⦃s : Set (β × γ)⦄,
    MeasurableSet s →
      ((κ ⊗ₖ η) a) s < ∞ →
        ∫ (z : β × γ), s.indicator (fun x ↦ c) z ∂(κ ⊗ₖ η) a =
          ∫ (x : β), ∫ (y : γ), s.indicator (fun x ↦ c) (x, y) ∂η (a, x) ∂κ a

Tactic:
intro c s hs h2s
    simp_rw [integral_indicator hs, ← indicator_comp_right, Function.comp_def,
      integral_indicator (measurable_prodMk_left hs), MeasureTheory.setIntegral_const,
      integral_smul_const, measureReal_def]
    congr 1
    rw [integral_toReal]
    rotate_left
    · exact (Kernel.measurable_kernel_prodMk_left' hs _).aemeasurable
    · exact ae_kernel_lt_top a h2s.ne
    rw [Kernel.compProd_apply hs]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Tilted

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : NeZero μ
hf : Integrable (fun x ↦ rexp (f x)) μ
⊢ ENNReal.ofReal (∫ (x : α), rexp (f x) ∂μ) * (ENNReal.ofReal (∫ (x : α), rexp (f x) ∂μ))⁻¹ = 1

Tactic:
ENNReal.mul_inv_cancel

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : NeZero μ
hf : Integrable (fun x ↦ rexp (f x)) μ
⊢ 1 = 1

case h0
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : NeZero μ
hf : Integrable (fun x ↦ rexp (f x)) μ
⊢ ENNReal.ofReal (∫ (x : α), rexp (f x) ∂μ) ≠ 0

case ht
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : NeZero μ
hf : Integrable (fun x ↦ rexp (f x)) μ
⊢ ENNReal.ofReal (∫ (x : α), rexp (f x) ∂μ) ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Goal state before:
pp: 𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
inst✝² : IsFiniteMeasure μ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsFiniteKernel η
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
s : Set 𝓧
hs : MeasurableSet s
hsμ : μ s < ∞
⊢ ∫⁻ (a : 𝓧) in s, ∫⁻ (b : 𝓨) in univ, (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂η a ∂μ = ∫⁻ (a : 𝓧) in s, (κ a) univ ∂μ

Tactic:
by
    rw [← Measure.setLIntegral_compProd (by fun_prop) hs .univ, Measure.setLIntegral_rnDeriv hκη,
      Measure.compProd_apply_prod hs .univ]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.IntegralCompProd

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : NormedAddCommGroup E
κ : Kernel α β
μ : Measure α
f : β → E
hf : AEStronglyMeasurable f (⇑κ ∘ₘ μ)
⊢ AEStronglyMeasurable f ((κ ∘ₖ Kernel.const Unit μ) ())

Tactic:
· simpa [Kernel.comp_apply]

Goal state after: