mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Invertible.Basic

Goal state before:
pp: α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible (a * b)
⊢ b * (⅟(a * b) * a) = 1

Tactic:
by
    rw [← (isUnit_of_invertible a).mul_right_inj, ← mul_assoc, ← mul_assoc, mul_invOf_self, mul_one,
      one_mul]

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: ι : Type u_5
α : ι → Type u_6
r : (i : ι) → α i → α i → Prop
d : (i : ι) → Set (α i)
hd : ∀ (i : ι), DirectedOn (r i) (d i)
⊢ DirectedOn (fun x y ↦ ∀ (i : ι), r i (x i) (y i)) (Set.univ.pi d)

Tactic:
intro a ha b hb
  choose f hfd haf hbf using fun i => hd i (a i) (ha i trivial) (b i) (hb i trivial)
  exact ⟨f, fun i _ => hfd i, haf, hbf⟩

Goal state after:
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
a b c d : K
hbc : Commute b c
hbd : Commute b d
hb : b ≠ 0
hd : d ≠ 0
⊢ a / b + c / d = a * d / (b * d) + b * c / (b * d)

Tactic:
mul_div_mul_right _ b hd,

Goal state after:
K : Type u_1
inst✝ : DivisionSemiring K
a b c d : K
hbc : Commute b c
hbd : Commute b d
hb : b ≠ 0
hd : d ≠ 0
⊢ a / b + c / d = a / b + b * c / (b * d)
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
⊢ StrictAntiOn f (insert a s) ↔ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s

Tactic:
rw [strictAntiOn_insert_iff]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
⊢ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
Module: Mathlib.Data.Set.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
⊢ StrictAntiOn f (insert a s) ↔ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s

Tactic:
rw [strictAntiOn_insert_iff]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
⊢ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: case h
α : Type u
β : Type v
inst✝ : Preorder β
f g : α → β
h : ∀ (a : α), f a ≤ g a
C : β
hC : C ∈ upperBounds (range g)
x : α
⊢ f x ≤ C

Tactic:
exact (h x).trans (hC <| mem_range_self x)

Goal state after:
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: case inr
α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.8
s t : Set α
p : α → Prop
inst✝ : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
x : α
h : x ∈ t
⊢ (fun x ↦ if hp : p ↑x then Sum.inl ⟨↑x, ⋯⟩ else Sum.inr ⟨↑x, ⋯⟩)
      ((fun o ↦
          match o with
          | Sum.inl x => ⟨↑x, ⋯⟩
          | Sum.inr x => ⟨↑x, ⋯⟩)
        (Sum.inr ⟨x, h⟩)) =
    Sum.inr ⟨x, h⟩

Tactic:
simp [ht _ h]

Goal state after:
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Preorder α
s t : Set α
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s ∧ IsCofinalFor t s ∨ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t ∧ IsCofinalFor s t →
    DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t)

Tactic:
rintro (⟨hs, hts⟩ | ⟨ht, hst⟩) x hx y hy

Goal state after:
case refine_2.inl
α : Type u_1
inst✝ : Preorder α
s t : Set α
hs : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
hts : IsCofinalFor t s
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
⊢ ∃ z ∈ s ∪ t, (fun x1 x2 ↦ x1 ≤ x2) x z ∧ (fun x1 x2 ↦ x1 ≤ x2) y z

case refine_2.inr
α : Type u_1
inst✝ : Preorder α
s t : Set α
ht : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
hst : IsCofinalFor s t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
⊢ ∃ z ∈ s ∪ t, (fun x1 x2 ↦ x1 ≤ x2) x z ∧ (fun x1 x2 ↦ x1 ≤ x2) y z
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
a ta t : α
pra : a = ta
prt : -ta = t
⊢ -a = t

Tactic:
by
  simp [pra, prt]

Goal state after:
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
m : ℕ
⊢ IsNat (↑↑m) m

Tactic:
exact ⟨rfl⟩

Goal state after:
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
m : ℤ
⊢ IsInt (↑↑m) m

Tactic:
exact ⟨rfl⟩

Goal state after:
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
hb : b < 0
⊢ 1 ≤ a / b ↔ a ≤ b

Tactic:
by rw [le_div_iff_of_neg hb, one_mul]

Goal state after:
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_4
inst✝³ : CommRing α
inst✝² : NoZeroDivisors α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
a b : α
a0 : 0 ≤ a
b0 : 0 ≤ b
⊢ a * a = b * b ↔ a = b

Tactic:
have := fun h ↦ le_antisymm (neg_nonneg.mp h) b0
  grind [sq_sub_sq, mul_eq_zero, add_eq_zero_iff_eq_neg]

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
⊢ (∃ l, Forall₂ R l₁ l ∧ l <+ map f l₂) → ∃ l, Forall₂ (fun a c ↦ R a (f c)) l₁ l ∧ l <+ l₂

Tactic:
rintro ⟨l1, h1, h2⟩
    obtain ⟨l', hl1, rfl⟩ := sublist_map_iff.mp h2
    use l'
    simpa [hl1] using h1

Goal state after:
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
f : α → β
g : α → List β
⊢ map f l ++ flatMap g l ~ flatMap (fun x ↦ f x :: g x) l

Tactic:
simpa [← map_eq_flatMap] using flatMap_append_perm l (fun x => [f x]) g

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
f : ℕ → M
n : ℕ
⊢ (map f (range n.succ)).prod = f 0 * (map (fun i ↦ f i.succ) (range n)).prod

Tactic:
by
  rw [range_succ_eq_map]
  simp [Function.comp_def]

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

Goal state before:
pp: case nil
M : Type u_4
inst✝¹ : Monoid M
l : List M
a : M
inst✝ : DecidableEq M
ha : a ∈ []
comm : ∀ (x : M), x ∈ [] → ∀ (y : M), y ∈ [] → x * y = y * x
⊢ a * ([].erase a).prod = [].prod

Tactic:
simp only [not_mem_nil] at ha

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : GroupWithZero M
r : ℤ
x : M
hx : x ≠ 0
l : NF M
hl : l.eval ≠ 0
⊢ ((r, x) ::ᵣ l).eval ≠ 0

Tactic:
by
  unfold eval cons
  apply mul_ne_zero ?_ hl
  simp [zpow'_eq_zero_iff, hx]

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a : M
i : ℕ
ih : ∀ {l : List M}, i ≤ l.length → (∀ (a' : M), a' ∈ take i l → Commute a a') → (l.insertIdx i a).prod = a * l.prod
l : List M
hlen : i + 1 ≤ l.length
hcomm : ∀ (a' : M), a' ∈ take (i + 1) l → Commute a a'
⊢ (l.insertIdx (i + 1) a).prod = a * l.prod

Tactic:
obtain ⟨hd, tl, rfl⟩ := exists_cons_of_length_pos (Nat.zero_lt_of_lt hlen)

Goal state after:
M : Type u_4
inst✝ : Monoid M
a : M
i : ℕ
ih : ∀ {l : List M}, i ≤ l.length → (∀ (a' : M), a' ∈ take i l → Commute a a') → (l.insertIdx i a).prod = a * l.prod
hd : M
tl : List M
hlen : i + 1 ≤ (hd :: tl).length
hcomm : ∀ (a' : M), a' ∈ take (i + 1) (hd :: tl) → Commute a a'
⊢ ((hd :: tl).insertIdx (i + 1) a).prod = a * (hd :: tl).prod
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
p : α → Bool
⊢ map (fun a ↦ ↑a) (filter (fun x ↦ p ↑x) l.attach) = map (fun x ↦ id ↑x) (filter p l).attach

Tactic:
id,

Goal state after:
α : Type u
l : List α
p : α → Bool
⊢ map (fun a ↦ ↑a) (filter (fun x ↦ p ↑x) l.attach) = map (fun x ↦ ↑x) (filter p l).attach
Module: Mathlib.Algebra.Ring.Rat

Goal state before:
pp: num den n : ℕ
⊢ mkRat (↑num) den ^ n = mkRat (↑num ^ n) (den ^ n)

Tactic:
by
  rw [mkRat_eq_divInt, mkRat_eq_divInt, divInt_pow, Int.natCast_pow]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: q : ℚ
⊢ |q| = ↑q.num.natAbs /. ↑q.den

Tactic:
grind [abs_of_nonpos, neg_def, Rat.num_nonneg, abs_of_nonneg, num_divInt_den]

Goal state after:
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: q : ℚ≥0
⊢ q.num ≠ 0 ↔ q ≠ 0

Tactic:
by simp [num]

Goal state after:
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y z : α
h : IsRelPrime y z
dvd : x ∣ y
⊢ IsRelPrime x z

Tactic:
obtain ⟨d, rfl⟩ := dvd

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
x z d : α
h : IsRelPrime (x * d) z
⊢ IsRelPrime x z
Module: Mathlib.Algebra.Group.Commute.Basic

Goal state before:
pp: G : Type u_1
inst✝ : DivisionMonoid G
a b c d : G
hbc : Commute b c
hbd : Commute b⁻¹ d
hcd : Commute c⁻¹ d
⊢ a / b / (c / d) = a / c / (b / d)

Tactic:
by
  simp_rw [div_eq_mul_inv, mul_inv_rev, inv_inv, hbd.symm.eq, hcd.symm.eq,
    hbc.inv_inv.mul_mul_mul_comm]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
a : α
inst✝ : Subsingleton αˣ
c d : α
hcd : a = a * c * d
⊢ a = a * c

Tactic:
rw [mul_assoc, eq_comm, mul_right_eq_self₀, mul_eq_one] at hcd

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
a : α
inst✝ : Subsingleton αˣ
c d : α
hcd : c = 1 ∧ d = 1 ∨ a = 0
⊢ a = a * c
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
m n : α
⊢ m ∣ n ↔ m = 0 → n = 0

Tactic:
refine ⟨fun ⟨a, ha⟩ hm => ?_, fun h => ?_⟩

Goal state after:
case refine_1
α : Type u_1
inst✝ : GroupWithZero α
m n : α
x✝ : m ∣ n
hm : m = 0
a : α
ha : n = m * a
⊢ n = 0

case refine_2
α : Type u_1
inst✝ : GroupWithZero α
m n : α
h : m = 0 → n = 0
⊢ m ∣ n
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ
⊢ {
        num :=
          (q₁.num * ↑q₂.den + q₂.num * ↑q₁.den) / ↑((q₁.num * ↑q₂.den + q₂.num * ↑q₁.den).natAbs.gcd (q₁.den * q₂.den)),
        den := q₁.den * q₂.den / (q₁.num * ↑q₂.den + q₂.num * ↑q₁.den).natAbs.gcd (q₁.den * q₂.den), den_nz := ⋯,
        reduced := ⋯ }.den ∣
    q₁.den.lcm q₂.den

Tactic:
Nat.div_dvd_iff_dvd_mul (Nat.gcd_dvd_right _ _)
    (Nat.gcd_pos_of_pos_right _ (by simp [Nat.pos_iff_ne_zero])),

Goal state after:
q₁ q₂ : ℚ
⊢ q₁.den * q₂.den ∣ (q₁.num * ↑q₂.den + q₂.num * ↑q₁.den).natAbs.gcd (q₁.den * q₂.den) * q₁.den.lcm q₂.den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case neg
n : ℤ
hn : ¬n = 0
⊢ ↑(n / n) = ↑n / ↑n

Tactic:
have : (n : ℚ) ≠ 0 := by rwa [← intCast_inj]  at hn

Goal state after:
case neg
n : ℤ
hn : ¬n = 0
this : ↑n ≠ 0
⊢ ↑(n / n) = ↑n / ↑n
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: a : ℕ
inst✝ : a.AtLeastTwo
⊢ (OfNat.ofNat a)⁻¹.den = OfNat.ofNat a

Tactic:
simp [den_inv, Int.natAbs_eq_iff]

Goal state after:
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : Field α
n1 n2 k e1 e2 t1 : α
h1 : n1 * e1 = t1
h2 : n2 / e2 = 1
h3 : n1 * n2 = k
⊢ k * (e1 / e2) = t1

Tactic:
rw [← h3, mul_assoc, mul_div_left_comm, h2, ← mul_assoc, h1, mul_comm, one_mul]

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₁ : β
⊢ ∀ ⦃j : β⦄, b₁ ≠ j → (Disjoint on extend e f ⊥) b₁ j

Tactic:
b₂

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₁ b₂ : β
⊢ b₁ ≠ b₂ → (Disjoint on extend e f ⊥) b₁ b₂
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsStrongAntichain r s
f : α → β
hf : Surjective f
h : ∀ (a b : α), r' (f a) (f b) → r a b
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : f a ≠ f b
c : α
⊢ ¬r' (f a) (f c) ∨ ¬r' (f b) (f c)

Tactic:
exact (hs ha hb (ne_of_apply_ne _ hab) _).imp (mt <| h _ _) (mt <| h _ _)

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: case neg
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
hS : ¬S = ∅
⊢ IsLUB S ⟨sSup (Subtype.val '' S), ⋯⟩

Tactic:
exact .of_image Subtype.coe_le_coe <| isLUB_csSup ((Set.nonempty_iff_ne_empty.mpr hS).image _)
        ((Subtype.mono_coe _).map_bddAbove (OrderTop.bddAbove S))

Goal state after:
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑n)⁻¹ = (↑n)⁻¹

Tactic:
by
  rcases n with - | n
  · simp
  rw [cast_def, inv_natCast_num, inv_natCast_den, if_neg n.succ_ne_zero,
    Int.sign_eq_one_of_pos (Int.ofNat_succ_pos n), Int.cast_one, one_div]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
⊢ 0 < ⌊a⌋ ↔ 1 ≤ a

Tactic:
Int.lt_iff_add_one_le,

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
⊢ 0 + 1 ≤ ⌊a⌋ ↔ 1 ≤ a
Module: Mathlib.Algebra.Order.Group.Basic

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x ↦ a ^ x
hlt : 1 < a
⊢ False

Tactic:
rcases exists_between hlt with ⟨b, hb, hba⟩

Goal state after:
case inr.inr
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x ↦ a ^ x
hlt : 1 < a
b : α
hb : 1 < b
hba : b < a
⊢ False
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
b : H
inst✝² : AddMonoidWithOne G
inst✝¹ : AddMonoid H
inst✝ : AddConstMapClass F G H 1 b
f : F
n : ℕ
⊢ f ↑n = f 0 + n • b

Tactic:
by
  simpa using map_add_nat' f 0 n

Goal state after:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddGroup G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H a b
f : F
x : G
⊢ f (x - a) = f x - b

Tactic:
simpa using map_sub_nsmul f x 1

Goal state after:
Module: Mathlib.Algebra.Torsor.Defs

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
g₁ g₂ : G
p : P
h : g₁ • p = g₂ • p
⊢ g₁ = g₂

Tactic:
rw [← smul_sdiv g₁ p, h, smul_sdiv]

Goal state after:
Module: Mathlib.Algebra.Torsor.Defs

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ : P
g : G
⊢ p₂ /ₛ g • p₂ = (p₂ /ₛ p₁) * ((p₁ /ₛ p₂) / g)

Tactic:
← inv_sdiv_eq_sdiv_rev,

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ : P
g : G
⊢ (g • p₂ /ₛ p₂)⁻¹ = (p₂ /ₛ p₁) * ((p₁ /ₛ p₂) / g)
Module: Mathlib.Algebra.Torsor.Defs

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ : P
g : G
⊢ g⁻¹ = (p₂ /ₛ p₁) * (p₁ /ₛ p₂) / g

Tactic:
← inv_sdiv_eq_sdiv_rev,

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ : P
g : G
⊢ g⁻¹ = (p₁ /ₛ p₂)⁻¹ * (p₁ /ₛ p₂) / g
Module: Mathlib.Algebra.Torsor.Defs

Goal state before:
pp: G : Type u_3
P : Type u_4
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
x y : P
⊢ (pointReflection x) y -ᵥ y = 2 • (x -ᵥ y)

Tactic:
by
  simp [pointReflection, two_nsmul, vadd_vsub_assoc]

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

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝¹ : Monoid α
inst✝ : MulAction α β
m : αˣ
⊢ Function.Bijective fun a ↦ ↑m • a

Tactic:
exact MulAction.bijective m

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x : K
n : ℤ
h : ↑n < x
⊢ ↑↑n < x

Tactic:
rwa [Rat.cast_intCast]

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
⊢ ∃ q, 0 < q ∧ x < q ^ n ∧ q ^ n < y

Tactic:
let m := Nat.find ex

Goal state after:
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
⊢ ∃ q, 0 < q ∧ x < q ^ n ∧ q ^ n < y
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : a ∈ s
⊢ (s.erase a).card = if a ∈ s then s.card.pred else s.card

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : ¬a ∈ s
⊢ (s.erase a).card = if a ∈ s then s.card.pred else s.card

Tactic:
· rwa [card_erase_of_mem h, if_pos]

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : ¬a ∈ s
⊢ (s.erase a).card = if a ∈ s then s.card.pred else s.card
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case refine_2.refine_1
α : Type u_1
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → m1.card = t.card → Rel r m1 t
b : α
m' : Multiset α
h : ∀ (a_1 b_1 : α), a_1 ∈ b ::ₘ m' → b_1 ∈ a ::ₘ t → r a_1 b_1
hc : (b ::ₘ m').card = t.card + 1
hb : b ∈ b ::ₘ m'
⊢ ∀ (a b : α), a ∈ m' → b ∈ t → r a b

Tactic:
exact fun _ _ ha hb => h _ _ (mem_cons_of_mem ha) (mem_cons_of_mem hb)

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ a ha, i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
this : t = map (fun x ↦ i ↑x ⋯) s.attach
⊢ map (fun x ↦ f ↑x) s.attach = map g t

Tactic:
rw [this, Multiset.map_map]; exact map_congr rfl fun x _ => h _ _

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ t + s ∩ t ≤ s + t

Tactic:
rw [Multiset.add_comm]

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ∩ t + t ≤ s + t
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ t + s ≤ s ∪ t + t

Tactic:
rw [Multiset.add_comm]

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s + t ≤ s ∪ t + t
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
⊢ count a (filter p s) = if p a then count a s else 0

Tactic:
split_ifs with h
  · exact count_filter_of_pos h
  · exact count_filter_of_neg h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
x✝ : List α
d : Nodup (Quot.mk (⇑(isSetoid α)) x✝)
⊢ x✝.erase a = List.filter (fun b ↦ decide ((fun x ↦ x ≠ a) b)) x✝

Tactic:
simpa using! List.Nodup.erase_eq_filter d a

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

Goal state before:
pp: α : Type u_1
x : α
xs : List α
⊢ [x] <:+: xs ↔ x ∈ xs

Tactic:
List.mem_iff_append,

Goal state after:
α : Type u_1
x : α
xs : List α
⊢ [x] <:+: xs ↔ ∃ s t, xs = s ++ x :: t
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
⊢ ∅ = map f s ↔ s = ∅

Tactic:
rw [eq_comm, map_eq_empty]

Goal state after:
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.succ ≤ p.rev
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev

Tactic:
succAbove_of_succ_le _ _ h,

Goal state after:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.succ ≤ p.rev
⊢ i.castSucc = (p.succAbove i.rev).rev
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : a.succAbove b ≠ 0
⊢ (a.pred ha).succAbove (b.pred hb) = (a.succAbove b).pred hk

Tactic:
simp_rw [← succ_inj (b := pred (succAbove a b) hk), ← succ_succAbove_succ, succ_pred]

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
p i : Fin n
h : p ≤ i
⊢ p.predAbove i.succ = i

Tactic:
predAbove_succ_of_le _ _ h

Goal state after:
case inl
n : ℕ
p i : Fin n
h : p ≤ i
⊢ i = i
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝⁴ : Finite α
p q : α → Prop
inst✝³ : Fintype { x // p x }
inst✝² : Fintype { x // ¬p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // ¬q x }
h : card { x // p x } = card { x // q x }
⊢ card { x // ¬p x } = card { x // ¬q x }

Tactic:
by
  cases nonempty_fintype α
  simp only [Fintype.card_subtype_compl, h]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case succ
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
j : Fin (n + 1)
⊢ cons a (snoc q b) j.succ = snoc (cons a q) b j.succ

Tactic:
cases j using Fin.lastCases with

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Set α
inst✝ : Fintype ↑s
h : s.Finite
⊢ h.toFinset = s.toFinset

Tactic:
rw [Finite.toFinset, Subsingleton.elim h.fintype]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Sort u_3
i : Fin (n + 1)
a : α
f : Fin n → α
j : Fin (n + 1)
⊢ i.insertNth a f j.rev = i.rev.insertNth a (f ∘ rev) j

Tactic:
induction j using Fin.succAboveCases
  · exact rev i
  · simp
  · simp [rev_succAbove]

Goal state after:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
inst✝¹ : Fintype α
a : α
inst✝ : Fintype ↑{x | x ≠ a}
this : DecidableEq α
⊢ {x | x ≠ a}.card = Fintype.card α - 1

Tactic:
Finset.filter_ne',

Goal state after:
α : Type u
inst✝¹ : Fintype α
a : α
inst✝ : Fintype ↑{x | x ≠ a}
this : DecidableEq α
⊢ (Finset.univ.erase a).card = Fintype.card α - 1
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
inst✝ : DecidableEq α
s₁ s₂ : Finset α
b₁ b₂ : β
⊢ Multiset.fold op (op b₁ b₂) (Multiset.map f ((s₁ ∪ s₂).val + (s₁ ∩ s₂).val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))

Tactic:
union_val,

Goal state after:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
inst✝ : DecidableEq α
s₁ s₂ : Finset α
b₁ b₂ : β
⊢ Multiset.fold op (op b₁ b₂) (Multiset.map f (s₁.val ∪ s₂.val + (s₁ ∩ s₂).val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
r : β → β → Prop
hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z
c : β
⊢ r c (fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)

Tactic:
classical
    induction s using Finset.induction_on with
    | empty => simp
    | insert a s ha IH =>
      rw [Finset.fold_insert ha, hr, IH, ← and_assoc, @and_comm (r c (f a)), and_assoc]
      simp

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
⊢ Decidable (Lex r (a :: l₁) (b :: l₂))

Tactic:
haveI := decidableRel r l₁ l₂
    refine decidable_of_iff (r a b ∨ a = b ∧ Lex r l₁ l₂) ⟨fun h => ?_, fun h => ?_⟩
    · rcases h with (h | ⟨rfl, h⟩)
      · exact Lex.rel h
      · exact Lex.cons h
    · rcases h with (_ | h | h)
      · exact Or.inl h
      · exact Or.inr ⟨rfl, h⟩

Goal state after: