Theorem: BunchImpl.Equiv.subbunch (BunchImpl/Equiv.lean)

State before:
P : Type u_1
b1 b2 : Bunch P
h : BunchWithHole P
⊢ b1 ≈ b2 → ↑h b1 ≈ ↑h b2
Tactic:
intro e
State after:
P : Type u_1
b1 b2 : Bunch P
h : BunchWithHole P
e : b1 ≈ b2
⊢ ↑h b1 ≈ ↑h b2

State before:
P : Type u_1
b1 b2 : Bunch P
h : BunchWithHole P
e : b1 ≈ b2
⊢ ↑h b1 ≈ ↑h b2
Tactic:
induction e with
| rel _ _ h =>
  apply EqvGen.rel
  apply PreEquiv.subbunch
  exact h
| refl =>
  exact refl
| symm _ _ _ ih =>
  exact symm ih
| trans _ _ _ _ _ ih1 ih2 =>
  exact trans ih1 ih2
State after:
no goals

State before:
case rel
P : Type u_1
b1 b2 : Bunch P
h✝ : BunchWithHole P
x✝ y✝ : Bunch P
h : PreEquiv x✝ y✝
⊢ ↑h✝ x✝ ≈ ↑h✝ y✝
Tactic:
apply EqvGen.rel
State after:
case rel.a
P : Type u_1
b1 b2 : Bunch P
h✝ : BunchWithHole P
x✝ y✝ : Bunch P
h : PreEquiv x✝ y✝
⊢ PreEquiv (↑h✝ x✝) (↑h✝ y✝)

State before:
case rel.a
P : Type u_1
b1 b2 : Bunch P
h✝ : BunchWithHole P
x✝ y✝ : Bunch P
h : PreEquiv x✝ y✝
⊢ PreEquiv (↑h✝ x✝) (↑h✝ y✝)
Tactic:
apply PreEquiv.subbunch
State after:
case rel.a.a
P : Type u_1
b1 b2 : Bunch P
h✝ : BunchWithHole P
x✝ y✝ : Bunch P
h : PreEquiv x✝ y✝
⊢ PreEquiv x✝ y✝

State before:
case rel.a.a
P : Type u_1
b1 b2 : Bunch P
h✝ : BunchWithHole P
x✝ y✝ : Bunch P
h : PreEquiv x✝ y✝
⊢ PreEquiv x✝ y✝
Tactic:
exact h
State after:
no goals

State before:
case refl
P : Type u_1
b1 b2 : Bunch P
h : BunchWithHole P
x✝ : Bunch P
⊢ ↑h x✝ ≈ ↑h x✝
Tactic:
exact refl
State after:
no goals

State before:
case symm
P : Type u_1
b1 b2 : Bunch P
h : BunchWithHole P
x✝ y✝ : Bunch P
a✝ : EqvGen PreEquiv x✝ y✝
ih : ↑h x✝ ≈ ↑h y✝
⊢ ↑h y✝ ≈ ↑h x✝
Tactic:
exact symm ih
State after:
no goals

State before:
case trans
P : Type u_1
b1 b2 : Bunch P
h : BunchWithHole P
x✝ y✝ z✝ : Bunch P
a✝¹ : EqvGen PreEquiv x✝ y✝
a✝ : EqvGen PreEquiv y✝ z✝
ih1 : ↑h x✝ ≈ ↑h y✝
ih2 : ↑h y✝ ≈ ↑h z✝
⊢ ↑h x✝ ≈ ↑h z✝
Tactic:
exact trans ih1 ih2
State after:
no goals