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

Goal state before:
pp: α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
b : β
l : List α
⊢ foldrM f b l = foldr (fun a mb ↦ mb >>= f a) (pure b) l

Tactic:
induction l

Goal state after:
case nil
α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
b : β
⊢ foldrM f b [] = foldr (fun a mb ↦ mb >>= f a) (pure b) []

case cons
α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
b : β
head✝ : α
tail✝ : List α
tail_ih✝ : foldrM f b tail✝ = foldr (fun a mb ↦ mb >>= f a) (pure b) tail✝
⊢ foldrM f b (head✝ :: tail✝) = foldr (fun a mb ↦ mb >>= f a) (pure b) (head✝ :: tail✝)
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
f g : α → Option β
l : List α
h : ∀ (x : α), x ∈ l → f x = g x
⊢ filterMap f l = filterMap g l

Tactic:
induction l

Goal state after:
case nil
α : Type u
β : Type v
f g : α → Option β
h : ∀ (x : α), x ∈ [] → f x = g x
⊢ filterMap f [] = filterMap g []

case cons
α : Type u
β : Type v
f g : α → Option β
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ (x : α), x ∈ tail✝ → f x = g x) → filterMap f tail✝ = filterMap g tail✝
h : ∀ (x : α), x ∈ head✝ :: tail✝ → f x = g x
⊢ filterMap f (head✝ :: tail✝) = filterMap g (head✝ :: tail✝)
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: l : List ℤ
n : ℤ
⊢ l.sum % n = (map (fun x ↦ x % n) l).sum % n

Tactic:
induction l

Goal state after:
case nil
n : ℤ
⊢ [].sum % n = (map (fun x ↦ x % n) []).sum % n

case cons
n head✝ : ℤ
tail✝ : List ℤ
tail_ih✝ : tail✝.sum % n = (map (fun x ↦ x % n) tail✝).sum % n
⊢ (head✝ :: tail✝).sum % n = (map (fun x ↦ x % n) (head✝ :: tail✝)).sum % n
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: l : List ℤ
n : ℤ
⊢ l.prod % n = (map (fun x ↦ x % n) l).prod % n

Tactic:
induction l

Goal state after:
case nil
n : ℤ
⊢ [].prod % n = (map (fun x ↦ x % n) []).prod % n

case cons
n head✝ : ℤ
tail✝ : List ℤ
tail_ih✝ : tail✝.prod % n = (map (fun x ↦ x % n) tail✝).prod % n
⊢ (head✝ :: tail✝).prod % n = (map (fun x ↦ x % n) (head✝ :: tail✝)).prod % n
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
l : List α
⊢ filterMap (fun x ↦ none) l = []

Tactic:
induction l

Goal state after:
case nil
α : Type u
β : Type v
⊢ filterMap (fun x ↦ none) [] = []

case cons
α : Type u
β : Type v
head✝ : α
tail✝ : List α
tail_ih✝ : filterMap (fun x ↦ none) tail✝ = []
⊢ filterMap (fun x ↦ none) (head✝ :: tail✝) = []
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
p : α → Bool
l : List α
⊢ filter p l = foldr (fun a out ↦ bif p a then a :: out else out) [] l

Tactic:
induction l

Goal state after:
case nil
α : Type u
p : α → Bool
⊢ filter p [] = foldr (fun a out ↦ bif p a then a :: out else out) [] []

case cons
α : Type u
p : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : filter p tail✝ = foldr (fun a out ↦ bif p a then a :: out else out) [] tail✝
⊢ filter p (head✝ :: tail✝) = foldr (fun a out ↦ bif p a then a :: out else out) [] (head✝ :: tail✝)
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 a ↦ ↑a) (map (Subtype.map id ⋯) (filter p l).attach)

Tactic:
map_map,

Goal state after:
α : Type u
l : List α
p : α → Bool
⊢ map (fun a ↦ ↑a) (filter (fun x ↦ p ↑x) l.attach) = map ((fun a ↦ ↑a) ∘ Subtype.map id ⋯) (filter p l).attach
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
⊢ filter (fun x ↦ true) l = l

Tactic:
induction l

Goal state after:
case nil
α : Type u
⊢ filter (fun x ↦ true) [] = []

case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : filter (fun x ↦ true) tail✝ = tail✝
⊢ filter (fun x ↦ true) (head✝ :: tail✝) = head✝ :: tail✝
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
⊢ filter (fun x ↦ false) l = []

Tactic:
induction l

Goal state after:
case nil
α : Type u
⊢ filter (fun x ↦ false) [] = []

case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : filter (fun x ↦ false) tail✝ = []
⊢ filter (fun x ↦ false) (head✝ :: tail✝) = []
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q : ℚ
hq : q.den = 1
⊢ ↑q.num = q.num /. ↑1

Tactic:
intCast_eq_divInt

Goal state after:
q : ℚ
hq : q.den = 1
⊢ q.num /. 1 = q.num /. ↑1
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
l : List α
p : β → Prop
f : α → β
⊢ Forall p (map f l) ↔ Forall (p ∘ f) l

Tactic:
induction l

Goal state after:
case nil
α : Type u
β : Type v
l : List α
p : β → Prop
f : α → β
⊢ Forall p (map f []) ↔ Forall (p ∘ f) []

case cons
α : Type u
β : Type v
l : List α
p : β → Prop
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ : Forall p (map f tail✝) ↔ Forall (p ∘ f) tail✝
⊢ Forall p (map f (head✝ :: tail✝)) ↔ Forall (p ∘ f) (head✝ :: tail✝)
Module: Mathlib.Algebra.Ring.Rat

Goal state before:
pp: n : ℕ
⊢ ↑↑n = ↑n /. 1

Tactic:
intCast_eq_divInt

Goal state after:
n : ℕ
⊢ ↑n /. 1 = ↑n /. 1
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b u : α
hu : IsUnit u
⊢ u * a ∣ b ↔ a ∣ b

Tactic:
rcases hu with ⟨u, rfl⟩
  apply Units.mul_left_dvd

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:
by
  obtain ⟨d, rfl⟩ := dvd; exact IsRelPrime.of_mul_left_left h

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

Goal state before:
pp: case inr.refine_2
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * ↑q.den
hqdn : q.num ∣ n
⊢ (n /. d).num ≠ 0

Tactic:
exact Rat.num_ne_zero.2 ((divInt_ne_zero hd).mpr hn)

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

Goal state before:
pp: q₁ q₂ : ℚ
⊢ (q₁ * q₂).den ∣ q₁.den * q₂.den

Tactic:
by
  rw [mul_def, normalize_eq]
  apply Nat.div_dvd_of_dvd
  apply Nat.gcd_dvd_right

Goal state after:
Module: Mathlib.Tactic.FieldSimp

Goal state before:
pp: «$v» : Level
«$M» : Type v
«$iM» : CommGroupWithZero «$M»
«$r» : ℤ
«$x» : «$M»
$snd✝ : ℕ
«$e» : «$M»
«$pf» : zpow' «$x» «$r» = «$e»
⊢ ((«$r», «$x») ::ᵣ []).eval = «$e»

Tactic:
rw [NF.eval_cons]; exact Eq.trans (one_mul _) pf

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

Goal state before:
pp: q r : ℚ
s : ℚ := ⋯
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
a✝ : ¬c = 0
h : q + r = s
⊢ s = ↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)

Tactic:
rw [← divInt_eq_div]

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

Goal state before:
pp: R : Type u_2
n' : ℤ
inst✝ : CommRing R
a : R
⊢ n' • a = ↑n' * a

Tactic:
simp only [zsmul_eq_mul]

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a₂ : R
ea₁ b : ℕ
xa₁ : R
⊢ (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ (ea₁ * b) * Nat.rawCast 1 * a₂ ^ b

Tactic:
simp [_root_.mul_pow, pow_mul, Nat.rawCast]

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
⊢ ⋂₀ S = (⋃₀ (compl '' S))ᶜ

Tactic:
rw [← compl_compl (⋂₀ S), compl_sInter]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
inst✝ : Preorder α
f : ι → α
⊢ ⋂ i, Iic (f i) = lowerBounds (range f)

Tactic:
ext c

Goal state after:
α : Type u_1
ι : Sort u_5
inst✝ : Preorder α
f : ι → α
c : α
⊢ c ∈ ⋂ i, Iic (f i) ↔ c ∈ lowerBounds (range f)
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
S : Set (Set α)
f : α → β
⊢ ⨅ x ∈ ⋃ i, ↑i, f x = ⨅ s ∈ S, ⨅ x ∈ s, f x

Tactic:
iInf_iUnion,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
S : Set (Set α)
f : α → β
⊢ ⨅ i, ⨅ a ∈ ↑i, f a = ⨅ s ∈ S, ⨅ x ∈ s, f x
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
f : (i : ι) → κ i → α
a : α
⊢ (⨆ i, ⨆ j, f i j) ⊓ a = ⨆ i, ⨆ j, f i j ⊓ a

Tactic:
simp only [iSup_inf_eq]

Goal state after:
Module: Mathlib.Order.LatticeIntervals

Goal state before:
pp: α : Type u_1
a b : α
inst✝¹ : Lattice α
inst✝ : Fact (a ≤ b)
x y : ↑(Icc a b)
⊢ Disjoint x y ∧ Codisjoint x y ↔ ↑x ⊓ ↑y = a ∧ ↑x ⊔ ↑y = b

Tactic:
Icc.disjoint_iff,

Goal state after:
α : Type u_1
a b : α
inst✝¹ : Lattice α
inst✝ : Fact (a ≤ b)
x y : ↑(Icc a b)
⊢ ↑x ⊓ ↑y = a ∧ Codisjoint x y ↔ ↑x ⊓ ↑y = a ∧ ↑x ⊔ ↑y = b
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
⊢ sInf (f '' Icc a b) = f a

Tactic:
by
  refine IsGLB.csInf_eq ?_ ((nonempty_Icc.mpr hab).image f)
  refine isGLB_iff_le_iff.mpr (fun b' ↦ ⟨?_, ?_⟩)
  · intro hb'
    rintro _ ⟨x, hx, rfl⟩
    exact hb'.trans <| h' (left_mem_Icc.mpr hab) hx hx.1
  · exact fun hb' ↦ hb' ⟨a, by simp [hab]⟩

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteDistribLattice β
⊢ CompleteDistribLattice α

Tactic:
by
  let completeLattice := e.completeLattice
  let biheytingAlgebra := e.biheytingAlgebra
  apply e.injective.completeDistribLattice <;> intros <;> first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
hf : Monotone f
⊢ IsChain (fun x1 x2 ↦ x1 ≤ x2) (f '' univ)

Tactic:
exact hf.isChain_image (isChain_of_trichotomous _)

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

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

Tactic:
← Set.not_nonempty_iff_eq_empty,

Goal state after:
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
hS : ¬¬S.Nonempty
⊢ sSup (Subtype.val '' S) ∈ Icc a b
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
hS : ¬S = ∅
⊢ sInf (Subtype.val '' S) ∈ Icc a b

Tactic:
← Set.not_nonempty_iff_eq_empty,

Goal state after:
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
hS : ¬¬S.Nonempty
⊢ sInf (Subtype.val '' S) ∈ Icc a b
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
⊢ mulSupport f = ∅ ↔ f = 1

Tactic:
by
  rw [← subset_empty_iff, mulSupport_subset_iff', funext_iff]
  simp

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
⊢ (mulSupport f).Nonempty ↔ f ≠ 1

Tactic:
nonempty_iff_ne_empty,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
⊢ mulSupport f ≠ ∅ ↔ f ≠ 1
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
n : ℕ
⊢ ↑(q ^ n) = ↑q ^ n

Tactic:
by
  rw [cast_def, cast_def, den_pow, num_pow, Nat.cast_pow, Nat.cast_pow, div_eq_mul_inv, ← inv_pow,
    ← (Nat.cast_commute _ _).mul_pow, ← div_eq_mul_inv]

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case neg.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : ¬2 * fract x < 1
H : ⌊2 * fract x⌋ = 1
⊢ ⌈fract x⌉ = (⌊2 * fract x⌋ + 1) / 2

Tactic:
suffices 0 < fract x by simp [this, H, ceil_eq_iff, (fract_lt_one _).le]

Goal state after:
case neg.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : ¬2 * fract x < 1
H : ⌊2 * fract x⌋ = 1
⊢ 0 < fract x
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inl
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m : ℤ
n : ℕ
hn : 0 < ↑n
l₀ : ℕ
hl : 0 ≤ ↑l₀
⊢ fract (↑↑l₀ / ↑n) = ↑(↑l₀ % ↑n) / ↑n

Tactic:
rw [cast_natCast, ← natCast_mod, cast_natCast, fract_div_natCast_eq_div_natCast_mod]

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌊↑(negOfNat n) / ↑d⌋ = negOfNat (-(-↑n / ↑d)).toNat

Tactic:
rw [← ceil_intCast_div_natCast n d, Int.cast_natCast]

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌊↑(negOfNat n) / ↑d⌋ = negOfNat ⌈↑n / ↑d⌉.toNat
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n | a ^ n ≤ g}
k : ℕ
hk : g⁻¹ ≤ a ^ k
h_ne : s.Nonempty
⊢ ∃! k, a ^ k ≤ g ∧ g < a ^ (k + 1)

Tactic:
obtain ⟨k, hk⟩ := MulArchimedean.arch g ha

Goal state after:
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n | a ^ n ≤ g}
k✝ : ℕ
hk✝ : g⁻¹ ≤ a ^ k✝
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
⊢ ∃! k, a ^ k ≤ g ∧ g < a ^ (k + 1)
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Archimedean R
inst✝ : ExistsAddOfLE R
x y : R
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
n : ℕ := Nat.find h
hn : x < y ^ n
hnp : 0 < n
hnsp : n.pred + 1 = n
hltn : n.pred < n
⊢ x < y ^ (n.pred + 1)

Tactic:
rwa [hnsp]

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

Goal state before:
pp: K : Type u_4
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
ε : K
hε : 0 < ε
⊢ ∃ n, 1 / (↑n + 1) < ε

Tactic:
obtain ⟨n, hn⟩ := exists_nat_gt (1 / ε)

Goal state after:
K : Type u_4
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
ε : K
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ ∃ n, 1 / (↑n + 1) < ε
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₂) / g

Tactic:
by
  rw [← mul_right_inj (p₂ /ₛ p₁ : G), sdiv_mul_sdiv_cancel, ← inv_sdiv_eq_sdiv_rev, smul_sdiv, ←
    mul_div_assoc, ← inv_sdiv_eq_sdiv_rev, inv_mul_cancel, one_div]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
a : map f l₁ <+~ map f l₂
⊢ l₁ <+~ l₂

Tactic:
obtain ⟨w, ⟨perm, sublist⟩⟩ := a
    obtain ⟨x, ⟨sublistₓ, mapₓ⟩⟩ := sublist_map_iff.mp sublist
    use x
    constructor
    · rw [mapₓ] at perm
      exact (map_perm_map_iff hf).mp perm
    · exact sublistₓ

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

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

Tactic:
← mul_comm_div

Goal state after:
G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
v₁ v₂ : G
p₁ p₂ : P
⊢ v₁ / v₂ * (p₁ /ₛ p₂) = v₁ / v₂ * (p₁ /ₛ p₂)
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case refine_2
α : Type u_1
m : Multiset α
r : α → α → Prop
⊢ ∀ (a : α) (s : Multiset α),
    ((∀ (x : α), x ∈ s → r x x) → Rel r s s) → (∀ (x : α), x ∈ a ::ₘ s → r x x) → Rel r (a ::ₘ s) (a ::ₘ s)

Tactic:
intro a m ih h

Goal state after:
case refine_2
α : Type u_1
m✝ : Multiset α
r : α → α → Prop
a : α
m : Multiset α
ih : (∀ (x : α), x ∈ m → r x x) → Rel r m m
h : ∀ (x : α), x ∈ a ::ₘ m → r x x
⊢ Rel r (a ::ₘ m) (a ::ₘ m)
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
β : Type v
r : α → β → Prop
hr : Relator.BiUnique r
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
hab : r a✝ b✝
h : Forall₂ r l₁✝ l₂✝
⊢ (fun x1 x2 ↦ x1 ↔ x2) (a✝ :: l₁✝).Nodup (b✝ :: l₂✝).Nodup

Tactic:
simpa only [nodup_cons] using
      Relator.rel_and (Relator.rel_not (rel_mem hr hab h)) (rel_nodup hr h)

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

Goal state before:
pp: α : Type u
l : List α
⊢ (∀ (a : α), ¬[a, a] <+ l) → l.Nodup

Tactic:
induction l

Goal state after:
case nil
α : Type u
⊢ (∀ (a : α), ¬[a, a] <+ []) → [].Nodup

case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ (a : α), ¬[a, a] <+ tail✝) → tail✝.Nodup
⊢ (∀ (a : α), ¬[a, a] <+ head✝ :: tail✝) → (head✝ :: tail✝).Nodup
Module: Mathlib.Data.Set.List

Goal state before:
pp: α : Type u_1
l : List α
x : α
⊢ x ∈ range l.get ↔ ∃ n, l.get n = x

Tactic:
mem_range

Goal state after:
α : Type u_1
l : List α
x : α
⊢ (∃ y, l.get y = x) ↔ ∃ n, l.get n = x
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
h : ¬a ∈ s
⊢ s ≤ a ::ₘ s.erase a

Tactic:
by rw [erase_of_notMem h]; apply le_cons_self

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

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
⊢ ∃ a, s = {a}

Tactic:
rw [← card_eq_one, ← card_map, h, card_singleton]

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
a : α
h1 : a ∈ s
h : map f s = f a ::ₘ t
this : f a ∈ map f s
⊢ ∃ a_1, a_1 ∈ s ∧ f a_1 = f a ∧ map f (s.erase a_1) = t

Tactic:
obtain ⟨u, rfl⟩ := exists_cons_of_mem h1

Goal state after:
case mpr
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
t : Multiset β
a : α
u : Multiset α
h1 : a ∈ a ::ₘ u
h : map f (a ::ₘ u) = f a ::ₘ t
this : f a ∈ map f (a ::ₘ u)
⊢ ∃ a_1, a_1 ∈ a ::ₘ u ∧ f a_1 = f a ∧ map f ((a ::ₘ u).erase a_1) = t
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
h : t₁.Disjoint t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : ¬x ∈ t₁
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂

Tactic:
by_cases h₂ : x ∈ t₂

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
h : t₁.Disjoint t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : ¬x ∈ t₁
h₂ : x ∈ t₂
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂

case neg
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
h : t₁.Disjoint t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : ¬x ∈ t₁
h₂ : ¬x ∈ t₂
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: case mp
α : Type u_1
s : Multiset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
⊢ (filter P s).card ≤ n → ∀ (s' : Multiset α), s' ≤ s → n < s'.card → ∃ a, a ∈ s' ∧ ¬P a

Tactic:
intro H s' hs' s'_card
    by_contra! rid
    have card := card_le_card (monotone_filter_left P hs') |>.trans H
    exact s'_card.not_ge (filter_eq_self.mpr rid ▸ card)

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

Goal state before:
pp: α : Type u_1
β : Type v
p : α → Prop
inst✝ : DecidablePred p
f : α → Option β
s : Multiset α
l : List α
⊢ List.filterMap f (List.filter (fun b ↦ decide (p b)) l) = List.filterMap (fun x ↦ if p x then f x else none) l

Tactic:
by
    simpa using List.filterMap_filter (f := f) (p := p)

Goal state after:
Module: Mathlib.Data.Finset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : List α
hs : s.Nodup
⊢ s.toFinset.toList.Perm s

Tactic:
apply List.perm_of_nodup_nodup_toFinset_eq (nodup_toList _) hs

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : List α
hs : s.Nodup
⊢ s.toFinset.toList.toFinset = s.toFinset
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
s t u : Multiset α
⊢ _root_.Disjoint s (t + u) ↔ _root_.Disjoint s t ∧ _root_.Disjoint s u

Tactic:
rw [_root_.disjoint_comm, disjoint_add_left]

Goal state after:
α : Type u_1
s t u : Multiset α
⊢ _root_.Disjoint t s ∧ _root_.Disjoint u s ↔ _root_.Disjoint s t ∧ _root_.Disjoint s u
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
r : β → β → Prop
m : Multiset α
h : {a | a ∈ m}.Pairwise fun a₁ a₂ ↦ r (f a₁) (f a₂)
a₁ : α
H₁ : a₁ ∈ m
h₁ : f a₁ ∈ {b | b ∈ map f m}
a₂ : α
H₂ : a₂ ∈ m
h₂ : f a₂ ∈ {b | b ∈ map f m}
hn : f a₁ ≠ f a₂
⊢ r (f a₁) (f a₂)

Tactic:
exact h H₁ H₂ (mt (congr_arg f) hn)

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
m : ¬a ∈ s
⊢ filter p (s.erase a) = (filter p s).erase a

Tactic:
· rw [erase_of_notMem m, erase_of_notMem (mt mem_of_mem_filter m)]

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

Goal state before:
pp: α : Type u_1
l₁ l₂ l₃ : List α
h✝ : l₁.length ≤ l₂.length
h : l₁ <+: l₂ ++ l₃
⊢ l₁ <+: l₂

Tactic:
rw [prefix_iff_eq_take] at *; nth_rw 1 [h, take_eq_left_iff]; tauto

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ ¬a ∈ s ∪ t ↔ ¬a ∈ s ∧ ¬a ∈ t

Tactic:
by rw [mem_union, not_or]

Goal state after:
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
β' : Type u_4
f : β ↪ γ
g : α ↪ β
f' : α ↪ β'
g' : β' ↪ γ
h_comm : ∀ (a : α), f (g a) = g' (f' a)
⊢ map f (map g s) = map g' (map f' s)

Tactic:
map_map,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
β' : Type u_4
f : β ↪ γ
g : α ↪ β
f' : α ↪ β'
g' : β' ↪ γ
h_comm : ∀ (a : α), f (g a) = g' (f' a)
⊢ map (g.trans f) s = map (f'.trans g') s
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f g : α → β
s : Finset α
h : Set.EqOn f g ↑s
a✝ : β
x : α
hx : x ∈ s
⊢ f x = a✝ ↔ g x = a✝

Tactic:
by rw [h hx]

Goal state after:
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
⊢ a ∈ image (fun i ↦ f i) (range n) → a ∈ Set.range f

Tactic:
rintro h
    simp only [mem_image, Set.mem_range, mem_range] at *
    rcases h with ⟨i, _, ha⟩
    exact ⟨i, ha⟩

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

Goal state before:
pp: n : ℕ
p i : Fin n
h : p < i
⊢ i.castSucc ≠ 0

Tactic:
cases n
  · exact i.elim0
  · grind [castSucc_ne_zero_iff]

Goal state after:
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
⊢ #s ≤ #t

Tactic:
classical
    let f' : α → β := fun a => f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩)
    apply card_le_card_of_injOn f'
    · aesop (add safe unfold Set.MapsTo)
    · intro a₁ ha₁ a₂ ha₂ haa
      rw [mem_coe] at ha₁ ha₂
      simp only [f', ha₁, ha₂, ← Subtype.ext_iff] at haa
      exact Subtype.ext_iff.mp (hf haa)

Goal state after:
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
f : ℕ → α
hf : ∀ i < n, f i ∈ s
f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j
⊢ Set.MapsTo f ↑(range n) ↑s

Tactic:
simpa [Set.MapsTo, mem_range] using hf

Goal state after:
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #(s \ t ∪ t) = #(s ∪ t)

Tactic:
sdiff_union_self_eq_union

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #(s ∪ t) = #(s ∪ t)
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
hi : i ≠ 0
⊢ predAbove 0 i = i.pred hi

Tactic:
obtain ⟨y, rfl⟩ := exists_succ_eq.2 hi

Goal state after:
n : ℕ
inst✝ : NeZero n
y : Fin n
hi : y.succ ≠ 0
⊢ predAbove 0 y.succ = y.succ.pred hi