mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LE α
inst✝² : LE β
inst✝¹ : EquivLike F α β
inst✝ : OrderIsoClass F α β
f : F
a b : β
⊢ EquivLike.inv f b ≤ EquivLike.inv f a ↔ b ≤ a

Tactic:
by
  simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : EquivLike F α β
inst✝ : OrderIsoClass F α β
f : F
a b : β
⊢ EquivLike.inv f b < EquivLike.inv f a ↔ b < a

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case a
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a * b)⁻¹ ≤ |a|ₘ * |b|ₘ

Tactic:
mul_inv

Goal state after:
case a
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ a⁻¹ * b⁻¹ ≤ |a|ₘ * |b|ₘ
Module: Mathlib.Data.Nat.Cast.NeZero

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ 1 ≤ n

Tactic:
have := NeZero.ne n

Goal state after:
n : ℕ
inst✝ : NeZero n
this : n ≠ 0
⊢ 1 ≤ n
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: s t : ℤ
r' : ℕ
s' t' : ℤ
⊢ xgcdAux 0 s t r' s' t' = (r', s', t')

Tactic:
rw [xgcdAux, Nat.strongRec_eq]

Goal state after:
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: s t : ℤ
r' : ℕ
s' t' : ℤ
r : ℕ
h : 0 < r.succ
⊢ r.succ.xgcdAux s t r' s' t' = (r' % r.succ).xgcdAux (s' - ↑r' / ↑r.succ * s) (t' - ↑r' / ↑r.succ * t) r.succ s t

Tactic:
rw [xgcdAux, Nat.strongRec_eq]

Goal state after:
s t : ℤ
r' : ℕ
s' t' : ℤ
r : ℕ
h : 0 < r.succ
⊢ (match r.succ, fun m x ↦
      Nat.strongRec (motive := fun x ↦ ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ)
        (fun n ih s t r' s' t' ↦
          match n, ih with
          | 0, ih => (r', s', t')
          | k.succ, ih =>
            have q := r' / k.succ;
            ih (r' % k.succ) ⋯ (s' - ↑q * s) (t' - ↑q * t) k.succ s t)
        m with
    | 0, ih => (r', s', t')
    | k.succ, ih =>
      have q := r' / k.succ;
      ih (r' % k.succ) ⋯ (s' - ↑q * s) (t' - ↑q * t) k.succ s t) =
    (r' % r.succ).xgcdAux (s' - ↑r' / ↑r.succ * s) (t' - ↑r' / ↑r.succ * t) r.succ s t
Module: Mathlib.Algebra.Order.Ring.Int

Goal state before:
pp: q n : ℕ
dvd : gcd 0 q ∣ n
le : pred 0 * q.pred ≤ n
b : ℕ
eq : n = q * b
⊢ 0 * 0 + b * q = n

Tactic:
simpa [mul_comm, eq_comm] using eq

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

Goal state before:
pp: n p : ℕ
dvd : (p + 1).gcd 0 ∣ n
le : (p + 1).pred * pred 0 ≤ n
a : ℕ
eq : n = (p.gcd 0 + 1).gcd 0 * a
⊢ a * (p + 1) + 0 * 0 = n

Tactic:
simpa [mul_comm, eq_comm] using eq

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

Goal state before:
pp: R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsLeftRegular b
ha : a = 0
⊢ b * a = b * 0

Tactic:
rw [ha]

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

Goal state before:
pp: R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsRightRegular b
ha : a = 0
⊢ a * b = 0 * b

Tactic:
rw [ha]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.WithTop

Goal state before:
pp: α : Type u
inst✝² : AddCommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
x : WithBot α
hx : x ≠ ⊥
y : WithBot α
⊢ y ≤ x + y

Tactic:
by
  induction x
  · simp at hx
  induction y
  · simp
  · rw [← WithBot.coe_add, WithBot.coe_le_coe]
    exact le_add_self

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

Goal state before:
pp: G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
a : Gˣ
⊢ withZeroUnitsEquiv.symm ↑a = ↑a

Tactic:
by
  simp

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b✝ c a b : α
h : a + b = 0
⊢ -a = b

Tactic:
by
    have ha : a ≠ ⊤ := by rintro rfl; simp at h
    exact left_neg_eq_right_neg (a := a) (by simp [neg_add_cancel_of_ne_top, *]) h

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝ : AddMonoidWithOne α
⊢ ↑0 = 0

Tactic:
simp [NatCast.natCast]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑(n + 1) = ↑n + 1

Tactic:
simp [NatCast.natCast]

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

Goal state before:
pp: case inl
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
x : R
n : ℤ
hx : |x| ≤ 1
hnx : 0 < n → 0 ≤ x + ↑n
hnx' : n < 0 → x + ↑n ≤ 0
h : n < 0
⊢ 0 ≤ ↑n ∧ 0 ≤ x + ↑n ∨ ↑n ≤ 0 ∧ x + ↑n ≤ 0

Tactic:
exact Or.inr ⟨mod_cast h.le, hnx' h⟩

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommMonoidWithZero α
a b : α
n : ℕ
⊢ ∀ ⦃x : (Additive α)ᵒᵈ⦄, x ≠ ⊤ → IsAddLeftRegular x

Tactic:
by simp; simp +contextual [bot_eq_zero, IsRegular.of_ne_zero]

Goal state after:
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case neg
P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
⊢ findGreatest P (k + 1) = m ↔ m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n

Tactic:
· rw [findGreatest_of_not hk, ihk]
      grind

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
hx : x ≠ 0
⊢ a ≤ x.log ↔ exp a ≤ x

Tactic:
← log_le_log exp_ne_zero hx,

Goal state after:
G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
hx : x ≠ 0
⊢ a ≤ x.log ↔ (exp a).log ≤ x.log
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : AddUnits R
⊢ (-y).mulLeft ↑(-x) = y.mulLeft ↑x

Tactic:
← neg_inj,

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : AddUnits R
⊢ -(-y).mulLeft ↑(-x) = -y.mulLeft ↑x
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
a b : R
inst✝¹ : Invertible a
inst✝ : Invertible b
⊢ -a = a * ⅟a * b + a * ⅟b * a ↔ -a = a * (⅟a * b + ⅟b * a)

Tactic:
by simp only [mul_add, mul_assoc]

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

Goal state before:
pp: R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a ^ n + b ^ n ≤ 2 * (a + b) ^ n

Tactic:
two_mul

Goal state after:
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
n : ℕ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a ^ n + b ^ n ≤ (a + b) ^ n + (a + b) ^ n
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
⊢ (a + b) ^ 2 = a ^ 2 + b ^ 2 + (a * b + b * a)

Tactic:
simp_rw [pow_succ', pow_zero, mul_one, add_mul, mul_add, add_comm (b * a), add_add_add_comm]

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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
⊢ a * a + b * b + (a * a + b * b) = 2 * (a * a + b * b)

Tactic:
two_mul

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

Goal state before:
pp: case h₂.inr
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
hba : b ≤ a
⊢ a ^ (n + 1) * b + b ^ (n + 1) * a ≤ a ^ (n + 1) * a + b ^ (n + 1) * b

Tactic:
exact mul_add_mul_le_mul_add_mul' (by gcongr) hba

Goal state after:
Module: Mathlib.Algebra.Ring.Divisibility.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Semigroup α
inst✝³ : Semigroup β
F : Type u_3
inst✝² : EquivLike F α β
inst✝¹ : MulEquivClass F α β
f : F
inst✝ : DecompositionMonoid β
a b c : α
h : a ∣ b * c
⊢ ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

Tactic:
rw [← map_dvd_iff f, map_mul] at h
    obtain ⟨a₁, a₂, h⟩ := DecompositionMonoid.primal _ h
    refine ⟨EquivLike.inv f a₁, EquivLike.inv f a₂, ?_⟩
    simp_rw [← map_dvd_iff f, EquivLike.apply_inv_apply, h, true_and, ← EquivLike.apply_eq_iff_eq f,
      h.2.2, map_mul, EquivLike.apply_inv_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
⊢ MonotoneOn f₂ s

Tactic:
by
  intro a ha b hb hab
  rw [← h ha, ← h hb]
  exact h₁ ha hb hab

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
⊢ StrictMonoOn f₂ s

Tactic:
by
  intro a ha b hb hab
  rw [← h ha, ← h hb]
  exact h₁ ha hb hab

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

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
f : α' → β' → γ
g : α → α'
h : β → β'
⊢ image2 (fun a b ↦ f (g a) b) univ (h '' univ) = (fun x ↦ f (g x.1) (h x.2)) '' univ

Tactic:
image2_image_right,

Goal state after:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
f : α' → β' → γ
g : α → α'
h : β → β'
⊢ image2 (fun a b ↦ f (g a) (h b)) univ univ = (fun x ↦ f (g x.1) (h x.2)) '' univ
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : α' → β' → δ
g₁ : α → α'
g₂ : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)
⊢ image2 (fun a b ↦ g (f a b)) s t = image2 (fun a b ↦ f' (g₁ a) b) s (g₂ '' t)

Tactic:
image2_image_right,

Goal state after:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : α' → β' → δ
g₁ : α → α'
g₂ : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)
⊢ image2 (fun a b ↦ g (f a b)) s t = image2 (fun a b ↦ f' (g₁ a) (g₂ b)) s t
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
⊢ image2 f (s ∩ s') (t ∪ t') ⊆ image2 f s t ∪ image2 f s' t'

Tactic:
by
  rw [image2_union_right]
  nth_grw 1 [inter_subset_left, inter_subset_right]

Goal state after:
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: α : Type u_1
β : Type u_2
a b c d : α
inst✝¹ : Preorder α
inst✝ : Preorder β
⊢ ∀ {a b : Antisymmetrization (α × β) fun x1 x2 ↦ x1 ≤ x2},
    { toFun := Quotient.lift (fun ab ↦ (⟦ab.1⟧, ⟦ab.2⟧)) ⋯, invFun := uncurry (Quotient.lift₂ (fun a b ↦ ⟦(a, b)⟧) ⋯),
            left_inv := ⋯, right_inv := ⋯ }
          a ≤
        { toFun := Quotient.lift (fun ab ↦ (⟦ab.1⟧, ⟦ab.2⟧)) ⋯,
            invFun := uncurry (Quotient.lift₂ (fun a b ↦ ⟦(a, b)⟧) ⋯), left_inv := ⋯, right_inv := ⋯ }
          b ↔
      a ≤ b

Tactic:
rintro ⟨_⟩ ⟨_⟩; rfl

Goal state after:
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
a a₁ a₂ b b₁ b₂ c x : α
inst✝¹ : One α
inst✝ : IsBotOneClass α
⊢ IsEmpty ↑(Iio 1)

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
a b : α
inst✝ : DenselyOrdered α
⊢ (Ioo a b).Nonempty ↔ a < b

Tactic:
exact nonempty_Ioo

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Preorder α
s t : Set α
hc : IsCofinalFor s t
a : α
has : a ∈ s
⊢ ∃ b ∈ t, a ≤ b

Tactic:
exact hc has

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

Goal state before:
pp: 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
x' : α
hx' : x' ∈ t
hxx' : x ≤ x'
⊢ ∃ z ∈ s ∪ t, (fun x1 x2 ↦ x1 ≤ x2) x z ∧ (fun x1 x2 ↦ x1 ≤ x2) y z

Tactic:
obtain ⟨y', hy', hyy'⟩ := hst.union_left hy

Goal state after:
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
x' : α
hx' : x' ∈ t
hxx' : x ≤ x'
y' : α
hy' : y' ∈ t
hyy' : y ≤ y'
⊢ ∃ z ∈ s ∪ t, (fun x1 x2 ↦ x1 ≤ x2) x z ∧ (fun x1 x2 ↦ x1 ≤ x2) y z
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ IsGreatest {w | w ⊓ a ≤ b} (a ⇨ b)

Tactic:
simp [IsGreatest, mem_upperBounds]

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

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

Tactic:
by rw [div_le_iff₀ hb, one_mul]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
⊢ a < a + a ↔ 0 < a

Tactic:
lt_add_iff_pos_left

Goal state after:
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
⊢ 0 < a ↔ 0 < a
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
h : a ≤ b
⊢ 1 / b ≤ 1 / a

Tactic:
div_le_iff_of_neg' hb,

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
hb : b < 0
h : a ≤ b
⊢ b * (1 / a) ≤ 1
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
x✝¹ : List α
x✝ : List β
h : Forall₂ R x✝¹ x✝
⊢ Forall₂ R (drop 0 x✝¹) (drop 0 x✝)

Tactic:
by simp only [drop, h]

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

Goal state before:
pp: case succ
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
n : ℕ
ihn : ∀ {l : List α} (hl : ∀ (x : α), x ∈ l → p x), (pmap f l hl).insertIdx n (f a ha) = pmap f (l.insertIdx n a) ⋯
l : List α
hl : ∀ (x : α), x ∈ l → p x
⊢ (pmap f l hl).insertIdx (n + 1) (f a ha) = pmap f (l.insertIdx (n + 1) a) ⋯

Tactic:
| succ n ihn =>

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

Goal state before:
pp: α : Type u
l : List α
x : α
n : ℕ
hn : n ≤ l.length
hn' : n < (l.insertIdx n x).length
⊢ (l.insertIdx n x).get ⟨n, hn'⟩ = x

Tactic:
by
  simp

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 γ
l1 : List β
h1 : Forall₂ R l₁ l1
h2 : l1 <+ map f l₂
⊢ ∃ l, Forall₂ (fun a c ↦ R a (f c)) l₁ l ∧ l <+ l₂

Tactic:
obtain ⟨l', hl1, rfl⟩ := sublist_map_iff.mp h2

Goal state after:
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ l' : List γ
hl1 : l' <+ l₂
h1 : Forall₂ R l₁ (map f l')
h2 : map f l' <+ map f l₂
⊢ ∃ l, Forall₂ (fun a c ↦ R a (f c)) l₁ l ∧ l <+ l₂
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
hf' : f 1 1 = 1
f₁ : ι → M
f₂ : ι → N
⊢ (map (fun i ↦ f (f₁ i) (f₂ i)) l).prod = f (map f₁ l).prod (map f₂ l).prod

Tactic:
by
  simp only [prod_eq_foldr, foldr_map]
  rw [← foldr_hom₂ l f _ _ ((fun x y => f (f₁ x) (f₂ x) * y)) _ _ (by simp [hf]), hf']

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

Goal state before:
pp: α : Type u
a : α
l : List α
⊢ (l ++ [a]).getLast ⋯ = a

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u
a : α
l : List α
⊢ (l.concat a).getLast ⋯ = a

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u
l : List α
i : Fin l.length
⊢ l.get i = l[i]?.get ⋯

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u
l : List α
i : ℕ
h : i < l.tail.length
h' : i + 1 < l.length
⊢ l.tail.get ⟨i, h⟩ = l.get ⟨i + 1, h'⟩

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : idxOf a l < l.length
⊢ l.get ⟨idxOf a l, h⟩ = a

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u
l : List α
n : Fin l.reverse.length
hn' : l.length - 1 - ↑n < l.length
⊢ l.reverse.get n = l.get ⟨l.length - 1 - ↑n, hn'⟩

Tactic:
by
  simp

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

Goal state before:
pp: G : Type u_7
inst✝ : Group G
x : G
xs : List G
⊢ (x :: xs).prod⁻¹ = (map (fun x ↦ x⁻¹) (x :: xs)).reverse.prod

Tactic:
simp [prod_append, prod_inv_reverse xs]

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

Goal state before:
pp: α : Type u
l : List α
⊢ (foldl (fun t h ↦ h :: t) [] l).reverse = l

Tactic:
by
  simp

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

Goal state before:
pp: f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : n₂.natAbs.Coprime d₂},
    f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } =
      f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
ha : a /. b = n₁ /. ↑d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
hc : c /. d = n₂ /. ↑d₂
⊢ f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } =
    f₁ a b c d /. f₂ a b c d

Tactic:
rw [fv]

Goal state after:
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : n₂.natAbs.Coprime d₂},
    f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } =
      f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
ha : a /. b = n₁ /. ↑d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
hc : c /. d = n₂ /. ↑d₂
⊢ f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂ = f₁ a b c d /. f₂ a b c d
Module: Mathlib.Data.List.Basic

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

Tactic:
simp [*, filter]

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

Goal state before:
pp: 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✝)

Tactic:
simp [*, filter]

Goal state after:
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✝
⊢ (match p head✝ with
    | true => head✝ :: foldr (fun a out ↦ bif p a then a :: out else out) [] tail✝
    | false => foldr (fun a out ↦ bif p a then a :: out else out) [] tail✝) =
    bif p head✝ then head✝ :: foldr (fun a out ↦ bif p a then a :: out else out) [] tail✝
    else foldr (fun a out ↦ bif p a then a :: out else out) [] tail✝
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: ⊢ 0 ≠ 1

Tactic:
by
  rw [ne_comm, ← divInt_one_one, divInt_ne_zero] <;> lia

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

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

Tactic:
simp [*, filter]

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

Goal state before:
pp: case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : filter (fun x ↦ true) tail✝ = tail✝
⊢ filter (fun x ↦ true) (head✝ :: tail✝) = head✝ :: tail✝

Tactic:
simp [*, filter]

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

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

Tactic:
simp [*, filter]

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

Goal state before:
pp: case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : filter (fun x ↦ false) tail✝ = []
⊢ filter (fun x ↦ false) (head✝ :: tail✝) = []

Tactic:
simp [*, filter]

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

Goal state before:
pp: q r : ℚ
⊢ (q * r).num * ↑q.den * ↑r.den = q.num * r.num * ↑(q * r).den

Tactic:
let s := q.num * r.num /. (q.den * r.den : ℤ)

Goal state after:
q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
⊢ (q * r).num * ↑q.den * ↑r.den = q.num * r.num * ↑(q * r).den
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : PosMulStrictMono R
a b c d : R
hab : a < b
hcd : c < d
⊢ a * c < b * d

Tactic:
have := posMulStrictMono_iff_mulPosStrictMono.1 ‹_›

Goal state after:
R : Type u
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : PosMulStrictMono R
a b c d : R
hab : a < b
hcd : c < d
this : MulPosStrictMono R
⊢ a * c < b * d
Module: Mathlib.Data.Nat.Set

Goal state before:
pp: case e'_4.succ
α : Type u_2
x : α
f : ℕ → α → α
n : ℕ
ihn : rec (f 0 x) (f ∘ succ) n = f n (rec x f n)
⊢ rec (f 0 x) (f ∘ succ) (n + 1) = f (n + 1) (rec x f (n + 1))

Tactic:
| succ n ihn =>

Goal state after:
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → α
k : ℕ
hf : Monotone fun n ↦ ⨅ i, ⨅ (_ : i ≥ n), f i
⊢ ⨆ n, ⨅ i, f (i + n + k) = ⨆ n, ⨅ i, f (i + (n + k))

Tactic:
← Nat.add_assoc

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
κ : ι → Sort u_6
inst✝ : CompleteLattice α
f : (i : ι) → κ i → α
⊢ ⨆ i, ⨆ j, f i j = ⊥ ↔ ∀ (i : ι) (j : κ i), f i j = ⊥

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a b : α
s : α → Set β
⊢ ⋃ x ∈ {a, b}, s x = s a ∪ s b

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
f : ι → Set α
⊢ ⋂ i, f i = ∅ ↔ ∀ (x : α), ∃ i, x ∉ f i

Tactic:
by
  simp [Set.eq_empty_iff_forall_notMem]

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

Goal state before:
pp: α : Type u_1
c : Set (Set α)
⊢ ⋂₀ c = ∅ ↔ ∀ (a : α), ∃ b ∈ c, a ∉ b

Tactic:
by
  simp [Set.eq_empty_iff_forall_notMem]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
⊢ (⋂ i, ⋂ j, s i j).Nonempty ↔ ∃ a, ∀ (i : ι) (j : κ i), a ∈ s i j

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u_1
s : Set (Set α)
⊢ ⋃₀ s = ⋃ i ∈ s, i

Tactic:
rw [← sUnion_image, image_id']

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

Goal state before:
pp: α : Type u_8
s : Set (α → Prop)
a : α
⊢ sSup s a ↔ ∃ r ∈ s, r a

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u_8
s : Set (α → Prop)
a : α
⊢ sInf s a ↔ ∀ r ∈ s, r a

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u_8
β : Type u_9
s : Set (α → β → Prop)
a : α
b : β
⊢ sSup s a b ↔ ∃ r ∈ s, r a b

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u_8
β : Type u_9
s : Set (α → β → Prop)
a : α
b : β
⊢ sInf s a b ↔ ∀ r ∈ s, r a b

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LE α
inst✝ : SupSet α
⊢ sSup {⊤} = ⊤

Tactic:
by
  simp

Goal state after: