mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case fst
R✝ : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹⁶ : Semiring R✝
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst✝¹⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝¹⁴ : (i : ι) → Module R✝ (φ i)
inst✝¹³ : (i : ι) → AddCommMonoid (ψ i)
inst✝¹² : (i : ι) → Module R✝ (ψ i)
inst✝¹¹ : (i : ι) → AddCommMonoid (χ i)
inst✝¹⁰ : (i : ι) → Module R✝ (χ i)
S : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : Module S M✝
inst✝³ : SMulCommClass R✝ S M✝
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
f : α ⊕ β → M
x✝ : α
⊢ ((Equiv.sumArrowEquivProdArrow α β M).toFun (r • f)).1 x✝ =
    ((RingHom.id R) r • (Equiv.sumArrowEquivProdArrow α β M).toFun f).1 x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case snd
R✝ : Type u
K : Type u'
M✝ : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst✝¹⁶ : Semiring R✝
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst✝¹⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝¹⁴ : (i : ι) → Module R✝ (φ i)
inst✝¹³ : (i : ι) → AddCommMonoid (ψ i)
inst✝¹² : (i : ι) → Module R✝ (ψ i)
inst✝¹¹ : (i : ι) → AddCommMonoid (χ i)
inst✝¹⁰ : (i : ι) → Module R✝ (χ i)
S : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : Module S M✝
inst✝³ : SMulCommClass R✝ S M✝
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
f : α ⊕ β → M
x✝ : β
⊢ ((Equiv.sumArrowEquivProdArrow α β M).toFun (r • f)).2 x✝ =
    ((RingHom.id R) r • (Equiv.sumArrowEquivProdArrow α β M).toFun f).2 x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : One α
inst✝³ : LocallyFiniteOrder α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
a b : α
inst✝ : NoMaxOrder α
h : a ≤ b
⊢ insert b (Ico a b) = Ico a (b + 1)

Tactic:
by
  simpa [succ_eq_add_one] using insert_Ico_right_eq_Ico_succ h

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_2.inl
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this : Fintype ι
i : ι
⊢ x (Sum.inl i) = (∑ i, x (Sum.inl i) • single (Sum.inl i) 1) (Sum.inl i)

Tactic:
simp [single_apply]

Goal state after:
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: case e'_4
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a : α
s : Set α
⊢ ⨆ b ∈ s, a ⊓ b = s.toFinset.sup fun i ↦ a ⊓ id i

Tactic:
rw [Finset.sup_eq_iSup]

Goal state after:
case e'_4
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a : α
s : Set α
⊢ ⨆ b ∈ s, a ⊓ b = ⨆ a_1 ∈ s.toFinset, a ⊓ id a_1
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: case e'_4
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a : α
s : Set α
⊢ ⨆ b ∈ s, a ⊓ b = ⨆ a_1 ∈ s, a ⊓ id a_1

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: case e'_3
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a : α
s : Set α
⊢ ⨅ b ∈ s, a ⊔ b = ⨅ a_1 ∈ s, a ⊔ id a_1

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mp.left
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : q ≤ p₁.prod p₂
y1 : M
y2 : M₂
hy1 : (y1, y2) ∈ ↑q
⊢ (LinearMap.fst R M M₂) (y1, y2) ∈ p₁

Tactic:
exact (h hy1).1

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
x y : α
⊢ (p x ∧ p y) = max (p x) (p y)

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
i j : ι
hj : j ∈ Iic i
⊢ j ∈ Set.Iic i

Tactic:
by simpa only [Set.mem_Iic, mem_Iic] using hj

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝⁵ : CommMonoid M
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
f : α → M
a b c : α
⊢ ∏ x ∈ Ico a b, f (x + c) = ∏ x ∈ Ico a b, f ((addRightEmbedding c) x)

Tactic:
rfl

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

Goal state before:
pp: n x y : ℕ
⊢ x < n + 1 ∧ n - x = y ↔ x + y = n

Tactic:
grind

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

Goal state before:
pp: n : ℕ
⊢ (0, n + 1 + 1) ::ₘ ((n + 1).succ, id 0) ::ₘ map (Prod.map Nat.succ id ∘ Prod.map id Nat.succ) (antidiagonal n) =
    (0, n + 2) ::ₘ (n + 2, 0) ::ₘ map (Prod.map Nat.succ Nat.succ) (antidiagonal n)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_4
m n : ℕ
inst✝ : CommGroup M
hmn : m ≤ n
f : ℕ → M
⊢ ∏ i ∈ Ico m (n + 1), f (i + 1) / f i = f (n + 1) / f m

Tactic:
prod_Ico_div

Goal state after:
M : Type u_4
m n : ℕ
inst✝ : CommGroup M
hmn : m ≤ n
f : ℕ → M
⊢ f (n + 1) / f m = f (n + 1) / f m

case hmn
M : Type u_4
m n : ℕ
inst✝ : CommGroup M
hmn : m ≤ n
f : ℕ → M
⊢ m ≤ n + 1
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case h₁
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
a b : Fin n
f : Fin n → α
⊢ ∀ a_1 ∈ range n, a_1 ∉ Icc ↑a ↑b → (if h : a_1 < n then if ⟨a_1, h⟩ ∈ Icc a b then f ⟨a_1, h⟩ else 1 else 1) = 1

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case h₂
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
a b : Fin n
f : Fin n → α
⊢ ∀ a_1 ∈ Icc ↑a ↑b, a_1 ∉ range n → (if h : a_1 < n then f ⟨a_1, h⟩ else 1) = 1

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case h
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
a b : Fin n
f : Fin n → α
⊢ ∀ a_1 ∈ range n,
    a_1 ∈ Icc ↑a ↑b →
      (if h : a_1 < n then if ⟨a_1, h⟩ ∈ Icc a b then f ⟨a_1, h⟩ else 1 else 1) = if h : a_1 < n then f ⟨a_1, h⟩ else 1

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ ∀ a_1 ∈ range n,
    a_1 ∉ range (↑a + 1) →
      (if h : a_1 < n then if ⟨a_1, h⟩ ∈ Iic a then f ⟨a_1, h⟩.succ / f ⟨a_1, h⟩.castSucc else 1 else 1) = 1

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ ∀ a_1 ∈ range (↑a + 1),
    a_1 ∉ range n →
      ((if hi : a_1 + 1 < n + 1 then f ⟨a_1 + 1, hi⟩ else 1) / if hi : a_1 < n + 1 then f ⟨a_1, hi⟩ else 1) = 1

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ ∀ (a_1 : ℕ) (a_2 : a_1 < n),
    a_1 ≤ ↑a →
      (if ⟨a_1, ⋯⟩ ≤ a then f ⟨a_1 + 1, ⋯⟩ / f ⟨a_1, ⋯⟩ else 1) = f ⟨a_1 + 1, ⋯⟩ / if h : a_1 ≤ n then f ⟨a_1, ⋯⟩ else 1

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case e'_3
M : Type u_3
inst✝ : CommGroup M
n : ℕ
a : Fin n
f : Fin (n + 1) → M
⊢ f a.succ / f 0 = (if hi : ↑a + 1 < n + 1 then f ⟨↑a + 1, hi⟩ else 1) / if hi : 0 < n + 1 then f ⟨0, hi⟩ else 1

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case e'_2.a
M : Type u_3
inst✝ : CommGroup M
n : ℕ
a b : Fin n
hab : a ≤ b
f : Fin (n + 1) → M
x✝ : ℕ
a✝ : ↑a ≤ x✝ ∧ x✝ ≤ ↑b
⊢ (if h : x✝ < n then f ⟨x✝ + 1, ⋯⟩ / f ⟨x✝, ⋯⟩ else 1) =
    (if h : x✝ < n then f ⟨x✝ + 1, ⋯⟩ else 1) / if h : x✝ ≤ n then f ⟨x✝, ⋯⟩ else 1

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case e'_3.e'_5
M : Type u_3
inst✝ : CommGroup M
n : ℕ
a b : Fin n
hab : a ≤ b
f : Fin (n + 1) → M
⊢ f b.succ = if hi : ↑b + 1 < n + 1 then f ⟨↑b + 1, hi⟩ else 1

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case e'_3.e'_6
M : Type u_3
inst✝ : CommGroup M
n : ℕ
a b : Fin n
hab : a ≤ b
f : Fin (n + 1) → M
⊢ f a.castSucc = f ⟨↑a, ⋯⟩

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
⊢ map ({ toFun := fun i ↦ (i, n - i), inj' := ⋯ }.trans { toFun := Prod.swap, inj' := ⋯ }) (range (n + 1)) =
    map { toFun := fun i ↦ (n - i, i), inj' := ⋯ } (range (n + 1))

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
⊢ cons (0, n + 1 + 1)
      (cons (({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ)) (n + 1, 0))
        (map
          (((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }).trans
            ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ)))
          (antidiagonal n))
        ⋯)
      ⋯ =
    cons (0, n + 2)
      (cons (n + 2, 0)
        (map
          ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective })
          (antidiagonal n))
        ⋯)
      ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.BigOperators.NatAntidiagonal

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ f (0, n + 1) *
      ∏ x ∈ antidiagonal n,
        f (({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Function.Embedding.refl ℕ)) x) =
    f (0, n + 1) * ∏ p ∈ antidiagonal n, f (p.1 + 1, p.2)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.BigOperators.NatAntidiagonal

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ ∏ x ∈ antidiagonal n, f ({ toFun := Prod.swap, inj' := ⋯ } x).swap = ∏ p ∈ antidiagonal n, f p

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.BigOperators.NatAntidiagonal

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ f (0, n + 1).swap * ∏ p ∈ antidiagonal n, f (p.swap.1 + 1, p.swap.2).swap =
    f (n + 1, 0) * ∏ p ∈ antidiagonal n, f (p.1, p.2 + 1)

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Semiring α
ι : Type u_1
x : ι → α
a : α
x✝ : ∃ y, x ↑y = a
j : ↑{x_1 | x x_1 ≠ 0}
hj : x ↑j = a
⊢ ¬a = 0

Tactic:
grind

Goal state after:
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x ↑I)
IJ : I ≤ J
xJ : x ∈ J
left✝ : 1 ∉ I
oJ : 1 ∈ J
⊢ y ∈ I

Tactic:
rcases Submodule.mem_span_insert.mp oJ with ⟨a, b, h, oe⟩

Goal state after:
α : Type u
inst✝ : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x ↑I)
IJ : I ≤ J
xJ : x ∈ J
left✝ : 1 ∉ I
oJ : 1 ∈ J
a b : α
h : b ∈ Submodule.span α ↑I
oe : 1 = a • x + b
⊢ y ∈ I
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
s : Set α
hs : span s = ⊤
I : Ideal α
hI : I ≠ ⊤
M : Ideal α
hM : M.IsMaximal
le : I ≤ M
this : ∃ a ∈ s, a ∉ ↑M
a : α
has : a ∈ s
haM : a ∉ ↑M
⊢ ∃ r ∈ s, Disjoint ↑I ↑(Submonoid.powers r)

Tactic:
exact ⟨a, has, Set.disjoint_left.mpr fun x hx ⟨n, hn⟩ ↦
    haM (hM.isPrime.mem_of_pow_mem _ (le <| hn ▸ hx))⟩

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: m : ℕ
this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i
⊢ 2 * (2 ^ 2) ^ m = 2 * 4 ^ m

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n k : ℕ
⊢ ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)

Tactic:
rcases lt_or_ge n k with h | h

Goal state after:
case inl
n k : ℕ
h : n < k
⊢ ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)

case inr
n k : ℕ
h : k ≤ n
⊢ ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I J : Ideal R
a b : R
S : Type v
x y : R
inst✝ : I.IsTwoSided
⊢ (ring I).toAddCommGroup = Submodule.Quotient.addCommGroup I

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case succ
n m : ℕ
hm : ∑ k ∈ range (m + 1), (-1) ^ k * ↑((n + 1).choose k) = (-1) ^ m * ↑(n.choose m)
⊢ (-1) ^ m * ↑(n.choose m) + (-1) ^ (m + 1) * ↑(n.choose m + n.choose m.succ) = (-1) ^ (m + 1) * ↑(n.choose (m + 1))

Tactic:
grind

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: case mk.mk
R : Type u
inst✝² : Ring R
I J : Ideal R
a b : R
S : Type v
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
h : I = J
x✝ : R ⧸ I
x : R
y✝ : R ⧸ I
y : R
⊢ (↑(Submodule.quotEquivOfEq I J h)).toFun
      (Quot.mk (⇑(Submodule.quotientRel I)) x * Quot.mk (⇑(Submodule.quotientRel I)) y) =
    (↑(Submodule.quotEquivOfEq I J h)).toFun (Quot.mk (⇑(Submodule.quotientRel I)) x) *
      (↑(Submodule.quotEquivOfEq I J h)).toFun (Quot.mk (⇑(Submodule.quotientRel I)) y)

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝² : Ring R
I J : Ideal R
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
h : I = J
x✝ : R ⧸ J
⊢ (quotEquivOfEq h).symm x✝ = (quotEquivOfEq ⋯) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case mk.mk
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a b : R
inst✝ : I.IsTwoSided
x✝ : (ι → R) ⧸ pi fun x ↦ I
a✝¹ : ι → R
y✝ : (ι → R) ⧸ pi fun x ↦ I
a✝ : ι → R
⊢ Quotient.liftOn'
      (Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) a✝¹ + Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) a✝)
      (fun f i ↦ (Quotient.mk I) (f i)) ⋯ =
    Quotient.liftOn' (Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) a✝¹) (fun f i ↦ (Quotient.mk I) (f i)) ⋯ +
      Quotient.liftOn' (Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) a✝) (fun f i ↦ (Quotient.mk I) (f i)) ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case mk.mk
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a b : R
inst✝ : I.IsTwoSided
m✝ : R ⧸ I
a✝¹ : R
x✝ : (ι → R) ⧸ pi fun x ↦ I
a✝ : ι → R
⊢ Quotient.liftOn' (Quot.mk (⇑(Submodule.quotientRel I)) a✝¹ • Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) a✝)
      (fun f i ↦ (Quotient.mk I) (f i)) ⋯ =
    (RingHom.id (R ⧸ I)) (Quot.mk (⇑(Submodule.quotientRel I)) a✝¹) •
      Quotient.liftOn' (Quot.mk (⇑(Submodule.quotientRel (pi fun x ↦ I))) a✝) (fun f i ↦ (Quotient.mk I) (f i)) ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Filter.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ g✝ : Filter α
s t✝ : Set α
f g : Filter α
x✝ y✝ : Set α
hx : x✝ ∈ {s | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f}
hy : y✝ ∈ {s | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f}
t : Set α
htg : t ∈ g
ht : x✝ ∩ y✝ ⊆ t
⊢ t ∈ f

Tactic:
← union_eq_right.2 ht,

Goal state after:
α : Type u_1
β : Type u_2
f✝ g✝ : Filter α
s t✝ : Set α
f g : Filter α
x✝ y✝ : Set α
hx : x✝ ∈ {s | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f}
hy : y✝ ∈ {s | ∀ ⦃t : Set α⦄, t ∈ g → s ⊆ t → t ∈ f}
t : Set α
htg : t ∈ g
ht : x✝ ∩ y✝ ⊆ t
⊢ x✝ ∩ y✝ ∪ t ∈ f
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_5
S : α → Submodule R M
x : α →₀ M
⊢ x ∈ submodule S ↔ ∀ (i : α), x i ∈ S i

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
q : α → Prop
⊢ (∀ (i : ι), p i → ∃ x ∈ s i, q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
g₁ g₂ : Filter β
m : α → β
⊢ comap m (g₁ ⊔ g₂) = comap m g₁ ⊔ comap m g₂

Tactic:
rw [sup_eq_iSup, comap_iSup, iSup_bool_eq, Bool.cond_true, Bool.cond_false]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type u_1
ι : Sort x
f✝ g : Filter α
s✝ t : Set α
f : Filter α
s : Set α
⊢ (∀ t ∈ f, ∀ (x : α), x ∈ s ∨ x ∈ t) ↔ ∀ (x : α), (∀ t ∈ f, x ∈ t) ∨ x ∈ s

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Filter.Tendsto

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
x : Filter α
y₁ y₂ : Filter β
⊢ Tendsto f x (y₁ ⊓ y₂) ↔ Tendsto f x y₁ ∧ Tendsto f x y₂

Tactic:
simp only [Tendsto, le_inf_iff]

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
f g : Filter α
⊢ (∀ ⦃s : Set α⦄, s ∈ f → ∀ ⦃s' : Set α⦄, s' ∈ g → (s ∩ s').Nonempty) ↔
    ∀ {p : α → Prop}, (∀ᶠ (x : α) in f, p x) → ∀ {U : Set α}, U ∈ g → ∃ x, p x ∧ x ∈ U

Tactic:
rfl

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

Goal state before:
pp: α : Type u
s : Set α
f : Filter α
⊢ 𝓟 s ≤ f ↔ ∀ V ∈ f, s ⊆ V

Tactic:
by
  simp_rw [le_def, mem_principal]

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

Goal state before:
pp: α : Type u
l : Filter α
p : α → Prop
⊢ (∃ᶠ (x : α) in l, p x) ↔ {x | p x}ᶜ ∉ l

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
f : α → β
hla : la.HasBasis pa sa
⊢ (∀ t ∈ lb, ∃ i, pa i ∧ sa i ⊆ f ⁻¹' t) ↔ ∀ t ∈ lb, ∃ i, pa i ∧ MapsTo f (sa i) t

Tactic:
rfl

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

Goal state before:
pp: α : Type u
β : Type v
l : Filter α
inst✝ : Mul β
f₁ f₂ f₃ : α → β
h : f₁ =ᶠ[l] f₂
⊢ f₃ =ᶠ[l] f₃

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
t : Set α
htf : t ∈ f
htg : t ∈ g
h : InjOn m t
⊢ map m (f ⊓ g) = map m f ⊓ map m g

Tactic:
lift f to Filter t using htf; lift g to Filter t using htg
  replace h : Injective (m ∘ ((↑) : t → α)) := h.injective
  simp only [map_map, ← map_inf Subtype.coe_injective, map_inf h]

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ (map ?f (comap f G ⊓ F)).NeBot ↔ (G ⊓ map f F).NeBot

pp: case f
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ α → ?m.13

pp: α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ Type ?u.26

Tactic:
Filter.push_pull'

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ (G ⊓ map f F).NeBot ↔ (G ⊓ map f F).NeBot
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
F : Filter β
u : α → β
inst✝ : Nonempty α
⊢ (∀ {p : β → Prop}, (∀ᶠ (x : β) in F, p x) → ∀ (a : α), ∃ b, a ≤ b ∧ p (u b)) ↔
    ∀ U ∈ F, ∀ (N : α), ∃ n, N ≤ n ∧ u n ∈ U

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
f : β → ↑(Ioi a)
l : Filter β
⊢ Tendsto (Subtype.val ∘ f) l atTop ↔ Tendsto (fun x ↦ ↑(f x)) l atTop

Tactic:
Function.comp_def

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
f : β → ↑(Ioi a)
l : Filter β
⊢ Tendsto (fun x ↦ ↑(f x)) l atTop ↔ Tendsto (fun x ↦ ↑(f x)) l atTop
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
f : β → ↑(Ici a)
l : Filter β
⊢ Tendsto (Subtype.val ∘ f) l atTop ↔ Tendsto (fun x ↦ ↑(f x)) l atTop

Tactic:
Function.comp_def

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
f : β → ↑(Ici a)
l : Filter β
⊢ Tendsto (fun x ↦ ↑(f x)) l atTop ↔ Tendsto (fun x ↦ ↑(f x)) l atTop
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
inst✝ : NoMaxOrder α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x ↦ f ↑x) atTop l ↔ Tendsto (f ∘ Subtype.val) atTop l

Tactic:
Function.comp_def

Goal state after:
α : Type u_3
β : Type u_4
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
inst✝ : NoMaxOrder α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x ↦ f ↑x) atTop l ↔ Tendsto (fun x ↦ f ↑x) atTop l
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x ↦ f ↑x) atTop l ↔ Tendsto (f ∘ Subtype.val) atTop l

Tactic:
Function.comp_def

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x ↦ f ↑x) atTop l ↔ Tendsto (fun x ↦ f ↑x) atTop l
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝ : SemilatticeSup α
f g : β → α
F : Filter β
hf : Tendsto f F atBot
hg : Tendsto g F atBot
⊢ Tendsto (fun x ↦ f x ⊔ g x) F atBot

Tactic:
Filter.tendsto_atBot

Goal state after:
α : Type u_6
β : Type u_7
inst✝ : SemilatticeSup α
f g : β → α
F : Filter β
hf : ∀ (b : α), ∀ᶠ (a : β) in F, f a ≤ b
hg : ∀ (b : α), ∀ᶠ (a : β) in F, g a ≤ b
⊢ ∀ (b : α), ∀ᶠ (a : β) in F, f a ⊔ g a ≤ b
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : Preorder β
l : Filter α
inst✝¹ : l.NeBot
f : α → β
inst✝ : NoMaxOrder β
h : Tendsto f l atTop
⊢ ¬BddAbove (range f)

Tactic:
by
  rintro ⟨M, hM⟩
  have : ∀ x, f x ≤ M := by aesop
  have : ∅ = f ⁻¹' Ioi M := by aesop (add forward safe not_le_of_gt)
  apply Filter.empty_notMem l
  aesop (add safe Ioi_mem_atTop)

Goal state after:
Module: Mathlib.RingTheory.Noetherian.Defs

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := ⋯
⊢ IsNoetherian R M → WellFoundedGT { N // N.FG }

Tactic:
intro H
    let f : α ↪o Submodule R M := OrderEmbedding.subtype _
    exact OrderEmbedding.wellFoundedLT f.dual

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a₁ : α
b₁ : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : PosSMulStrictMono α β
inst✝ : SMulPosStrictMono α β
h₁ : 0 < a₁
ha : a₁ ≤ a₁
hb : b₁ ≤ b₁
h₂ : 0 < b₁
⊢ a₁ • b₁ = a₁ • b₁

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : PosSMulStrictMono α β
inst✝ : SMulPosStrictMono α β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h₁ : 0 < a₁
h₂ : 0 < b₂
⊢ a₁ • b₁ = a₂ • b₂ ↔ a₁ = a₂ ∧ b₁ = b₂

Tactic:
by
  refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
  simp only [eq_iff_le_not_lt, ha, hb, true_and]
  refine ⟨fun ha ↦ h.not_lt ?_, fun hb ↦ h.not_lt ?_⟩
  · exact (smul_le_smul_of_nonneg_left hb h₁.le).trans_lt (smul_lt_smul_of_pos_right ha h₂)
  · exact (smul_lt_smul_of_pos_left hb h₁).trans_le (smul_le_smul_of_nonneg_right ha h₂.le)

Goal state after: