mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l l' : List α
⊢ (l ++ l').rotate l.length = l' ++ l

Tactic:
rotate_eq_rotate'

Goal state after:
α : Type u
l l' : List α
⊢ (l ++ l').rotate' l.length = l' ++ l
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ l.rotate n ~ l

Tactic:
rotate_eq_rotate'

Goal state after:
α : Type u
l : List α
n : ℕ
⊢ l.rotate' n ~ l
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case cons
α : Type u_1
inst✝ : LinearOrder α
a : α
as : List α
ha : IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
b : α
bs : List α
hm : IsChain (fun x1 x2 ↦ x1 > x2) (b :: bs)
hmas : b :: bs ≤ as
⊢ IsChain (fun x1 x2 ↦ x1 > x2) (a :: b :: bs)

Tactic:
apply hm.cons_cons
    cases as with
    | nil =>
      simp only [le_iff_lt_or_eq, reduceCtorEq, or_false] at hmas
      exact (List.not_lt_nil _ hmas).elim
    | cons a' as =>
      rw [List.isChain_cons_cons] at ha
      refine lt_of_le_of_lt ?_ ha.1
      rw [le_iff_lt_or_eq] at hmas
      rcases hmas with hmas | hmas
      · exact head_le_of_lt hmas
      · simp_all only [List.cons.injEq, le_refl]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: l : List ℤ
h : l.prod = -1
⊢ -1 ≠ 1

Tactic:
by decide

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: l : List ℤ
h : l.prod = -1
x : ℤ
h₁ : x ∈ l
h₂ : x ≠ 1
⊢ -1 * -1 = 1

Tactic:
by decide

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
F : Type u_8
inst✝¹ : FunLike F M Nᵐᵒᵖ
inst✝ : MonoidHomClass F M Nᵐᵒᵖ
f : F
l : List M
⊢ MulOpposite.unop (map (⇑f) l).prod = (map (MulOpposite.unop ∘ ⇑f) l).reverse.prod

Tactic:
MulOpposite.unop_list_prod,

Goal state after:
M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
F : Type u_8
inst✝¹ : FunLike F M Nᵐᵒᵖ
inst✝ : MonoidHomClass F M Nᵐᵒᵖ
f : F
l : List M
⊢ (map MulOpposite.unop (map (⇑f) l)).reverse.prod = (map (MulOpposite.unop ∘ ⇑f) l).reverse.prod
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ l[k] = (l.rotate n)[(l.length - n % l.length + k) % l.length]

Tactic:
rw [getElem_rotate]
  refine congr_arg l.get (Fin.eq_of_val_eq ?_)
  simp only [mod_add_mod]
  rw [← add_mod_mod, Nat.add_right_comm, Nat.sub_add_cancel, add_mod_left, mod_eq_of_lt]
  exacts [hk, (mod_lt _ (k.zero_le.trans_lt hk)).le]

Goal state after:
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case mp
α : Type u
l l' : List α
⊢ l.reverse ~r l' → l ~r l'.reverse

Tactic:
intro h

Goal state after:
case mp
α : Type u
l l' : List α
h : l.reverse ~r l'
⊢ l ~r l'.reverse
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case mpr
α : Type u
l l' : List α
⊢ l ~r l'.reverse → l.reverse ~r l'

Tactic:
intro h

Goal state after:
case mpr
α : Type u
l l' : List α
h : l ~r l'.reverse
⊢ l.reverse ~r l'
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: ⊢ (0 + 1) * choose 0 0 = (0 + 1).choose (0 + 1) * (0 + 1)

Tactic:
by decide

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k s : ℕ
hsk : s ≤ k
⊢ n.choose k * k.choose s = n.choose s * (n - s).choose (k - s)

Tactic:
by
  obtain hnk | hkn := lt_or_ge n k
  · grind
  have h : 0 < (n - k)! * (k - s)! * s ! := by apply_rules [factorial_pos, Nat.mul_pos]
  apply Nat.mul_right_cancel h
  calc
    _ = n.choose s * s ! * ((n - s).choose (k - s) * (k - s)! * (n - s - (k - s))!) := by
      grind [choose_mul_factorial_mul_factorial]
    _ = n.choose s * (n - s).choose (k - s) * ((n - k)! * (k - s)! * s !) := by
      grind

Goal state after:
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a : α
b : δ a
s : Multiset α
hs : ¬a ∈ s
f₁ f₂ : (a : α) → a ∈ s → δ a
eq : cons s a b f₁ = cons s a b f₂
a' : α
h' : a' ∈ s
ne : a ≠ a'
this : a' ∈ a ::ₘ s
⊢ cons s a b f₁ a' this = cons s a b f₂ a' this

Tactic:
by rw [eq]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n : ℕ
⊢ (n + 1 + 1).choose (n + 1) = n + 1 + 1

Tactic:
rw [choose_succ_succ, choose_succ_self_right n, choose_self]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + 1).ascFactorial k = k ! * (n + k).choose k

Tactic:
rw [Nat.mul_comm]
  apply Nat.mul_right_cancel (n + k - k).factorial_pos
  rw [choose_mul_factorial_mul_factorial <| Nat.le_add_left k n, Nat.add_sub_cancel_right,
    ← factorial_mul_ascFactorial, Nat.mul_comm]

Goal state after:
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
s✝ : Multiset α
t : (a : α) → Multiset (β a)
a : α
s : Multiset α
ih : s.Nodup → (∀ (a : α), a ∈ s → (t a).Nodup) → (s.pi t).Nodup
hs✝ : (a ::ₘ s).Nodup
ht : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → (t a_1).Nodup
has : ¬a ∈ s
hs : s.Nodup
b₁ : β a
x✝³ : b₁ ∈ t a
b₂ : β a
x✝² : b₂ ∈ t a
neb : b₁ ≠ b₂
f : (a : α) → a ∈ s → β a
x✝¹ : f ∈ s.pi t
g : (a : α) → a ∈ s → β a
x✝ : g ∈ s.pi t
eq : Pi.cons s a b₁ f = Pi.cons s a b₂ g
⊢ Pi.cons s a b₁ f a ⋯ = Pi.cons s a b₂ g a ⋯

Tactic:
by rw [eq]

Goal state after:
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ kernImage f (f ⁻¹' t ∪ s) = t ∪ kernImage f s

Tactic:
union_comm,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ kernImage f (s ∪ f ⁻¹' t) = t ∪ kernImage f s
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
hf : Bijective f
s : ι → Set α
⊢ f '' ⋂ i, s i = ⋂ i, f '' s i

Tactic:
by
  cases isEmpty_or_nonempty ι
  · simp_rw [iInter_of_empty, image_univ_of_surjective hf.surjective]
  · exact hf.injective.injOn.image_iInter_eq

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
a : α
⊢ a⁻¹ ∈ s⁻¹ ↔ a ∈ s

Tactic:
by simp only [mem_inv, inv_inv]

Goal state after:
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
C : Set (Set β)
⊢ s ×ˢ ⋃ i ∈ C, i = ⋃ i ∈ (fun t ↦ s ×ˢ t) '' C, i

Tactic:
biUnion_image,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
C : Set (Set β)
⊢ s ×ˢ ⋃ i ∈ C, i = ⋃ y ∈ C, s ×ˢ y
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : (i : ι) → κ i → Set α
t : Set β
⊢ image2 f (⋃ i, ⋃ j, s i j) t = ⋃ i, ⋃ j, image2 f (s i j) t

Tactic:
simp_rw [image2_iUnion_left]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
S : Type u_4
H : S
inst✝³ : SetLike S G
inst✝² : SubgroupClass S G
inst✝¹ : Preorder S
inst✝ : IsConcreteLE S G
x : ↥H
⊢ (inclusion ⋯) x = x

Tactic:
cases x

Goal state after:
case mk
G : Type u_1
inst✝⁴ : Group G
S : Type u_4
H : S
inst✝³ : SetLike S G
inst✝² : SubgroupClass S G
inst✝¹ : Preorder S
inst✝ : IsConcreteLE S G
val✝ : G
property✝ : val✝ ∈ H
⊢ (inclusion ⋯) ⟨val✝, property✝⟩ = ⟨val✝, property✝⟩
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
S : Type u_4
H K : S
inst✝³ : SetLike S G
inst✝² : SubgroupClass S G
inst✝¹ : LE S
inst✝ : IsConcreteLE S G
h : H ≤ K
x : ↥K
hx : ↑x ∈ H
⊢ (inclusion h) ⟨↑x, hx⟩ = x

Tactic:
cases x

Goal state after:
case mk
G : Type u_1
inst✝⁴ : Group G
S : Type u_4
H K : S
inst✝³ : SetLike S G
inst✝² : SubgroupClass S G
inst✝¹ : LE S
inst✝ : IsConcreteLE S G
h : H ≤ K
val✝ : G
property✝ : val✝ ∈ K
hx : ↑⟨val✝, property✝⟩ ∈ H
⊢ (inclusion h) ⟨↑⟨val✝, property✝⟩, hx⟩ = ⟨val✝, property✝⟩
Module: Mathlib.Algebra.Group.Subgroup.Defs

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
S : Type u_4
H K : S
inst✝³ : SetLike S G
inst✝² : SubgroupClass S G
inst✝¹ : Preorder S
inst✝ : IsConcreteLE S G
L : S
hHK : H ≤ K
hKL : K ≤ L
x : ↥H
⊢ (inclusion hKL) ((inclusion hHK) x) = (inclusion ⋯) x

Tactic:
cases x

Goal state after:
case mk
G : Type u_1
inst✝⁴ : Group G
S : Type u_4
H K : S
inst✝³ : SetLike S G
inst✝² : SubgroupClass S G
inst✝¹ : Preorder S
inst✝ : IsConcreteLE S G
L : S
hHK : H ≤ K
hKL : K ≤ L
val✝ : G
property✝ : val✝ ∈ H
⊢ (inclusion hKL) ((inclusion hHK) ⟨val✝, property✝⟩) = (inclusion ⋯) ⟨val✝, property✝⟩
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
x : Subgroup G
⊢ (fun S ↦
        let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
        { toSubmonoid := __src, inv_mem' := ⋯ })
      ((fun S ↦
          let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
          { toAddSubmonoid := __src, neg_mem' := ⋯ })
        x) =
    x

Tactic:
cases x

Goal state after:
case mk
G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
toSubmonoid✝ : Submonoid G
inv_mem'✝ : ∀ {x : G}, x ∈ toSubmonoid✝.carrier → x⁻¹ ∈ toSubmonoid✝.carrier
⊢ (fun S ↦
        let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
        { toSubmonoid := __src, inv_mem' := ⋯ })
      ((fun S ↦
          let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
          { toAddSubmonoid := __src, neg_mem' := ⋯ })
        { toSubmonoid := toSubmonoid✝, inv_mem' := inv_mem'✝ }) =
    { toSubmonoid := toSubmonoid✝, inv_mem' := inv_mem'✝ }
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
x : AddSubgroup (Additive G)
⊢ (fun S ↦
        let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
        { toAddSubmonoid := __src, neg_mem' := ⋯ })
      ((fun S ↦
          let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
          { toSubmonoid := __src, inv_mem' := ⋯ })
        x) =
    x

Tactic:
cases x

Goal state after:
case mk
G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
toAddSubmonoid✝ : AddSubmonoid (Additive G)
neg_mem'✝ : ∀ {x : Additive G}, x ∈ toAddSubmonoid✝.carrier → -x ∈ toAddSubmonoid✝.carrier
⊢ (fun S ↦
        let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
        { toAddSubmonoid := __src, neg_mem' := ⋯ })
      ((fun S ↦
          let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
          { toSubmonoid := __src, inv_mem' := ⋯ })
        { toAddSubmonoid := toAddSubmonoid✝, neg_mem' := neg_mem'✝ }) =
    { toAddSubmonoid := toAddSubmonoid✝, neg_mem' := neg_mem'✝ }
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
x : AddSubgroup A
⊢ (fun S ↦
        let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
        { toAddSubmonoid := __src, neg_mem' := ⋯ })
      ((fun S ↦
          let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
          { toSubmonoid := __src, inv_mem' := ⋯ })
        x) =
    x

Tactic:
cases x

Goal state after:
case mk
G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
toAddSubmonoid✝ : AddSubmonoid A
neg_mem'✝ : ∀ {x : A}, x ∈ toAddSubmonoid✝.carrier → -x ∈ toAddSubmonoid✝.carrier
⊢ (fun S ↦
        let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
        { toAddSubmonoid := __src, neg_mem' := ⋯ })
      ((fun S ↦
          let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
          { toSubmonoid := __src, inv_mem' := ⋯ })
        { toAddSubmonoid := toAddSubmonoid✝, neg_mem' := neg_mem'✝ }) =
    { toAddSubmonoid := toAddSubmonoid✝, neg_mem' := neg_mem'✝ }
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
x : Subgroup (Multiplicative A)
⊢ (fun S ↦
        let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
        { toSubmonoid := __src, inv_mem' := ⋯ })
      ((fun S ↦
          let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
          { toAddSubmonoid := __src, neg_mem' := ⋯ })
        x) =
    x

Tactic:
cases x

Goal state after:
case mk
G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
toSubmonoid✝ : Submonoid (Multiplicative A)
inv_mem'✝ : ∀ {x : Multiplicative A}, x ∈ toSubmonoid✝.carrier → x⁻¹ ∈ toSubmonoid✝.carrier
⊢ (fun S ↦
        let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
        { toSubmonoid := __src, inv_mem' := ⋯ })
      ((fun S ↦
          let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
          { toAddSubmonoid := __src, neg_mem' := ⋯ })
        { toSubmonoid := toSubmonoid✝, inv_mem' := inv_mem'✝ }) =
    { toSubmonoid := toSubmonoid✝, inv_mem' := inv_mem'✝ }
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Subsingleton ↥H
⊢ H = ⊥

Tactic:
Subgroup.eq_bot_iff_forall

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Subsingleton ↥H
⊢ ∀ x ∈ H, x = 1
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ Nontrivial ↥H ↔ H ≠ ⊥

Tactic:
rw [nontrivial_iff_exists_ne_one, ne_eq, eq_bot_iff_forall]
  simp only [ne_eq, not_forall, exists_prop]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: case mp
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
⊢ x / y ∈ f.ker → f x = f y

Tactic:
intro h

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : x / y ∈ f.ker
⊢ f x = f y
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
⊢ f x = f y → x / y ∈ f.ker

Tactic:
intro h

Goal state after:
case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : f x = f y
⊢ x / y ∈ f.ker
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: case mp
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
⊢ f x = f y → y⁻¹ * x ∈ f.ker

Tactic:
intro h

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : f x = f y
⊢ y⁻¹ * x ∈ f.ker
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
⊢ y⁻¹ * x ∈ f.ker → f x = f y

Tactic:
intro h

Goal state after:
case mpr
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
h : y⁻¹ * x ∈ f.ker
⊢ f x = f y
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
⊢ f.range = ⊥ ↔ f = 1

Tactic:
rw [← le_bot_iff, f.range_eq_map, map_le_iff_le_comap, top_le_iff, comap_bot, ker_eq_top_iff]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
⊢ comap f (map f H) = H ⊔ f.ker

Tactic:
refine le_antisymm ?_ (sup_le (le_comap_map _ _) (ker_le_comap _ _))

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
⊢ comap f (map f H) ≤ H ⊔ f.ker
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : (fun g ↦ ↑g.1 * ↑g.2) x = (fun g ↦ ↑g.1 * ↑g.2) y
⊢ x = y

Tactic:
← inv_mul_eq_iff_eq_mul,

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : (↑y.1)⁻¹ * (fun g ↦ ↑g.1 * ↑g.2) x = ↑y.2
⊢ x = y
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
S x : Submonoid M
⊢ (fun S ↦ { carrier := ⇑Additive.ofMul ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Additive.toMul ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ }) x) =
    x

Tactic:
cases x

Goal state after:
case mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
S : Submonoid M
toSubsemigroup✝ : Subsemigroup M
one_mem'✝ : 1 ∈ toSubsemigroup✝.carrier
⊢ (fun S ↦ { carrier := ⇑Additive.ofMul ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Additive.toMul ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ })
        { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }) =
    { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
S : Submonoid M
x : AddSubmonoid (Additive M)
⊢ (fun S ↦ { carrier := ⇑Additive.toMul ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Additive.ofMul ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ }) x) =
    x

Tactic:
cases x

Goal state after:
case mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
S : Submonoid M
toAddSubsemigroup✝ : AddSubsemigroup (Additive M)
zero_mem'✝ : 0 ∈ toAddSubsemigroup✝.carrier
⊢ (fun S ↦ { carrier := ⇑Additive.toMul ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Additive.ofMul ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ })
        { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ }) =
    { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ }
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : AddZeroClass A
x : AddSubmonoid A
⊢ (fun S ↦ { carrier := ⇑Multiplicative.ofAdd ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Multiplicative.toAdd ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ }) x) =
    x

Tactic:
cases x

Goal state after:
case mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : AddZeroClass A
toAddSubsemigroup✝ : AddSubsemigroup A
zero_mem'✝ : 0 ∈ toAddSubsemigroup✝.carrier
⊢ (fun S ↦ { carrier := ⇑Multiplicative.ofAdd ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Multiplicative.toAdd ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ })
        { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ }) =
    { toAddSubsemigroup := toAddSubsemigroup✝, zero_mem' := zero_mem'✝ }
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : AddZeroClass A
x : Submonoid (Multiplicative A)
⊢ (fun S ↦ { carrier := ⇑Multiplicative.toAdd ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Multiplicative.ofAdd ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ }) x) =
    x

Tactic:
cases x

Goal state after:
case mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : AddZeroClass A
toSubsemigroup✝ : Subsemigroup (Multiplicative A)
one_mem'✝ : 1 ∈ toSubsemigroup✝.carrier
⊢ (fun S ↦ { carrier := ⇑Multiplicative.toAdd ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Multiplicative.ofAdd ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ })
        { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }) =
    { toSubsemigroup := toSubsemigroup✝, one_mem' := one_mem'✝ }
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: case mp
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ u ≤ s.prod t → map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t

Tactic:
intro h

Goal state after:
case mp
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : u ≤ s.prod t
⊢ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: case mp
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
⊢ s.prod t ≤ u → map (inl M N) s ≤ u ∧ map (inr M N) t ≤ u

Tactic:
intro h

Goal state after:
case mp
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : s.prod t ≤ u
⊢ map (inl M N) s ≤ u ∧ map (inr M N) t ≤ u
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: a b : ℕ
⊢ a ≤ pair a b

Tactic:
simpa using unpair_left_le (pair a b)

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: n : ℕ
h : 2 ≤ n
⊢ 0 < 2

Tactic:
by decide

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : N →* G
x : N
⊢ (∀ (h : G), h ∈ H ↔ f x * h * (f x)⁻¹ ∈ H) → ∀ (h : N), f h ∈ H ↔ f (x * h * x⁻¹) ∈ H

Tactic:
intro h

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : N →* G
x : N
h : ∀ (h : G), h ∈ H ↔ f x * h * (f x)⁻¹ ∈ H
⊢ ∀ (h : N), f h ∈ H ↔ f (x * h * x⁻¹) ∈ H
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
⊢ Pairwise (Disjoint on fun a ↦ a • s) ↔ ∀ (a : α), (a • s ∩ s).Nonempty → a = 1

Tactic:
Pairwise,

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
⊢ (∀ ⦃i j : α⦄, i ≠ j → (Disjoint on fun a ↦ a • s) i j) ↔ ∀ (a : α), (a • s ∩ s).Nonempty → a = 1
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: α : Type u_1
a : α
⊢ of a ≠ 1

Tactic:
intro h

Goal state after:
α : Type u_1
a : α
h : of a = 1
⊢ False
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
b : FreeMonoid α
hb : (map f) b = of d
⊢ ∃ a, f a = d

Tactic:
induction b using FreeMonoid.inductionOn' with

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons.inr
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
x y : M
ys : List M
ih : x ∈ ys → x ≤ ys.prod
h₁ : x ∈ ys
⊢ x ≤ (y :: ys).prod

Tactic:
specialize ih h₁
      simp only [List.prod_cons]
      exact le_mul_left ih

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x✝ : M
hx : x✝ ∈ closure (⋃ i, ↑(S i))
x y : M
hx✝ : x ∈ closure (⋃ i, ↑(S i))
hy✝ : y ∈ closure (⋃ i, ↑(S i))
i : ι
hi : x ∈ S i
j : ι
hj : y ∈ S j
k : ι
hik : S i ≤ S k
hjk : S j ≤ S k
⊢ ∃ i, x * y ∈ S i

Tactic:
exact ⟨k, mul_mem (hik hi) (hjk hj)⟩

Goal state after:
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case left.left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : Std.Asymm r
inst✝ : ∀ (i : ι), Std.Antisymm (s i)
i✝ j✝ : ι
a : α i✝
b : α j✝
hij : r i✝ j✝
hji : r j✝ i✝
⊢ ⟨i✝, a⟩ = ⟨j✝, b⟩

Tactic:
exact (asymm hij hji).elim

Goal state after:
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
inst✝¹ : Std.Asymm r
inst✝ : ∀ (i : ι), Std.Antisymm (s i)
⊢ ∀ (a b : (i : ι) × α i), Lex r s a b → Lex r s b a → a = b

Tactic:
by
    rintro _ _ (⟨a, b, hij⟩ | ⟨a, b, hab⟩) (⟨_, _, hji⟩ | ⟨_, _, hba⟩)
    · exact (asymm hij hji).elim
    · exact (irrefl _ hij).elim
    · exact (irrefl _ hji).elim
    · exact congr_arg (Sigma.mk _ ·) <| antisymm hab hba

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Union

Goal state before:
pp: α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
s : Finset α
t : α → Finset β
⊢ s.sup t = s.biUnion t

Tactic:
ext
  rw [mem_sup, mem_biUnion]

Goal state after: