mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.CharZero.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : AddMonoidWithOne M
inst✝ : CharZero M
⊢ ↑1 ≠ 0

Tactic:
Nat.cast_ne_zero

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoidWithOne M
inst✝ : CharZero M
⊢ 1 ≠ 0
Module: Mathlib.Algebra.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : CommSemigroup α
a b c : α
h : a * b ∣ c
d : α
ceq : c = a * b * d
⊢ b * (a * d) = c

Tactic:
by simp [ceq]

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

Goal state before:
pp: α : Type u_3
inst✝ : Semiring α
t : IsCancelMulZero α
⊢ ¬Subsingleton α → IsDomain α

Tactic:
not_subsingleton_iff_nontrivial

Goal state after:
α : Type u_3
inst✝ : Semiring α
t : IsCancelMulZero α
⊢ Nontrivial α → IsDomain α
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x y : M₀
h : IsUnit x
⊢ y * x * x⁻¹ʳ = y

Tactic:
by
  rw [mul_assoc, mul_inverse_cancel x h, mul_one]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
n : ℕ
ha : a ≠ 0
⊢ a ^ Int.negSucc n ≠ 0

Tactic:
by rw [zpow_negSucc]; exact inv_ne_zero (pow_ne_zero _ ha)

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Semiring α
a b : α
n : ℕ
inst✝ : IsCancelAdd α
hn : Odd n
hab : a + b = 0
⊢ a ^ n + b ^ n = 0

Tactic:
by
  obtain ⟨k, rfl⟩ := hn
  induction k with | zero => simpa | succ k ih => ?_
  have : a ^ 2 = b ^ 2 := add_right_cancel <|
    calc
      a ^ 2 + a * b = 0 := by rw [sq, ← mul_add, hab, mul_zero]
      _ = b ^ 2 + a * b := by rw [sq, ← add_mul, add_comm, hab, zero_mul]
  refine add_right_cancel (b := b ^ (2 * k + 1) * a ^ 2) ?_
  calc
    _ = (a ^ (2 * k + 1) + b ^ (2 * k + 1)) * a ^ 2 + b ^ (2 * k + 3) := by
      rw [add_mul, ← pow_add, add_right_comm]; rfl
    _ = _ := by rw [ih, zero_mul, zero_add, zero_add, this, ← pow_add]

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

Goal state before:
pp: α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LE α
inst✝ : MulLeftReflectLE α
a b : α
h : a ≤ a * b
⊢ a * 1 ≤ a * b

Tactic:
by simpa only [mul_one]

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

Goal state before:
pp: α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LE α
inst✝ : MulLeftReflectLE α
a b : α
h : a * b ≤ a
⊢ a * b ≤ a * 1

Tactic:
by simpa only [mul_one]

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

Goal state before:
pp: α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LT α
inst✝ : MulLeftReflectLT α
a b : α
h : a < a * b
⊢ a * 1 < a * b

Tactic:
by simpa only [mul_one]

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

Goal state before:
pp: α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LT α
inst✝ : MulLeftReflectLT α
a b : α
h : a * b < a
⊢ a * b < a * 1

Tactic:
by simpa only [mul_one]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : ContravariantClass α>0 α (fun x y ↦ y * ↑x) fun x1 x2 ↦ x1 < x2
a : { x // 0 ≤ x }
b c : α
h : (fun x1 x2 ↦ x1 < x2) ((fun x y ↦ y * ↑x) a b) ((fun x y ↦ y * ↑x) a c)
⊢ (fun x1 x2 ↦ x1 < x2) b c

Tactic:
by
        obtain ha | ha := a.prop.eq_or_lt
        · simp [← ha] at h
        · exact @ContravariantClass.elim α>0 α (fun x y => y * x) (· < ·) _ ⟨_, ha⟩ _ _ h

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

Goal state before:
pp: α : Sort u
γ : Sort w
inst✝ : Inhabited γ
⊢ (Embedding.refl α).arrowCongrLeft = Embedding.refl (α → γ)

Tactic:
ext
  simp [coe_refl]

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
ha : 0 < a
⊢ a⁻¹ * b ≤ 1 ↔ b ≤ a

Tactic:
rw [inv_mul_le_iff₀ ha, mul_one]

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hb : 0 ≤ b
hc : 0 ≤ c
h : a ≤ c * b
⊢ a * b⁻¹ ≤ c

Tactic:
by
  obtain rfl | hb := hb.eq_or_lt
  · simp [hc]
  · rwa [mul_inv_le_iff₀ hb]

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
a : G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : ZeroLEOneClass G₀
⊢ ¬(0 < a ∧ a ≤ 1) ↔ a ≤ 0 ∨ ¬a ≤ 1

Tactic:
not_and_or,

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
a : G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : ZeroLEOneClass G₀
⊢ ¬0 < a ∨ ¬a ≤ 1 ↔ a ≤ 0 ∨ ¬a ≤ 1
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: x✝ y✝ x y : ℕ
h : 0 < x
IH : ∀ (s t s' t' : ℤ), ((y % x).xgcdAux s t x s' t').1 = (y % x).gcd x
s t s' t' : ℤ
⊢ (y % x).gcd x = x.gcd y

Tactic:
rw [← gcd_rec]

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

Goal state before:
pp: case succ
M : Type u_1
inst✝ : Monoid M
n m : ℕ
y : Mˣ
hn : y ^ ↑n = 1
hm : y ^ ↑(m + 1) = 1
⊢ 1 ^ (m + 1).gcdA n * 1 ^ (m + 1).gcdB n = 1

Tactic:
one_zpow,

Goal state after:
case succ
M : Type u_1
inst✝ : Monoid M
n m : ℕ
y : Mˣ
hn : y ^ ↑n = 1
hm : y ^ ↑(m + 1) = 1
⊢ 1 * 1 ^ (m + 1).gcdB n = 1
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case succ
M : Type u_1
inst✝ : Monoid M
n m : ℕ
y : Mˣ
hn : y ^ ↑n = 1
hm : y ^ ↑(m + 1) = 1
⊢ 1 * 1 ^ (m + 1).gcdB n = 1

Tactic:
one_zpow,

Goal state after:
case succ
M : Type u_1
inst✝ : Monoid M
n m : ℕ
y : Mˣ
hn : y ^ ↑n = 1
hm : y ^ ↑(m + 1) = 1
⊢ 1 * 1 = 1
Module: Mathlib.Algebra.Order.Monoid.WithTop

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

pp: case coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
y : WithBot α
a✝ : α
hx : ↑a✝ ≠ ⊥
⊢ y ≤ y + ↑a✝

Tactic:
· simp at hx

Goal state after:
case coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
y : WithBot α
a✝ : α
hx : ↑a✝ ≠ ⊥
⊢ y ≤ y + ↑a✝
Module: Mathlib.Algebra.Order.Monoid.WithTop

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

pp: case coe
α : Type u
inst✝² : AddCommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
y : WithBot α
a✝ : α
hx : ↑a✝ ≠ ⊥
⊢ y ≤ ↑a✝ + y

Tactic:
· simp at hx

Goal state after:
case coe
α : Type u
inst✝² : AddCommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
y : WithBot α
a✝ : α
hx : ↑a✝ ≠ ⊥
⊢ y ≤ ↑a✝ + y
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : a ≤ b
⊢ a - b + b = max a b

Tactic:
max_eq_right h,

Goal state after:
case inl
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : a ≤ b
⊢ a - b + b = b
Module: Mathlib.Data.Nat.Cast.Order.Ring

Goal state before:
pp: case inr
α : Type u_2
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsOrderedRing α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
n m : ℕ
h : n ≤ m + n
⊢ ↑(m + n - n) = ↑(m + n) - ↑n

Tactic:
add_tsub_cancel_right,

Goal state after:
case inr
α : Type u_2
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsOrderedRing α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
n m : ℕ
h : n ≤ m + n
⊢ ↑m = ↑(m + n) - ↑n
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
x✝ : Nontrivial αˣ ∧ DenselyOrdered αˣ
H₁ : Nontrivial αˣ
H₂ : DenselyOrdered αˣ
x : α
y : αˣ
h : x < ↑y
⊢ ∃ a, x < a ∧ a < ↑y

Tactic:
obtain rfl | hx := eq_zero_or_pos x

Goal state after:
case refine_3.inl
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
x✝ : Nontrivial αˣ ∧ DenselyOrdered αˣ
H₁ : Nontrivial αˣ
H₂ : DenselyOrdered αˣ
y : αˣ
h : 0 < ↑y
⊢ ∃ a, 0 < a ∧ a < ↑y

case refine_3.inr
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
x✝ : Nontrivial αˣ ∧ DenselyOrdered αˣ
H₁ : Nontrivial αˣ
H₂ : DenselyOrdered αˣ
x : α
y : αˣ
h : x < ↑y
hx : 0 < x
⊢ ∃ a, x < a ∧ a < ↑y
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : WithBot α
⊢ x = ⊥ ↔ ∀ (b : α), x < ↑b

Tactic:
cases x <;> simp; simpa using ⟨_, lt_irrefl _⟩

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

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ ⌈a⌉ ≤ z - 1 ↔ a ≤ ↑z - 1

Tactic:
ceil_le

Goal state after:
α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ a ≤ ↑(z - 1) ↔ a ≤ ↑z - 1
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
n : ℕ
inst✝ : IsStrictOrderedRing R
hn : n ≠ 0
⊢ ⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1

Tactic:
by
  rw [← le_floor_iff' hn, ← Nat.cast_one, ← Nat.cast_add, ← floor_lt' (Nat.add_one_ne_zero n),
    Nat.lt_add_one_iff, le_antisymm_iff, and_comm]

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a b : R
⊢ Nat.cast ⁻¹' Ico a b = Ico ⌈a⌉₊ ⌈b⌉₊

Tactic:
ext
  simp [ceil_le, lt_ceil]

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

Goal state before:
pp: α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
⊢ a * c = b ↔ a = b * ⅟c

Tactic:
← mul_left_inj_of_invertible (c := ⅟c),

Goal state after:
α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
⊢ a * c * ⅟c = b * ⅟c ↔ a = b * ⅟c
Module: Mathlib.Algebra.GroupWithZero.Units.Lemmas

Goal state before:
pp: G₀ : Type u_3
G₀' : Type u_5
F : Type u_6
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero G₀'
inst✝¹ : FunLike F G₀ G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a : G₀
⊢ f a⁻¹ = (f a)⁻¹

Tactic:
by_cases h : a = 0

Goal state after:
case pos
G₀ : Type u_3
G₀' : Type u_5
F : Type u_6
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero G₀'
inst✝¹ : FunLike F G₀ G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a : G₀
h : a = 0
⊢ f a⁻¹ = (f a)⁻¹

case neg
G₀ : Type u_3
G₀' : Type u_5
F : Type u_6
inst✝³ : GroupWithZero G₀
inst✝² : GroupWithZero G₀'
inst✝¹ : FunLike F G₀ G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a : G₀
h : ¬a = 0
⊢ f a⁻¹ = (f a)⁻¹
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: case inl
v : ℤ
h : 1 * v = -1
⊢ 1 = 1 ∧ v = -1 ∨ 1 = -1 ∧ v = 1

Tactic:
exact Or.inl ⟨rfl, one_mul v ▸ h⟩

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝ : Field K
a : K
n : ℕ
⊢ a ^ (↑n + 1) = a ^ ↑n * a

Tactic:
by_cases h : a = 0

Goal state after:
case pos
K : Type u_1
L : Type u_2
inst✝ : Field K
a : K
n : ℕ
h : a = 0
⊢ a ^ (↑n + 1) = a ^ ↑n * a

case neg
K : Type u_1
L : Type u_2
inst✝ : Field K
a : K
n : ℕ
h : ¬a = 0
⊢ a ^ (↑n + 1) = a ^ ↑n * a
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ |a| = |b| ↔ |a| * |a| = b * b

Tactic:
← abs_mul_abs_self b

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ |a| = |b| ↔ |a| * |a| = |b| * |b|
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ |a| < |b| ↔ |a| * |a| < b * b

Tactic:
← abs_mul_abs_self b

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ |a| < |b| ↔ |a| * |a| < |b| * |b|
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ |a| ≤ |b| ↔ |a| * |a| ≤ b * b

Tactic:
← abs_mul_abs_self b

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ |a| ≤ |b| ↔ |a| * |a| ≤ |b| * |b|
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → α → β
s t : Set α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f (s ∪ t) (s ∩ t) ⊆ image2 f s t

Tactic:
rw [image2_comm hf]

Goal state after:
α : Type u_1
β : Type u_3
f : α → α → β
s t : Set α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f (s ∩ t) (s ∪ t) ⊆ image2 f s t
Module: Mathlib.Order.WellFounded

Goal state before:
pp: β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
⊢ g ∈ {f | StrictMono f} → range f = range g → f = g

Tactic:
hg

Goal state after:
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
⊢ range f = range g → f = g
Module: Mathlib.Order.Bounds.OrderIso

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set β
x : α
⊢ IsLUB (⇑f.symm '' s) x ↔ IsLUB s (f.symm.symm x)

Tactic:
isLUB_image

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set β
x : α
⊢ IsLUB s (f.symm.symm x) ↔ IsLUB s (f.symm.symm x)
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : SemilatticeInf α
a b c : α
⊢ Ioc a b ∩ Iic c = Ioc a (b ⊓ c)

Tactic:
by
  rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_assoc, Iic_inter_Iic]

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ a / b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

Tactic:
simp [division_def, mul_neg_iff]

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

Goal state before:
pp: case inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
B ε : α
hε : 0 < ε
n : ℕ
this : ∀ (B : α), 0 < B → ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε
B_pos : B ≤ 0
δ : α
δ_pos : δ > 0
cont : ∀ (q r : α), |r| ≤ 1 → |q - r| ≤ δ → |q ^ n - r ^ n| < ε
⊢ ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε

Tactic:
exact ⟨δ, δ_pos, fun q r hr ↦ cont q r (hr.trans (B_pos.trans zero_le_one))⟩

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

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

Tactic:
by
  simp only [reverse_cons, concat_eq_append]

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

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
⊢ (if a = 0 ∧ 0 = 0 then 0 else 1) = a / a

Tactic:
by_cases h : a = 0

Goal state after:
case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
h : a = 0
⊢ (if a = 0 ∧ 0 = 0 then 0 else 1) = a / a

case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
h : ¬a = 0
⊢ (if a = 0 ∧ 0 = 0 then 0 else 1) = a / a
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝ : Inhabited α
t s : List α
h : s ≠ []
⊢ (s ++ t).head! = s.head!

Tactic:
by
  induction s
  · contradiction
  · rfl

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| xs.prod * (y * ys.prod)

Tactic:
rw [mul_comm, mul_assoc]

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| y * (ys.prod * xs.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 ↦ ↑x) (filter p l).attach

Tactic:
← Function.comp_apply (g := Subtype.val),

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

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

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

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
⊢ a ^ n ∣ a ^ m ↔ n ≤ m

Tactic:
by
  constructor
  · intro h
    rw [← not_lt]
    intro hmn
    apply ha
    have : a ^ m * a ∣ a ^ m * 1 := by
      rw [← pow_succ, mul_one]
      exact (pow_dvd_pow _ (Nat.succ_le_of_lt hmn)).trans h
    rwa [mul_dvd_mul_iff_left, ← isUnit_iff_dvd_one] at this
    apply pow_ne_zero m ha₀
  · apply pow_dvd_pow

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

Goal state before:
pp: n : ℕ
⊢ IsSquare ↑n ↔ IsSquare n

Tactic:
simp_rw [isSquare_iff, num_natCast, den_natCast, IsSquare.one, and_true, Int.isSquare_natCast_iff]

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

Goal state before:
pp: a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' = b
hc : c' * c' = c
⊢ Int.ofNat a ^ b' * Int.ofNat a ^ b' = Int.ofNat (c' * c')

Tactic:
← h1

Goal state after:
a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' = b
hc : c' * c' = c
⊢ Int.ofNat a ^ b' * Int.ofNat a ^ b' = Int.ofNat (a.pow b' * a.pow b')
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' + 1 = b
hc : c' * (c' * a) = c
⊢ Int.ofNat a ^ b' * Int.ofNat a ^ b' * -Int.ofNat a = -Int.ofNat (c' * (c' * a))

Tactic:
← h1

Goal state after:
a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' + 1 = b
hc : c' * (c' * a) = c
⊢ Int.ofNat a ^ b' * Int.ofNat a ^ b' * -Int.ofNat a = -Int.ofNat (a.pow b' * (a.pow b' * a))
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: α β : Type u_2
inst : CSLift α β
a b : α
a' b' : β
h1 : CSLiftVal a a'
h2 : CSLiftVal b b'
h : a' = b'
⊢ CSLift.lift a = CSLift.lift b

Tactic:
rwa [← h1.1, ← h2.1]

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

Goal state before:
pp: α : Type u
t : BinaryTree α
m : Type u → Type u_1
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
⊢ traverse pure t = pure t

Tactic:
induction t with
  | nil => rw [traverse]
  | node v l r hl hr =>
    rw [traverse, hl, hr, map_pure, pure_seq, seq_pure, map_pure, map_pure]

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

Goal state before:
pp: α : Type u_1
ι : Type u_8
inst✝ : SupSet α
f : ULift ι → α
⊢ ⨆ i, f i = ⨆ i, f { down := i }

Tactic:
by simp only [iSup]; congr with x; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : α → Set β
⊢ ⋃ i, s i = range fun a ↦ ↑a.snd

Tactic:
simp [Set.ext_iff]

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

Goal state before:
pp: β : Type u_2
ι : Sort u_5
s : ι → Set β
⊢ ⋃ i, s i = range fun a ↦ ↑a.snd

Tactic:
simp [Set.ext_iff]

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

Goal state before:
pp: α : Type u_12
⊢ ⋃ x, {x} = univ

Tactic:
simp [Set.ext_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst✝⁸ : Max α
inst✝⁷ : Min α
inst✝⁶ : LE α
inst✝⁵ : LT α
inst✝⁴ : SupSet α
inst✝³ : InfSet α
inst✝² : Top α
inst✝¹ : Bot α
inst✝ : CompleteLattice β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
x✝ : Set α
⊢ IsLUB ((fun {y} ↦ f y) '' x✝) (f (sSup x✝))

Tactic:
by rw [map_sSup]; exact isLUB_biSup

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : Frame α
ι : Type u_1
ι' : Type u_2
f : ι → α
g : ι' → α
⊢ (⨆ i, f i) ⊓ ⨆ j, g j = ⨆ i, f i.1 ⊓ g i.2

Tactic:
simp_rw [iSup_inf_eq, inf_iSup_eq, iSup_prod]

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 : ι) → CompletelyDistribLattice (π i)
ι✝ : Type (max u_1 u_2)
κ✝ : ι✝ → Type (max u_1 u_2)
f : (a : ι✝) → κ✝ a → (i : ι) → π i
i : ι
⊢ (⨅ a, ⨆ b, f a b) i = (⨆ g, ⨅ a, f a (g a)) i

Tactic:
simp only [iInf_apply, iSup_apply, iInf_iSup_eq]

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

Goal state before:
pp: case pos
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
haS : a ∈ S
h₁ : S ⊆ {⊤}
⊢ ⊤ ≤ a

Tactic:
cases a
        · exact le_rfl
        cases h₁ haS

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
h : (⇑ofDual ⁻¹' s).OrdConnected
⊢ s.OrdConnected

Tactic:
simpa only [ordConnected_def] using! h.dual

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: α : Type u_2
s : Set α
inst✝² : Preorder α
inst✝¹ : InfSet α
inst✝ : Inhabited ↑s
⊢ sInf ∅ = default

Tactic:
by
  simp [sInf]

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
ht : t.Nonempty
h_bdd : BddAbove t
⊢ sSup (Subtype.val '' t) ∈ s

Tactic:
by
  obtain ⟨c, hct⟩ : ∃ c, c ∈ t := ht
  obtain ⟨B, hB⟩ : ∃ B, B ∈ upperBounds t := h_bdd
  refine hs.out c.2 B.2 ⟨?_, ?_⟩
  · exact (Subtype.mono_coe (· ∈ s)).le_csSup_image hct ⟨B, hB⟩
  · exact (Subtype.mono_coe (· ∈ s)).csSup_image_le ⟨c, hct⟩ hB

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:
rw [← Set.not_nonempty_iff_eq_empty, not_not] at hS

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:
rw [← Set.not_nonempty_iff_eq_empty, not_not] at hS

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.Order.CompleteLatticeIntervals

Goal state before:
pp: case pos
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
⊢ IsGLB ∅ ⟨b, ⋯⟩

Tactic:
simp only [isGLB_empty_iff, isTop_iff_eq_top]

Goal state after:
case pos
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
⊢ ⟨b, ⋯⟩ = ⊤
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case mp
n : ℕ
⊢ n ! = 1 → n ≤ 1

Tactic:
intro h
    rw [← not_lt, ← one_lt_factorial, h]
    apply lt_irrefl

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

Goal state before:
pp: case refl
i : ℕ
hi : 2 ≤ i
⊢ i + 1! < (i + 1)!

Tactic:
rw [factorial_one]

Goal state after:
case refl
i : ℕ
hi : 2 ≤ i
⊢ i + 1 < (i + 1)!
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case inl
i n : ℕ
h✝ : 2 ≤ i
⊢ i + (n + 1)! ≤ (i + (n + 1))!

Tactic:
rw [← Nat.add_assoc]

Goal state after:
case inl
i n : ℕ
h✝ : 2 ≤ i
⊢ i + (n + 1)! ≤ (i + n + 1)!
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: ⊢ factorial = factorialBinarySplitting

Tactic:
by
  ext n
  simp [factorialBinarySplitting, ← ascFactorial_eq_ascFactorialBinary]

Goal state after: