mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Add α
w x✝ y✝ z✝ : WithBot α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
x y z : WithBot α
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) x y) ((fun x1 x2 ↦ x1 + x2) x z)

Tactic:
cases x <;> cases y <;> cases z <;> simp [← coe_add]; simpa using fun _ ↦ by gcongr

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
⊢ Multiplicative.toAdd (unzero hx) ≤ a ↔ x ≤ exp a

Tactic:
← le_ofAdd_iff hx,

Goal state after:
G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
hx : x ≠ 0
⊢ x ≤ ↑(Multiplicative.ofAdd a) ↔ x ≤ exp a
Module: Mathlib.Order.Directed

Goal state before:
pp: β : Type u_2
inst✝² : PartialOrder β
inst✝¹ : Nontrivial β
inst✝ : IsDirectedOrder β
b : β
hb : IsMax b
hb' : IsMin b
a c : β
hac : c < a
⊢ False

Tactic:
have := hb.isTop a

Goal state after:
β : Type u_2
inst✝² : PartialOrder β
inst✝¹ : Nontrivial β
inst✝ : IsDirectedOrder β
b : β
hb : IsMax b
hb' : IsMin b
a c : β
hac : c < a
this : a ≤ b
⊢ False
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x : AddUnits R
y : R
⊢ ↑x * y + x.neg * y = 0

Tactic:
simp [← add_mul]

Goal state after:
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x : AddUnits R
y : R
⊢ x.neg * y + ↑x * y = 0

Tactic:
simp [← add_mul]

Goal state after:
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Invertible 2
⊢ 1 + 1 - 1 = 1

Tactic:
add_sub_cancel_right

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : Invertible 2
⊢ 1 = 1
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:
by
    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.Algebra.Order.Ring.Basic

Goal state before:
pp: case inr.inr
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
⊢ d < c

Tactic:
refine lt_of_add_lt_add_right (a := a + b) ?_

Goal state after:
case inr.inr
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
⊢ d + (a + b) < c + (a + b)
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝¹⁸ : Zero K
inst✝¹⁷ : Add K
inst✝¹⁶ : Neg K
inst✝¹⁵ : Sub K
inst✝¹⁴ : One K
inst✝¹³ : Mul K
inst✝¹² : Inv K
inst✝¹¹ : Div K
inst✝¹⁰ : SMul ℕ K
inst✝⁹ : SMul ℤ K
inst✝⁸ : SMul ℚ≥0 K
inst✝⁷ : SMul ℚ K
inst✝⁶ : Pow K ℕ
inst✝⁵ : Pow K ℤ
inst✝⁴ : NatCast K
inst✝³ : IntCast K
inst✝² : NNRatCast K
inst✝¹ : RatCast K
f : K → L
hf : Injective f
inst✝ : DivisionRing L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
neg : ∀ (x : K), f (-x) = -f x
sub : ∀ (x y : K), f (x - y) = f x - f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
qsmul : ∀ (q : ℚ) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q
ratCast : ∀ (q : ℚ), f ↑q = ↑q
q : ℚ
a : K
⊢ ↑q * f a = f ↑q * f a

Tactic:
ratCast

Goal state after:
K : Type u_1
L : Type u_2
inst✝¹⁸ : Zero K
inst✝¹⁷ : Add K
inst✝¹⁶ : Neg K
inst✝¹⁵ : Sub K
inst✝¹⁴ : One K
inst✝¹³ : Mul K
inst✝¹² : Inv K
inst✝¹¹ : Div K
inst✝¹⁰ : SMul ℕ K
inst✝⁹ : SMul ℤ K
inst✝⁸ : SMul ℚ≥0 K
inst✝⁷ : SMul ℚ K
inst✝⁶ : Pow K ℕ
inst✝⁵ : Pow K ℤ
inst✝⁴ : NatCast K
inst✝³ : IntCast K
inst✝² : NNRatCast K
inst✝¹ : RatCast K
f : K → L
hf : Injective f
inst✝ : DivisionRing L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
neg : ∀ (x : K), f (-x) = -f x
sub : ∀ (x y : K), f (x - y) = f x - f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
qsmul : ∀ (q : ℚ) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q
ratCast : ∀ (q : ℚ), f ↑q = ↑q
q : ℚ
a : K
⊢ ↑q * f a = ↑q * f a
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
u : Set γ
⊢ image2 f s t ⊆ u ↔ ∀ (a : α), a ∈ s → (fun b ↦ f a b) '' t ⊆ u

Tactic:
simp_rw [image2_subset_iff, image_subset_iff, subset_def, mem_preimage]

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

Goal state before:
pp: α✝¹ : 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
o : ↑s ⊕ ↑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, ⋯⟩)
        o) =
    o

Tactic:
by
    rcases o with (⟨x, h⟩ | ⟨x, h⟩) <;> [simp [hs _ h]; simp [ht _ h]]

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

Goal state before:
pp: α : Type u_3
β : α → Type u_4
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
⊢ (f, g) ∈ ⇑(piEquivPiSubtypeProd p β).symm ⁻¹' univ.pi s ↔ (f, g) ∈ (univ.pi fun i ↦ s ↑i) ×ˢ univ.pi fun i ↦ s ↑i

Tactic:
simp only [mem_preimage, mem_univ_pi, prodMk_mem_set_prod_eq, Subtype.forall, ← forall_and]

Goal state after:
α : Type u_3
β : α → Type u_4
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
⊢ (∀ (i : α), (piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i) ↔
    ∀ (x : α), (∀ (b : p x), f ⟨x, b⟩ ∈ s x) ∧ ∀ (b : ¬p x), g ⟨x, b⟩ ∈ s x
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c : α
⊢ Icc a b = {c} ↔ a = c ∧ b = c

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

Goal state after:
case refine_1
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : Icc a b = {c}
⊢ a = c ∧ b = c

case refine_2
α : Type u_1
inst✝ : PartialOrder α
a b c : α
⊢ a = c ∧ b = c → Icc a b = {c}
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b c d : α
h : a * b / c ≤ d
hc : 0 < c
⊢ b * a ≤ d * c

Tactic:
mul_comm b,

Goal state after:
α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b c d : α
h : a * b / c ≤ d
hc : 0 < c
⊢ a * b ≤ d * c
Module: Mathlib.Data.List.Defs

Goal state before:
pp: α : Type u_1
t : α
ts is : List α
⊢ Prod.Lex (fun a₁ a₂ ↦ a₁ < a₂) (fun a₁ a₂ ↦ a₁ < a₂) (ts.length + (t :: is).length, ts.length)
    ((t :: ts).length + is.length, (t :: ts).length)

Tactic:
simp_wf; grind

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

Goal state before:
pp: α : Type u_1
t : α
ts is : List α
⊢ Prod.Lex (fun a₁ a₂ ↦ a₁ < a₂) (fun a₁ a₂ ↦ a₁ < a₂) (is.length + [].length, is.length)
    ((t :: ts).length + is.length, (t :: ts).length)

Tactic:
simp_wf; grind

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 c : α
hc : c < 0
⊢ a < b / c ↔ b < c * a

Tactic:
by
  rw [mul_comm, lt_div_iff_of_neg hc]

Goal state after:
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
⊢ foldr (fun x y ↦ f (f₁ x) (f₂ x) * y) 1 l = f (foldr (fun x y ↦ f₁ x * y) 1 l) (foldr (fun x y ↦ f₂ x * y) 1 l)

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

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 = (map f (range n)).prod * f n

Tactic:
by
  rw [range_succ, map_append, map_singleton, prod_append, prod_cons, prod_nil, mul_one]

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
ha : a ∈ l
⊢ a ∈ take (l.length - 1) l ↔ idxOf a l < l.length - 1

Tactic:
mem_take_iff_idxOf_lt ha

Goal state after:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
ha : a ∈ l
⊢ idxOf a l < l.length - 1 ↔ idxOf a l < l.length - 1
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
r : ℤ
p : ℤ × M
⊢ ((fun x ↦ zpow' x.2 x.1) ∘ fun x ↦ (r * x.1, x.2)) p = ((fun x ↦ zpow' x r) ∘ fun x ↦ zpow' x.2 x.1) p

Tactic:
simp [← zpow'_mul, mul_comm]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
⊢ map g ∘ map f = map (g ∘ f)

Tactic:
ext l

Goal state after:
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
l : List α
i✝ : ℕ
a✝ : γ
⊢ ((map g ∘ map f) l)[i✝]? = some a✝ ↔ (map (g ∘ f) l)[i✝]? = some a✝
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:
by
    simp_rw [map_map, comp_def, Subtype.map, id, ← Function.comp_apply (g := Subtype.val),
      ← filter_map, attach_map_subtype_val]

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

Goal state before:
pp: x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ n /. x / (d /. x) = n /. d

Tactic:
rw [div_eq_mul_inv, inv_divInt, divInt_mul_divInt_cancel hx]

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

Goal state before:
pp: q : ℚ
⊢ |q|.num = |q.num|

Tactic:
abs_def'

Goal state after:
q : ℚ
⊢ { num := |q.num|, den := q.den, den_nz := ⋯, reduced := ⋯ }.num = |q.num|
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: q : ℚ
⊢ |q|.den = q.den

Tactic:
abs_def'

Goal state after:
q : ℚ
⊢ { num := |q.num|, den := q.den, den_nz := ⋯, reduced := ⋯ }.den = q.den
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: p q : ℚ
hp : 0 ≤ p
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat

Tactic:
by
  rcases le_total 0 q with hq | hq
  · ext; simp [toNNRat, hp, hq, mul_nonneg]
  · have hpq := mul_nonpos_of_nonneg_of_nonpos hp hq
    rw [toNNRat_eq_zero.2 hq, toNNRat_eq_zero.2 hpq, mul_zero]

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

Goal state before:
pp: case inr
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
m n : α
hm : IsPrimal m
hn : IsPrimal n
h0 : m ≠ 0
b : α
⊢ ∀ ⦃c : α⦄, m * n ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ m * n = a₁ * a₂

Tactic:
c

Goal state after:
case inr
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
m n : α
hm : IsPrimal m
hn : IsPrimal n
h0 : m ≠ 0
b c : α
⊢ m * n ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ m * n = a₁ * a₂
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
a d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
hd : ↑d ≠ 0
hb : ↑0 ≠ 0
e : divNat a 0 = ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩
⊢ False

Tactic:
exact hb Nat.cast_zero

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

Goal state before:
pp: b c : ℤ
⊢ ↑(b * c / b) = ↑(b * c) / ↑b

Tactic:
mul_comm b,

Goal state after:
b c : ℤ
⊢ ↑(c * b / b) = ↑(c * b) / ↑b
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case mp
m n : ℤ
hn : ↑n ≠ 0
⊢ ↑(↑m / ↑n).num = ↑m / ↑n → n ∣ m

Tactic:
eq_div_iff hn

Goal state after:
case mp
m n : ℤ
hn : ↑n ≠ 0
⊢ ↑(↑m / ↑n).num * ↑n = ↑m → n ∣ m
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : Nontrivial R
a : R
⊢ Odd a → 0 < a

Tactic:
rintro ⟨k, rfl⟩; simp

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort x
κ : ι → Sort u_1
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
f : (i : ι) → κ i → α
⊢ l (⨆ i, ⨆ j, f i j) = ⨆ i, ⨆ j, l (f i j)

Tactic:
simp_rw [gc.l_iSup]

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

Goal state before:
pp: case mp
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
y : β
s : Set α
hs : s ∈ C
⊢ (fun s ↦ ↑(f s y)) ⟨s, hs⟩ ∈ ⋃₀ C

Tactic:
refine ⟨_, hs, ?_⟩

Goal state after:
case mp
α : Type u_12
β : Type u_13
C : Set (Set α)
f : (s : ↑C) → β → ↑↑s
hf : ∀ (s : ↑C), Surjective (f s)
y : β
s : Set α
hs : s ∈ C
⊢ (fun s ↦ ↑(f s y)) ⟨s, hs⟩ ∈ s
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
⊢ (∃ i, x ∈ range fun x ↦ ↑(f x i)) → ∃ i, x ∈ C i

Tactic:
rintro ⟨y, i, rfl⟩

Goal state after:
case mp
α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
y : β
i : ι
⊢ ∃ i_1, (fun x ↦ ↑(f x y)) i ∈ C i_1
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : Set α
t : (i : ι) → κ i → Set α
⊢ s ∪ ⋂ i, ⋂ j, t i j = ⋂ i, ⋂ j, s ∪ t i j

Tactic:
union_distrib_iInter_left

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α → Set β
s₁ s₂ : Set α
⊢ ⋃ x ∈ s₁, t x ⊆ ⋃ x ∈ s₂ ∪ s₁ \ s₂, t x

Tactic:
apply biUnion_subset_biUnion_left

Goal state after:
α : Type u_1
β : Type u_2
t : α → Set β
s₁ s₂ : Set α
⊢ s₁ ⊆ s₂ ∪ s₁ \ s₂
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α → Set β
s₁ s₂ : Set α
⊢ (⋃ x ∈ s₁, t x) \ ⋃ x ∈ s₂, t x ⊆ ⋃ x ∈ s₁ \ s₂, t x

Tactic:
by
  simp only [sdiff_subset_iff, ← biUnion_union]
  apply biUnion_subset_biUnion_left
  rw [union_sdiff_self]
  apply subset_union_right

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι✝¹ : Sort w
κ : ι✝¹ → Sort w'
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → CompleteAtomicBooleanAlgebra (π i)
ι✝ : Type (max u_1 u_2)
κ✝ : ι✝ → Type (max u_1 u_2)
f : (a : ι✝) → κ✝ a → (i : ι) → π i
⊢ ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)

Tactic:
ext; rw [iInf_iSup_eq]

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
h_ne : i ≠ j
t : Set α
hfi : t ⊆ f i
hfj : t ⊆ f j
ht : ¬t ⊆ ⊥
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ i ≠ j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
replace ht : t.Nonempty := by
    rwa [le_bot_iff, bot_eq_empty, ← Ne, ← nonempty_iff_ne_empty] at ht

Goal state after:
α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
h_ne : i ≠ j
t : Set α
hfi : t ⊆ f i
hfj : t ⊆ f j
ht : t.Nonempty
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ i ≠ j ∧ ∃ x, x ∈ f i ∩ f j
Module: Mathlib.Algebra.Order.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
a : S
ha : 0 ≤ a
b c : S
hbc : b ≤ c
⊢ f 0 ≤ f a

Tactic:
le

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
a : S
ha : 0 ≤ a
b c : S
hbc : b ≤ c
⊢ 0 ≤ a
Module: Mathlib.Algebra.Order.Monoid.Basic

Goal state before:
pp: α : Type u
β : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedCancelMonoid α
inst✝¹ : CommMonoid β
inst✝ : Preorder β
f : β → α
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a b c : β
bc : a * b ≤ a * c
⊢ f (a * b) ≤ f (a * c)

Tactic:
le

Goal state after:
α : Type u
β : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedCancelMonoid α
inst✝¹ : CommMonoid β
inst✝ : Preorder β
f : β → α
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a b c : β
bc : a * b ≤ a * c
⊢ a * b ≤ a * c
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.Tactic.NormNum.DivMod

Goal state before:
pp: a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h₂ : r.blt b' = true
h : ↑r + m = a
⊢ ↑r % ↑b' = ↑r

Tactic:
rw [Int.emod_eq_of_lt] <;> [simp; simpa using h₂]

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

Goal state before:
pp: q : ℚ
K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
hq : 0 < q
⊢ 0 < ↑q

Tactic:
rw [Rat.cast_def]
  exact div_pos (Int.cast_pos.2 <| num_pos.2 hq) (Nat.cast_pos.2 q.pos)

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

Goal state before:
pp: $u✝ «$u» : Level
«$α» : Type u
«$lα» : LE «$α»
«$a» «$b» : «$α»
«$e» : Prop
«$ra» : AddMonoidWithOne «$α»
«$na» : ℕ
«$pa» : IsNat «$a» «$na»
«$rb» : AddMonoidWithOne «$α»
«$nb» : ℕ
«$pb» : IsNat «$b» «$nb»
$fst✝¹ : Semiring «$α»
$fst✝ : PartialOrder «$α»
«$_i» : IsOrderedRing «$α»
⊢ AddMonoidWithOne «$α»

Tactic:
by clear! ra rb; infer_instance

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

Goal state before:
pp: $u✝ «$u» : Level
«$α» : Type u
«$lα» : LE «$α»
«$a» «$b» : «$α»
«$e» : Prop
«$na» : ℕ
«$rb» : AddMonoidWithOne «$α»
«$nb» : ℕ
«$pb» : IsNat «$b» «$nb»
$fst✝¹ : Semiring «$α»
$fst✝ : PartialOrder «$α»
«$_i» : IsOrderedRing «$α»
«$ra» : AddMonoidWithOne «$α» := inferInstance
«$pa» : IsNat «$a» «$na»
⊢ AddMonoidWithOne «$α»

Tactic:
by clear! ra rb; infer_instance

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

Goal state before:
pp: $u✝ «$u» : Level
«$α» : Type u
«$lα» : LT «$α»
«$a» «$b» : «$α»
«$e» : Prop
«$ra» : AddMonoidWithOne «$α»
«$na» : ℕ
«$pa» : IsNat «$a» «$na»
«$rb» : AddMonoidWithOne «$α»
«$nb» : ℕ
«$pb» : IsNat «$b» «$nb»
$fst✝¹ : Semiring «$α»
$fst✝ : PartialOrder «$α»
«$_i» : IsOrderedRing «$α»
⊢ AddMonoidWithOne «$α»

Tactic:
by clear! ra rb; infer_instance

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

Goal state before:
pp: $u✝ «$u» : Level
«$α» : Type u
«$lα» : LT «$α»
«$a» «$b» : «$α»
«$e» : Prop
«$na» : ℕ
«$rb» : AddMonoidWithOne «$α»
«$nb» : ℕ
«$pb» : IsNat «$b» «$nb»
$fst✝¹ : Semiring «$α»
$fst✝ : PartialOrder «$α»
«$_i» : IsOrderedRing «$α»
«$ra» : AddMonoidWithOne «$α» := inferInstance
«$pa» : IsNat «$a» «$na»
⊢ AddMonoidWithOne «$α»

Tactic:
by clear! ra rb; infer_instance

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

Goal state before:
pp: ⊢ (0 + 0) * ascFactorial 0 0 = 0

Tactic:
ascFactorial_zero,

Goal state after:
⊢ (0 + 0) * 1 = 0
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ n * n.succ.ascFactorial 0 = n * n.ascFactorial 0

Tactic:
ascFactorial_zero,

Goal state after:
n : ℕ
⊢ n * 1 = n * n.ascFactorial 0
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
ascFactorial_zero,

Goal state after:
n : ℕ
⊢ n ! * 1 = (n + 0)!
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ n ^ 0 ≤ n.ascFactorial 0

Tactic:
ascFactorial_zero,

Goal state after:
n : ℕ
⊢ n ^ 0 ≤ 1
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ (n + 1).ascFactorial 0 ≤ (n + 0) ^ 0

Tactic:
ascFactorial_zero,

Goal state after:
n : ℕ
⊢ 1 ≤ (n + 0) ^ 0
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ (n + 0).descFactorial 0 = (n + 1).ascFactorial 0

Tactic:
ascFactorial_zero,

Goal state after:
n : ℕ
⊢ (n + 0).descFactorial 0 = 1
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ (n + 0 - 1).descFactorial 0 = n.ascFactorial 0

Tactic:
ascFactorial_zero,

Goal state after:
n : ℕ
⊢ (n + 0 - 1).descFactorial 0 = 1
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
h : k ≤ n
⊢ (n - k)! * n.descFactorial k = (n - k)! * (n ! / (n - k)!)

Tactic:
rw [factorial_mul_descFactorial h]

Goal state after:
n k : ℕ
h : k ≤ n
⊢ n ! = (n - k)! * (n ! / (n - k)!)
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ 2 ^ n * n ! ≤ (2 * n)!

Tactic:
obtain _ | n := n
  · simp
  rw [Nat.mul_comm, Nat.two_mul]
  calc
    _ ≤ (n + 1)! * (n + 2) ^ (n + 1) :=
      Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (le_add_left _ _) _)
    _ ≤ _ := Nat.factorial_mul_pow_le_factorial

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

Goal state before:
pp: case succ
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
n : ℕ
IH : (h : 0 < n) → p ⟨n, h⟩
h : 0 < n + 1
⊢ p ⟨n + 1, h⟩

Tactic:
rcases n with - | n
    · exact one
    · exact succ _ (IH n.succ_pos)

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

Goal state before:
pp: m k : ℕ+
h : k ∣ m
⊢ ↑k * (m.div k).succ = ↑m

Tactic:
rw [← div_add_mod m k, dvd_iff'.mp h, Nat.mul_succ]

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✝² : AddMonoid G
inst✝¹ : AddMonoid H
inst✝ : AddConstMapClass F G H a b
f : F
n : ℕ
⊢ f (n • a) = f 0 + n • b

Tactic:
simpa using map_add_nsmul 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
n : ℕ
| f (x - n • a) + n • b - n • b

Tactic:
add_sub_cancel_right

Goal state after:
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
n : ℕ
| f (x - n • a)